Let x0 of type ι be given.
Let x1 of type ι → ι be given.
Let x2 of type ι → ι → ο be given.
Let x3 of type ι → ι → ο be given.
Assume H0:
∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x1 x4 ⟶ iff (x2 x4 x5) (x3 x4 x5).
Apply set_of_pairs_ext with
Sep2 x0 x1 x2,
Sep2 x0 x1 x3 leaving 3 subgoals.
The subproof is completed by applying Sep2_set_of_pairs with x0, x1, x2.
The subproof is completed by applying Sep2_set_of_pairs with x0, x1, x3.
Let x4 of type ι be given.
Let x5 of type ι be given.
Apply iffI with
lam 2 (λ x6 . If_i (x6 = 0) x4 x5) ∈ Sep2 x0 x1 x2,
lam 2 (λ x6 . If_i (x6 = 0) x4 x5) ∈ Sep2 x0 x1 x3 leaving 2 subgoals.
Assume H1:
lam 2 (λ x6 . If_i (x6 = 0) x4 x5) ∈ Sep2 x0 x1 x2.
Apply Sep2E' with
x0,
x1,
x2,
x4,
x5,
lam 2 (λ x6 . If_i (x6 = 0) x4 x5) ∈ Sep2 x0 x1 x3 leaving 2 subgoals.
The subproof is completed by applying H1.
Assume H2:
and (x4 ∈ x0) (x5 ∈ x1 x4).
Assume H3: x2 x4 x5.
Apply H2 with
lam 2 (λ x6 . If_i (x6 = 0) x4 x5) ∈ Sep2 x0 x1 x3.
Assume H4: x4 ∈ x0.
Assume H5: x5 ∈ x1 x4.
Apply Sep2I with
x0,
x1,
x3,
x4,
x5 leaving 3 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
Apply H0 with
x4,
x5,
x3 x4 x5 leaving 3 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
Assume H6: x2 x4 x5 ⟶ x3 x4 x5.
Assume H7: x3 x4 x5 ⟶ x2 x4 x5.
Apply H6.
The subproof is completed by applying H3.
Assume H1:
lam 2 (λ x6 . If_i (x6 = 0) x4 x5) ∈ Sep2 x0 x1 x3.
Apply Sep2E' with
x0,
x1,
x3,
x4,
x5,
lam 2 (λ x6 . If_i (x6 = 0) x4 x5) ∈ Sep2 x0 x1 x2 leaving 2 subgoals.
The subproof is completed by applying H1.
Assume H2:
and (x4 ∈ x0) (x5 ∈ x1 x4).
Assume H3: x3 x4 x5.
Apply H2 with
lam 2 (λ x6 . If_i (x6 = 0) x4 x5) ∈ Sep2 x0 x1 x2.
Assume H4: x4 ∈ x0.
Assume H5: x5 ∈ x1 x4.
Apply Sep2I with
x0,
x1,
x2,
x4,
x5 leaving 3 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
Apply H0 with
x4,
x5,
x2 x4 x5 leaving 3 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
Assume H6: x2 x4 x5 ⟶ x3 x4 x5.
Assume H7: x3 x4 x5 ⟶ x2 x4 x5.
Apply H7.
The subproof is completed by applying H3.