Search for blocks/addresses/...

Proofgold Proof

pf
Assume H0: ∃ x0 . ∃ x1 : ι → ι . ∃ x2 x3 . ∃ x4 : ι → ι → ι → ι . ∃ x5 : ι → ι → ι → ι → ι → ι → ι . MetaCat_subobject_classifier_p IrreflexiveTransitiveReln BinRelnHom struct_id struct_comp x0 x1 x2 x3 x4 x5.
Apply H0 with False.
Let x0 of type ι be given.
Assume H1: (λ x1 . ∃ x2 : ι → ι . ∃ x3 x4 . ∃ x5 : ι → ι → ι → ι . ∃ x6 : ι → ι → ι → ι → ι → ι → ι . MetaCat_subobject_classifier_p IrreflexiveTransitiveReln BinRelnHom struct_id struct_comp x1 x2 x3 x4 x5 x6) x0.
Apply H1 with False.
Let x1 of type ι → ι be given.
Assume H2: (λ x2 : ι → ι . ∃ x3 x4 . ∃ x5 : ι → ι → ι → ι . ∃ x6 : ι → ι → ι → ι → ι → ι → ι . MetaCat_subobject_classifier_p IrreflexiveTransitiveReln BinRelnHom struct_id struct_comp x0 x2 x3 x4 x5 x6) x1.
Apply H2 with False.
Let x2 of type ι be given.
Assume H3: (λ x3 . ∃ x4 . ∃ x5 : ι → ι → ι → ι . ∃ x6 : ι → ι → ι → ι → ι → ι → ι . MetaCat_subobject_classifier_p IrreflexiveTransitiveReln BinRelnHom struct_id struct_comp x0 x1 x3 x4 x5 x6) x2.
Apply H3 with False.
Let x3 of type ι be given.
Assume H4: (λ x4 . ∃ x5 : ι → ι → ι → ι . ∃ x6 : ι → ι → ι → ι → ι → ι → ι . MetaCat_subobject_classifier_p IrreflexiveTransitiveReln BinRelnHom struct_id struct_comp x0 x1 x2 x4 x5 x6) x3.
Apply H4 with False.
Let x4 of type ι → ι → ι → ι be given.
Assume H5: (λ x5 : ι → ι → ι → ι . ∃ x6 : ι → ι → ι → ι → ι → ι → ι . MetaCat_subobject_classifier_p IrreflexiveTransitiveReln BinRelnHom struct_id struct_comp x0 x1 x2 x3 x5 x6) x4.
Apply H5 with False.
Let x5 of type ι → ι → ι → ι → ι → ι → ι be given.
Assume H6: MetaCat_subobject_classifier_p IrreflexiveTransitiveReln BinRelnHom struct_id struct_comp x0 x1 x2 x3 x4 x5.
Apply H6 with False.
Assume H7: and (and (MetaCat_terminal_p IrreflexiveTransitiveReln BinRelnHom struct_id struct_comp x0 x1) (IrreflexiveTransitiveReln x2)) (BinRelnHom x0 x2 x3).
Apply H7 with (∀ x6 x7 x8 . MetaCat_monic_p IrreflexiveTransitiveReln BinRelnHom struct_id struct_comp x6 x7 x8 ⟶ and (BinRelnHom x7 x2 (x4 x6 x7 x8)) (MetaCat_pullback_p IrreflexiveTransitiveReln BinRelnHom struct_id struct_comp x0 x7 x2 x3 (x4 x6 x7 x8) x6 (x1 x6) x8 (x5 x6 x7 x8))) ⟶ False.
Assume H8: and (MetaCat_terminal_p IrreflexiveTransitiveReln BinRelnHom struct_id struct_comp x0 x1) (IrreflexiveTransitiveReln x2).
Apply H8 with BinRelnHom x0 x2 x3 ⟶ (∀ x6 x7 x8 . MetaCat_monic_p IrreflexiveTransitiveReln BinRelnHom struct_id struct_comp x6 x7 x8 ⟶ and (BinRelnHom x7 x2 (x4 x6 x7 x8)) (MetaCat_pullback_p IrreflexiveTransitiveReln BinRelnHom struct_id struct_comp x0 x7 x2 x3 (x4 x6 x7 x8) x6 (x1 x6) x8 (x5 x6 x7 x8))) ⟶ False.
Assume H9: MetaCat_terminal_p IrreflexiveTransitiveReln BinRelnHom struct_id struct_comp x0 x1.
Apply FalseE with ... ⟶ ... ⟶ (∀ x6 x7 x8 . ... ⟶ and (BinRelnHom x7 x2 (x4 x6 x7 x8)) (MetaCat_pullback_p IrreflexiveTransitiveReln BinRelnHom struct_id struct_comp x0 ... ... ... ... ... ... ... ...)) ⟶ False.
...
■