Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι → ι be given.
Claim L0: ∀ x2 : ι → ι . (∀ x3 . x3 ∈ x0 ⟶ x1 x3 = x2 x3) ⟶ (λ x3 . λ x4 : ι → ι . bij x3 x3 x4) x0 x2 = (λ x3 . λ x4 : ι → ι . bij x3 x3 x4) x0 x1
Let x2 of type ι → ι be given.
Assume H0: ∀ x3 . x3 ∈ x0 ⟶ x1 x3 = x2 x3.
Apply prop_ext_2 with (λ x3 . λ x4 : ι → ι . bij x3 x3 x4) x0 x2, (λ x3 . λ x4 : ι → ι . bij x3 x3 x4) x0 x1 leaving 2 subgoals.
Assume H1: (λ x3 . λ x4 : ι → ι . bij x3 x3 x4) x0 x2.
Apply H1 with (λ x3 . λ x4 : ι → ι . bij x3 x3 x4) x0 x1.
Assume H2: and (∀ x3 . x3 ∈ x0 ⟶ x2 x3 ∈ x0) (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4).
Apply H2 with (∀ x3 . x3 ∈ x0 ⟶ ∃ x4 . and (x4 ∈ x0) (x2 x4 = x3)) ⟶ (λ x3 . λ x4 : ι → ι . bij x3 x3 x4) x0 x1.
Assume H3: ∀ x3 . x3 ∈ x0 ⟶ x2 x3 ∈ x0.
Assume H4: ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4.
Assume H5: ∀ x3 . x3 ∈ x0 ⟶ ∃ x4 . and (x4 ∈ x0) (x2 x4 = x3).
Apply bijI with x0, x0, x1 leaving 3 subgoals.
Let x3 of type ι be given.
Assume H6: x3 ∈ x0.
Apply H0 with x3, λ x4 x5 . x5 ∈ x0 leaving 2 subgoals.
The subproof is completed by applying H6.
Apply H3 with x3.
The subproof is completed by applying H6.
Let x3 of type ι be given.
Assume H6: x3 ∈ x0.
Let x4 of type ι be given.
Assume H7: x4 ∈ x0.
Assume H8: x1 x3 = x1 x4.
Apply H4 with x3, x4 leaving 3 subgoals.
The subproof is completed by applying H6.
The subproof is completed by applying H7.
set y5 to be x2 x3
set y6 to be x3 y5
Claim L9: ∀ x7 : ι → ο . x7 y6 ⟶ x7 y5
Let x7 of type ι → ο be given.
Assume H9: x7 (x4 y6).
set y8 to be λ x8 . x7
Apply H0 with y5, λ x9 x10 . y8 x10 x9 leaving 2 subgoals.
The subproof is completed by applying H6.
Apply H8 with λ x9 . y8.
Apply H0 with x7, λ x9 . y8 leaving 2 subgoals.
The subproof is completed by applying H7.
The subproof is completed by applying H9.
Let x7 of type ι → ι → ο be given.
Apply L9 with λ x8 . x7 x8 y6 ⟶ x7 y6 x8.
Assume H10: x7 y6 y6.
The subproof is completed by applying H10.
Let x3 of type ι be given.
Assume H6: x3 ∈ x0.
Apply H5 with x3, ∃ x4 . and (x4 ∈ x0) (x1 x4 = x3) leaving 2 subgoals.
The subproof is completed by applying H6.
Let x4 of type ι be given.
Assume H7: (λ x5 . and (x5 ∈ x0) (x2 x5 = x3)) x4.
Apply H7 with ∃ x5 . and (x5 ∈ x0) (... = ...).
...
...
Apply unpack_u_o_eq with λ x2 . λ x3 : ι → ι . bij x2 x2 x3, x0, x1.
The subproof is completed by applying L0.
■