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 : ι → ι . inj x3 x3 x4) x0 x2 = (λ x3 . λ x4 : ι → ι . inj 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 : ι → ι . inj x3 x3 x4) x0 x2, (λ x3 . λ x4 : ι → ι . inj x3 x3 x4) x0 x1 leaving 2 subgoals.
Assume H1: (λ x3 . λ x4 : ι → ι . inj x3 x3 x4) x0 x2.
Apply H1 with (λ x3 . λ x4 : ι → ι . inj x3 x3 x4) x0 x1.
Assume H2: ∀ x3 . x3 ∈ x0 ⟶ x2 x3 ∈ x0.
Assume H3: ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4.
Apply andI with ∀ x3 . x3 ∈ x0 ⟶ x1 x3 ∈ x0, ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x1 x3 = x1 x4 ⟶ x3 = x4 leaving 2 subgoals.
Let x3 of type ι be given.
Assume H4: x3 ∈ x0.
Apply H0 with x3, λ x4 x5 . x5 ∈ x0 leaving 2 subgoals.
The subproof is completed by applying H4.
Apply H2 with x3.
The subproof is completed by applying H4.
Let x3 of type ι be given.
Assume H4: x3 ∈ x0.
Let x4 of type ι be given.
Assume H5: x4 ∈ x0.
Assume H6: x1 x3 = x1 x4.
Apply H3 with x3, x4 leaving 3 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
set y5 to be x2 x3
set y6 to be x3 y5
Claim L7: ∀ x7 : ι → ο . x7 y6 ⟶ x7 y5
Let x7 of type ι → ο be given.
Assume H7: 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 H4.
Apply H6 with λ x9 . y8.
Apply H0 with x7, λ x9 . y8 leaving 2 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying H7.
Let x7 of type ι → ι → ο be given.
Apply L7 with λ x8 . x7 x8 y6 ⟶ x7 y6 x8.
Assume H8: x7 y6 y6.
The subproof is completed by applying H8.
Assume H1: (λ x3 . λ x4 : ι → ι . inj x3 x3 x4) x0 x1.
Apply H1 with (λ x3 . λ x4 : ι → ι . inj x3 x3 x4) x0 x2.
Assume H2: ∀ x3 . x3 ∈ x0 ⟶ x1 x3 ∈ x0.
Assume H3: ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x1 x3 = x1 x4 ⟶ x3 = x4.
Apply andI with ∀ x3 . x3 ∈ x0 ⟶ x2 x3 ∈ x0, ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4 leaving 2 subgoals.
Let x3 of type ι be given.
Assume H4: x3 ∈ ....
...
...
Apply unpack_u_o_eq with λ x2 . λ x3 : ι → ι . inj x2 x2 x3, x0, x1.
The subproof is completed by applying L0.
■