Proofgold Address

Param bij^bij : ι → ι → (ι → ι) → ο
Definition equip^equip := λ x0 x1 . ∀ x2 : ο . (∀ x3 : ι → ι . bij x0 x1 x3 ⟶ x2) ⟶ x2
Param Sing^Sing : ι → ι
Param ordsucc^ordsucc : ι → ι
Definition u1 := 1
Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Known bijI^bijI : ∀ x0 x1 . ∀ x2 : ι → ι . (∀ x3 . x3 ∈ x0 ⟶ x2 x3 ∈ x1) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4) ⟶ (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 : ο . (∀ x5 . and (x5 ∈ x0) (x2 x5 = x3) ⟶ x4) ⟶ x4) ⟶ bij x0 x1 x2
Known In_0_1^In_0_1 : 0 ∈ 1
Known SingE^SingE : ∀ x0 x1 . x1 ∈ Sing x0 ⟶ x1 = x0
Known cases_1^cases_1 : ∀ x0 . x0 ∈ 1 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 x0
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Known SingI^SingI : ∀ x0 . x0 ∈ Sing x0
Theorem 5169f..^equip_Sing_1 : ∀ x0 . equip (Sing x0) u1 (proof)
Definition inj^inj := λ x0 x1 . λ x2 : ι → ι . and (∀ x3 . x3 ∈ x0 ⟶ x2 x3 ∈ x1) (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4)
Definition atleastp^atleastp := λ x0 x1 . ∀ x2 : ο . (∀ x3 : ι → ι . inj x0 x1 x3 ⟶ x2) ⟶ x2
Known equip_atleastp^{equip_atleastp} : ∀ x0 x1 . equip x0 x1 ⟶ atleastp x0 x1
Theorem 4f2c3.. : ∀ x0 . atleastp (Sing x0) u1 (proof)
Param nat_p^nat_p : ι → ο
Definition or^or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known nat_ind^nat_ind : ∀ x0 : ι → ο . x0 0 ⟶ (∀ x1 . nat_p x1 ⟶ x0 x1 ⟶ x0 (ordsucc x1)) ⟶ ∀ x1 . nat_p x1 ⟶ x0 x1
Known Empty_or_ex^Empty_or_ex : ∀ x0 . or (x0 = 0) (∀ x1 : ο . (∀ x2 . x2 ∈ x0 ⟶ x1) ⟶ x1)
Known orIL^orIL : ∀ x0 x1 : ο . x0 ⟶ or x0 x1
Known 71267.. : ∀ x0 . atleastp 0 x0
Known orIR^orIR : ∀ x0 x1 : ο . x1 ⟶ or x0 x1
Param binunion^binunion : ι → ι → ι
Param setminus^setminus : ι → ι → ι
Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Definition nIn^nIn := λ x0 x1 . not (x0 ∈ x1)
Param setsum^setsum : ι → ι → ι
Known nat_setsum_ordsucc^{nat_setsum1_ordsucc} : ∀ x0 . nat_p x0 ⟶ setsum 1 x0 = ordsucc x0
Known 385ef.. : ∀ x0 x1 x2 x3 . atleastp x0 x2 ⟶ atleastp x1 x3 ⟶ (∀ x4 . x4 ∈ x0 ⟶ nIn x4 x1) ⟶ atleastp (binunion x0 x1) (setsum x2 x3)
Known nat_ordsucc^nat_ordsucc : ∀ x0 . nat_p x0 ⟶ nat_p (ordsucc x0)
Param combine_funcs^{combine_funcs} : ι → ι → (ι → ι) → (ι → ι) → ι → ι
Param Inj0^Inj0 : ι → ι
Param Inj1^Inj1 : ι → ι
Known f4c7c.. : ∀ x0 x1 . ∀ x2 : ι → ο . (∀ x3 . x3 ∈ x0 ⟶ x2 (Inj0 x3)) ⟶ (∀ x3 . x3 ∈ x1 ⟶ x2 (Inj1 x3)) ⟶ ∀ x3 . x3 ∈ setsum x0 x1 ⟶ x2 x3
Known combine_funcs_eq1^{combine_funcs_eq1} : ∀ x0 x1 . ∀ x2 x3 : ι → ι . ∀ x4 . combine_funcs x0 x1 x2 x3 (Inj0 x4) = x2 x4
Known combine_funcs_eq2^{combine_funcs_eq2} : ∀ x0 x1 . ∀ x2 x3 : ι → ι . ∀ x4 . combine_funcs x0 x1 x2 x3 (Inj1 x4) = x3 x4
Known setminusE1^setminusE1 : ∀ x0 x1 x2 . x2 ∈ setminus x0 x1 ⟶ x2 ∈ x0
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Known setminusE2^setminusE2 : ∀ x0 x1 x2 . x2 ∈ setminus x0 x1 ⟶ nIn x2 x1
Known setminus_nIn_I2^{setminus_nIn_I2} : ∀ x0 x1 x2 . x2 ∈ x1 ⟶ nIn x2 (setminus x0 x1)
Known binunion_com^binunion_com : ∀ x0 x1 . binunion x0 x1 = binunion x1 x0
Known eb0c4..^{binunion_remove1_eq} : ∀ x0 x1 . x1 ∈ x0 ⟶ x0 = binunion (setminus x0 (Sing x1)) (Sing x1)
Theorem 48e0f.. : ∀ x0 . nat_p x0 ⟶ ∀ x1 . or (atleastp x1 x0) (atleastp (ordsucc x0) x1) (proof)
Definition Subq^Subq := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
Param u12 : ι
Definition u2 := ordsucc u1
Definition u3 := ordsucc u2
Definition u4 := ordsucc u3
Definition u5 := ordsucc u4
Param u16 : ι
Definition u6 := ordsucc u5
Param binintersect^binintersect : ι → ι → ι
Known nat_1^nat_1 : nat_p 1
Known 4fb58..^{Pigeonhole_not_atleastp_ordsucc} : ∀ x0 . nat_p x0 ⟶ not (atleastp (ordsucc x0) x0)
Known nat_5^nat_5 : nat_p 5
Known atleastp_tra^atleastp_tra : ∀ x0 x1 x2 . atleastp x0 x1 ⟶ atleastp x1 x2 ⟶ atleastp x0 x2
Known nat_4^nat_4 : nat_p 4
Known binintersectE1^{binintersectE1} : ∀ x0 x1 x2 . x2 ∈ binintersect x0 x1 ⟶ x2 ∈ x0
Known binintersect_Subq_2^{binintersect_Subq_2} : ∀ x0 x1 . binintersect x0 x1 ⊆ x1
Known set_ext^set_ext : ∀ x0 x1 . x0 ⊆ x1 ⟶ x1 ⊆ x0 ⟶ x0 = x1
Known xm^xm : ∀ x0 : ο . or x0 (not x0)
Known binunionI2^binunionI2 : ∀ x0 x1 x2 . x2 ∈ x1 ⟶ x2 ∈ binunion x0 x1
Known binintersectI^{binintersectI} : ∀ x0 x1 x2 . x2 ∈ x0 ⟶ x2 ∈ x1 ⟶ x2 ∈ binintersect x0 x1
Known binunionI1^binunionI1 : ∀ x0 x1 x2 . x2 ∈ x0 ⟶ x2 ∈ binunion x0 x1
Known setminusI^setminusI : ∀ x0 x1 x2 . x2 ∈ x0 ⟶ nIn x2 x1 ⟶ x2 ∈ setminus x0 x1
Known binunionE^binunionE : ∀ x0 x1 x2 . x2 ∈ binunion x0 x1 ⟶ or (x2 ∈ x0) (x2 ∈ x1)
Known binintersectE2^{binintersectE2} : ∀ x0 x1 x2 . x2 ∈ binintersect x0 x1 ⟶ x2 ∈ x1
Theorem a62ab.. : ∀ x0 : ι → ι → ο . (∀ x1 . x1 ⊆ u12 ⟶ atleastp u5 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ not (x0 x2 x3))) ⟶ ∀ x1 . x1 ⊆ u16 ⟶ atleastp u6 x1 ⟶ (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ not (x0 x2 x3)) ⟶ atleastp u2 (setminus x1 u12) (proof)