Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι → ο be given.
Assume H0: ∀ x1 . x0 x1 ⟶ struct_r x1.
Assume H1: ∀ x1 x2 x3 x4 . x0 x1 ⟶ x0 x2 ⟶ BinRelnHom x1 x2 x3 ⟶ BinRelnHom x1 x2 x4 ⟶ x0 (05907.. x1 x2 x3 x4).
Let x1 of type ο be given.
Assume H2: ∀ x2 : ι → ι → ι → ι → ι . (∃ x3 : ι → ι → ι → ι → ι . ∃ x4 : ι → ι → ι → ι → ι → ι → ι . MetaCat_equalizer_struct_p x0 BinRelnHom struct_id struct_comp x2 x3 x4) ⟶ x1.
Apply H2 with 05907...
Let x2 of type ο be given.
Assume H3: ∀ x3 : ι → ι → ι → ι → ι . (∃ x4 : ι → ι → ι → ι → ι → ι → ι . MetaCat_equalizer_struct_p x0 BinRelnHom struct_id struct_comp 05907.. x3 x4) ⟶ x2.
Apply H3 with λ x3 x4 x5 x6 . lam {x7 ∈ ap x3 0|ap x5 x7 = ap x6 x7} (λ x7 . x7).
Let x3 of type ο be given.
Assume H4: ∀ x4 : ι → ι → ι → ι → ι → ι → ι . MetaCat_equalizer_struct_p x0 BinRelnHom struct_id struct_comp 05907.. (λ x5 x6 x7 x8 . lam {x9 ∈ ap x5 0|ap x7 x9 = ap x8 x9} (λ x9 . x9)) x4 ⟶ x3.
Apply H4 with λ x4 x5 x6 x7 x8 x9 . lam (ap x8 0) (λ x10 . ap x9 x10).
Claim L5: ...
...
Let x4 of type ι be given.
Let x5 of type ι be given.
Assume H6: x0 x4.
Assume H7: x0 x5.
Let x6 of type ι be given.
Let x7 of type ι be given.
Assume H8: BinRelnHom x4 x5 x6.
Assume H9: BinRelnHom x4 x5 x7.
Apply L5 with x4, x5, x6, x7, MetaCat_equalizer_p x0 BinRelnHom struct_id struct_comp x4 x5 x6 x7 (05907.. x4 x5 x6 x7) (lam {x8 ∈ ap x4 0|ap x6 x8 = ap x7 x8} (λ x8 . x8)) (λ x8 x9 . lam (ap x8 0) (ap x9)) leaving 5 subgoals.
The subproof is completed by applying H6.
The subproof is completed by applying H7.
The subproof is completed by applying H8.
The subproof is completed by applying H9.
Assume H10: BinRelnHom (05907.. x4 x5 x6 x7) x4 (lam {x8 ∈ ap x4 0|ap x6 x8 = ap x7 x8} (λ x8 . x8)).
Assume H11: struct_comp (05907.. x4 x5 x6 x7) x4 x5 x6 (lam {x8 ∈ ap x4 0|ap x6 x8 = ap x7 x8} (λ x8 . x8)) = struct_comp (05907.. x4 x5 x6 x7) x4 x5 x7 (lam {x8 ∈ ap x4 0|ap x6 x8 = ap x7 x8} (λ x8 . x8)).
Assume H12: ∀ x8 . ... ⟶ ∀ x9 . ... ⟶ ... ⟶ and (and (BinRelnHom x8 (05907.. x4 x5 x6 x7) (lam (ap x8 0) (ap x9))) (struct_comp x8 (05907.. x4 x5 x6 x7) x4 (lam {x10 ∈ ap x4 0|ap x6 ... = ...} ...) ... = ...)) ....
...
■