We will prove f ∈ 𝒫 (∑x ∈ X, ⋃ (Y x)).

Apply PowerI to the current goal.

We will prove f ⊆ ∑x ∈ X, ⋃ (Y x).

Let z be given.

Assume Hz: z ∈ f.

We will prove z ∈ ∑x ∈ X, ⋃ (Y x).

Apply (H1 z Hz) to the current goal.

Assume H3: pair (z 0) (z 1) = z.

Assume H4: z 0 ∈ X.

rewrite the current goal using H3 (from right to left).

We will prove pair (z 0) (z 1) ∈ ∑x ∈ X, ⋃ (Y x).

Apply pair_Sigma to the current goal.

We will prove z 0 ∈ X.

An exact proof term for the current goal is H4.

We will prove z 1 ∈ ⋃ (Y (z 0)).

Apply (UnionI (Y (z 0)) (z 1) (f (z 0))) to the current goal.

We will prove z 1 ∈ f (z 0).

Apply apI to the current goal.

We will prove pair (z 0) (z 1) ∈ f.

rewrite the current goal using H3 (from left to right).

An exact proof term for the current goal is Hz.

We will prove f (z 0) ∈ Y (z 0).

An exact proof term for the current goal is (H2 (z 0) H4).