Proofgold Address

Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Param ordsucc^ordsucc : ι → ι
Definition 15fbd.. := λ x0 : ι → ι → ο . λ x1 . λ x2 : ι → ι . and (∀ x3 . x3 ∈ x1 ⟶ x0 (x2 x3) (x2 (ordsucc x3))) (x0 (x2 x1) (x2 0))
Param bij^bij : ι → ι → (ι → ι) → ο
Definition f1360.. := λ x0 : ι → ι → ο . λ x1 x2 . ∀ x3 : ο . (∀ x4 : ι → ι . and (bij (ordsucc x1) x2 x4) (15fbd.. x0 x1 x4) ⟶ x3) ⟶ x3
Definition Subq^Subq := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
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
Definition u1 := 1
Definition u2 := ordsucc u1
Definition u3 := ordsucc u2
Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Param equip^equip : ι → ι → ο
Definition u4 := ordsucc u3
Known dneg^dneg : ∀ x0 : ο . not (not x0) ⟶ x0
Known In_0_4^In_0_4 : 0 ∈ 4
Known neq_i_sym^neq_i_sym : ∀ x0 x1 . (x0 = x1 ⟶ ∀ x2 : ο . x2) ⟶ x1 = x0 ⟶ ∀ x2 : ο . x2
Param nat_p^nat_p : ι → ο
Known 4fb58..^{Pigeonhole_not_atleastp_ordsucc} : ∀ x0 . nat_p x0 ⟶ not (atleastp (ordsucc x0) x0)
Known nat_4^nat_4 : nat_p 4
Definition u5 := ordsucc u4
Known atleastp_tra^atleastp_tra : ∀ x0 x1 x2 . atleastp x0 x1 ⟶ atleastp x1 x2 ⟶ atleastp x0 x2
Known 368c2.. : ∀ x0 x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ (x1 = x2 ⟶ ∀ x6 : ο . x6) ⟶ (x1 = x3 ⟶ ∀ x6 : ο . x6) ⟶ (x2 = x3 ⟶ ∀ x6 : ο . x6) ⟶ (x1 = x4 ⟶ ∀ x6 : ο . x6) ⟶ (x2 = x4 ⟶ ∀ x6 : ο . x6) ⟶ (x3 = x4 ⟶ ∀ x6 : ο . x6) ⟶ (x1 = x5 ⟶ ∀ x6 : ο . x6) ⟶ (x2 = x5 ⟶ ∀ x6 : ο . x6) ⟶ (x3 = x5 ⟶ ∀ x6 : ο . x6) ⟶ (x4 = x5 ⟶ ∀ x6 : ο . x6) ⟶ atleastp u5 x0
Known equip_atleastp^{equip_atleastp} : ∀ x0 x1 . equip x0 x1 ⟶ atleastp x0 x1
Param binunion^binunion : ι → ι → ι
Param Sing^Sing : ι → ι
Definition SetAdjoin^SetAdjoin := λ x0 x1 . binunion x0 (Sing x1)
Param UPair^UPair : ι → ι → ι
Known aa241.. : ∀ x0 x1 x2 . ∀ x3 : ι → ο . x3 x0 ⟶ x3 x1 ⟶ x3 x2 ⟶ ∀ x4 . x4 ∈ SetAdjoin (UPair x0 x1) x2 ⟶ x3 x4
Known 5d098.. : ∀ x0 x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ (x1 = x2 ⟶ ∀ x4 : ο . x4) ⟶ (x1 = x3 ⟶ ∀ x4 : ο . x4) ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ atleastp u3 x0
Known 6be8c.. : ∀ x0 x1 x2 . x0 ∈ SetAdjoin (UPair x0 x1) x2
Known 535ce.. : ∀ x0 x1 x2 . x1 ∈ SetAdjoin (UPair x0 x1) x2
Known f4e2f.. : ∀ x0 x1 x2 . x2 ∈ SetAdjoin (UPair x0 x1) x2
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Param ap^ap : ι → ι → ι
Param lam^Sigma : ι → (ι → ι) → ι
Param If_i^If_i : ο → ι → ι → ι
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Known cases_4^cases_4 : ∀ x0 . x0 ∈ 4 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 1 ⟶ x1 2 ⟶ x1 3 ⟶ x1 x0
Known tuple_4_0_eq^tuple_4_0_eq : ∀ x0 x1 x2 x3 . ap (lam 4 (λ x5 . If_i (x5 = 0) x0 (If_i (x5 = 1) x1 (If_i (x5 = 2) x2 x3)))) 0 = x0
Known tuple_4_1_eq^tuple_4_1_eq : ∀ x0 x1 x2 x3 . ap (lam 4 (λ x5 . If_i (x5 = 0) x0 (If_i (x5 = 1) x1 (If_i (x5 = 2) x2 x3)))) 1 = x1
Known tuple_4_2_eq^tuple_4_2_eq : ∀ x0 x1 x2 x3 . ap (lam 4 (λ x5 . If_i (x5 = 0) x0 (If_i (x5 = 1) x1 (If_i (x5 = 2) x2 x3)))) 2 = x2
Known tuple_4_3_eq^tuple_4_3_eq : ∀ x0 x1 x2 x3 . ap (lam 4 (λ x5 . If_i (x5 = 0) x0 (If_i (x5 = 1) x1 (If_i (x5 = 2) x2 x3)))) 3 = x3
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 nat_3^nat_3 : nat_p 3
Known 13005.. : ∀ x0 . ∀ x1 : ι → ι . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 = x1 x3 ⟶ x2 = x3) ⟶ atleastp x0 (prim5 x0 x1)
Param setminus^setminus : ι → ι → ι
Known Subq_atleastp^{Subq_atleastp} : ∀ x0 x1 . x0 ⊆ x1 ⟶ atleastp x0 x1
Known ReplE_impred^ReplE_impred : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ prim5 x0 x1 ⟶ ∀ x3 : ο . (∀ x4 . x4 ∈ x0 ⟶ x2 = x1 x4 ⟶ x3) ⟶ x3
Definition nIn^nIn := λ x0 x1 . not (x0 ∈ x1)
Known setminusI^setminusI : ∀ x0 x1 x2 . x2 ∈ x0 ⟶ nIn x2 x1 ⟶ x2 ∈ setminus x0 x1
Known SingE^SingE : ∀ x0 x1 . x1 ∈ Sing x0 ⟶ x1 = x0
Known In_1_4^In_1_4 : 1 ∈ 4
Known In_2_4^In_2_4 : 2 ∈ 4
Known In_3_4^In_3_4 : 3 ∈ 4
Known 7f437.. : ∀ x0 x1 x2 . x2 ∈ x0 ⟶ atleastp x0 (ordsucc x1) ⟶ atleastp (setminus x0 (Sing x2)) x1
Known cases_3^cases_3 : ∀ x0 . x0 ∈ 3 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 1 ⟶ x1 2 ⟶ x1 x0
Param Sep^Sep : ι → (ι → ο) → ι
Known Subq_tra^Subq_tra : ∀ x0 x1 x2 . x0 ⊆ x1 ⟶ x1 ⊆ x2 ⟶ x0 ⊆ x2
Known setminus_Subq^{setminus_Subq} : ∀ x0 x1 . setminus x0 x1 ⊆ x0
Known equip_sym^equip_sym : ∀ x0 x1 . equip x0 x1 ⟶ equip x1 x0
Known 9c223..^{equip_ordsucc_remove1} : ∀ x0 x1 x2 . x2 ∈ x0 ⟶ equip x0 (ordsucc x1) ⟶ equip (setminus x0 (Sing x2)) x1
Known bijE^bijE : ∀ x0 x1 . ∀ x2 : ι → ι . bij x0 x1 x2 ⟶ ∀ x3 : ο . ((∀ x4 . x4 ∈ x0 ⟶ x2 x4 ∈ x1) ⟶ (∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ x2 x4 = x2 x5 ⟶ x4 = x5) ⟶ (∀ x4 . x4 ∈ x1 ⟶ ∀ x5 : ο . (∀ x6 . and (x6 ∈ x0) (x2 x6 = x4) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3
Known SepI^SepI : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2 ∈ x0 ⟶ x1 x2 ⟶ x2 ∈ Sep x0 x1
Known PowerI^PowerI : ∀ x0 x1 . x1 ⊆ x0 ⟶ x1 ∈ prim4 x0
Definition or^or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known UPairE^UPairE : ∀ x0 x1 x2 . x0 ∈ UPair x1 x2 ⟶ or (x0 = x1) (x0 = x2)
Known ced33.. : ∀ x0 x1 . (x0 = x1 ⟶ ∀ x2 : ο . x2) ⟶ equip (UPair x0 x1) u2
Known UPairI1^UPairI1 : ∀ x0 x1 . x0 ∈ UPair x0 x1
Known UPairI2^UPairI2 : ∀ x0 x1 . x1 ∈ UPair x0 x1
Known setminusE1^setminusE1 : ∀ x0 x1 x2 . x2 ∈ setminus x0 x1 ⟶ x2 ∈ x0
Known 77ee8.. : ∀ x0 x1 x2 . ∀ x3 : ι → ι . nat_p x0 ⟶ equip x1 x0 ⟶ equip x2 x0 ⟶ inj x1 x2 x3 ⟶ bij x1 x2 x3
Known 8ac0e.. : ∀ x0 . nat_p x0 ⟶ ∀ x1 . x1 ∈ ordsucc x0 ⟶ equip x0 (setminus (ordsucc x0) (Sing x1))
Known da3b9.. : ∀ x0 . equip x0 u3 ⟶ equip {x1 ∈ prim4 x0|equip x1 u2} u3
Known setminusE^setminusE : ∀ x0 x1 x2 . x2 ∈ setminus x0 x1 ⟶ and (x2 ∈ x0) (nIn x2 x1)
Known SingI^SingI : ∀ x0 . x0 ∈ Sing x0
Theorem 1f34f.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 x3 . x1 x2 x3 ⟶ x1 x3 x2) ⟶ (∀ x2 . x2 ⊆ x0 ⟶ atleastp u3 x2 ⟶ not (∀ x3 . x3 ∈ x2 ⟶ ∀ x4 . x4 ∈ x2 ⟶ (x3 = x4 ⟶ ∀ x5 : ο . x5) ⟶ x1 x3 x4)) ⟶ ∀ x2 . x2 ⊆ x0 ⟶ equip x2 u4 ⟶ ∀ x3 x4 : ι → ι . (∀ x5 . x5 ∈ u4 ⟶ x3 x5 ∈ x2) ⟶ (∀ x5 . x5 ∈ u4 ⟶ x4 x5 ∈ x2) ⟶ (∀ x5 . x5 ∈ u4 ⟶ x3 x5 = x4 x5 ⟶ ∀ x6 : ο . x6) ⟶ (∀ x5 . x5 ∈ u4 ⟶ x1 (x3 x5) (x4 x5)) ⟶ (∀ x5 . x5 ∈ u4 ⟶ ∀ x6 . x6 ∈ u4 ⟶ x3 x5 = x3 x6 ⟶ x4 x5 = x4 x6 ⟶ x5 = x6) ⟶ (∀ x5 . x5 ∈ u4 ⟶ ∀ x6 . x6 ∈ u4 ⟶ x3 x5 = x4 x6 ⟶ x4 x5 = x3 x6 ⟶ x5 = x6) ⟶ f1360.. x1 u3 x2 (proof)
Param binintersect^binintersect : ι → ι → ι
Definition DirGraphOutNeighbors := λ x0 . λ x1 : ι → ι → ο . λ x2 . {x3 ∈ x0|and (x2 = x3 ⟶ ∀ x4 : ο . x4) (x1 x2 x3)}
Param u18 : ι
Definition 4b3fa.. := λ x0 : ι → ι → ο . λ x1 x2 . prim0 (λ x3 . x3 ∈ binintersect (DirGraphOutNeighbors u18 x0 x2) (DirGraphOutNeighbors u18 x0 x1))
Param u6 : ι
Known Eps_i_ex^Eps_i_ex : ∀ x0 : ι → ο . (∀ x1 : ο . (∀ x2 . x0 x2 ⟶ x1) ⟶ x1) ⟶ x0 (prim0 x0)
Known 52ae1.. : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u3 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ x0 x2 x3)) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u6 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ not (x0 x2 x3))) ⟶ ∀ x1 . x1 ∈ u18 ⟶ ∀ x2 . x2 ∈ u18 ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ not (x0 x1 x2) ⟶ atleastp u1 (binintersect (DirGraphOutNeighbors u18 x0 x1) (DirGraphOutNeighbors u18 x0 x2))
Known binunionI1^binunionI1 : ∀ x0 x1 x2 . x2 ∈ x0 ⟶ x2 ∈ binunion x0 x1
Known In_0_1^In_0_1 : 0 ∈ 1
Known binunionI2^binunionI2 : ∀ x0 x1 x2 . x2 ∈ x1 ⟶ x2 ∈ binunion x0 x1
Theorem 998ca.. : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u3 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ x0 x2 x3)) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u6 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ not (x0 x2 x3))) ⟶ ∀ x1 . x1 ∈ u18 ⟶ ∀ x2 . x2 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1)) ⟶ 4b3fa.. x0 x1 x2 ∈ binintersect (DirGraphOutNeighbors u18 x0 x2) (DirGraphOutNeighbors u18 x0 x1) (proof)
Known SepE^SepE : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2 ∈ Sep x0 x1 ⟶ and (x2 ∈ x0) (x1 x2)
Known f5939.. : ∀ x0 . equip u1 x0 ⟶ ∀ x1 : ο . (∀ x2 . and (x2 ∈ x0) (x0 = Sing x2) ⟶ x1) ⟶ x1
Known binintersectI^{binintersectI} : ∀ x0 x1 x2 . x2 ∈ x0 ⟶ x2 ∈ x1 ⟶ x2 ∈ binintersect x0 x1
Known SepE1^SepE1 : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2 ∈ Sep x0 x1 ⟶ x2 ∈ x0
Known setminusE2^setminusE2 : ∀ x0 x1 x2 . x2 ∈ setminus x0 x1 ⟶ nIn x2 x1
Theorem 96f77.. : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u3 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ x0 x2 x3)) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u6 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ not (x0 x2 x3))) ⟶ ∀ x1 . x1 ∈ u18 ⟶ ∀ x2 . x2 ∈ {x3 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x3) (DirGraphOutNeighbors u18 x0 x1)) u1} ⟶ and (4b3fa.. x0 x1 x2 ∈ binintersect (DirGraphOutNeighbors u18 x0 x2) (DirGraphOutNeighbors u18 x0 x1)) (∀ x3 . x3 ∈ DirGraphOutNeighbors u18 x0 x1 ⟶ x0 x3 x2 ⟶ x3 = 4b3fa.. x0 x1 x2) (proof)
Theorem 42af1.. : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u3 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ x0 x2 x3)) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u6 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ not (x0 x2 x3))) ⟶ ∀ x1 . x1 ∈ u18 ⟶ ∀ x2 . x2 ∈ {x3 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x3) (DirGraphOutNeighbors u18 x0 x1)) u1} ⟶ 4b3fa.. x0 x1 x2 ∈ binintersect (DirGraphOutNeighbors u18 x0 x2) (DirGraphOutNeighbors u18 x0 x1) (proof)
Theorem 80db2.. : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u3 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ x0 x2 x3)) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u6 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ not (x0 x2 x3))) ⟶ ∀ x1 . x1 ∈ u18 ⟶ ∀ x2 . x2 ∈ {x3 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x3) (DirGraphOutNeighbors u18 x0 x1)) u1} ⟶ ∀ x3 . x3 ∈ DirGraphOutNeighbors u18 x0 x1 ⟶ x0 x3 x2 ⟶ x3 = 4b3fa.. x0 x1 x2 (proof)
Known binintersectE^{binintersectE} : ∀ x0 x1 x2 . x2 ∈ binintersect x0 x1 ⟶ and (x2 ∈ x0) (x2 ∈ x1)
Known 97232.. : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u3 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ x0 x2 x3)) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u6 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ not (x0 x2 x3))) ⟶ ∀ x1 . x1 ∈ u18 ⟶ ∀ x2 . x2 ∈ DirGraphOutNeighbors u18 x0 x1 ⟶ ∀ x3 . x3 ∈ {x4 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x4) (DirGraphOutNeighbors u18 x0 x1)) u1} ⟶ ∀ x4 . x4 ∈ {x5 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x5) (DirGraphOutNeighbors u18 x0 x1)) u1} ⟶ x0 x3 x2 ⟶ x0 x4 x2 ⟶ x3 = x4
Known SepE2^SepE2 : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2 ∈ Sep x0 x1 ⟶ x1 x2
Known binintersectE1^{binintersectE1} : ∀ x0 x1 x2 . x2 ∈ binintersect x0 x1 ⟶ x2 ∈ x0
Theorem abdca.. : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u3 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ x0 x2 x3)) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u6 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ not (x0 x2 x3))) ⟶ ∀ x1 . x1 ∈ u18 ⟶ ∀ x2 . x2 ∈ {x3 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x3) (DirGraphOutNeighbors u18 x0 x1)) u1} ⟶ ∀ x3 . x3 ∈ {x4 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x4) (DirGraphOutNeighbors u18 x0 x1)) u1} ⟶ 4b3fa.. x0 x1 x2 = 4b3fa.. x0 x1 x3 ⟶ x2 = x3 (proof)
Definition f14ce.. := λ x0 : ι → ι → ο . λ x1 x2 . prim0 (λ x3 . and (x3 ∈ binintersect (DirGraphOutNeighbors u18 x0 x2) (DirGraphOutNeighbors u18 x0 x1)) (x3 = 4b3fa.. x0 x1 x2 ⟶ ∀ x4 : ο . x4))
Known feddd.. : ∀ x0 . equip u2 x0 ⟶ ∀ x1 : ο . (∀ x2 . and (x2 ∈ x0) (∀ x3 : ο . (∀ x4 . and (x4 ∈ x0) (and (x2 = x4 ⟶ ∀ x5 : ο . x5) (x0 = UPair x2 x4)) ⟶ x3) ⟶ x3) ⟶ x1) ⟶ x1
Known xm^xm : ∀ x0 : ο . or x0 (not x0)
Theorem 0ddae.. : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u3 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ x0 x2 x3)) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u6 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ not (x0 x2 x3))) ⟶ ∀ x1 . x1 ∈ u18 ⟶ ∀ x2 . x2 ∈ {x3 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x3) (DirGraphOutNeighbors u18 x0 x1)) u2} ⟶ and (f14ce.. x0 x1 x2 ∈ binintersect (DirGraphOutNeighbors u18 x0 x2) (DirGraphOutNeighbors u18 x0 x1)) (f14ce.. x0 x1 x2 = 4b3fa.. x0 x1 x2 ⟶ ∀ x3 : ο . x3) (proof)
Theorem d5d16.. : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u3 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ x0 x2 x3)) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u6 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ not (x0 x2 x3))) ⟶ ∀ x1 . x1 ∈ u18 ⟶ ∀ x2 . x2 ∈ {x3 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x3) (DirGraphOutNeighbors u18 x0 x1)) u2} ⟶ f14ce.. x0 x1 x2 ∈ binintersect (DirGraphOutNeighbors u18 x0 x2) (DirGraphOutNeighbors u18 x0 x1) (proof)
Theorem 3f745.. : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u3 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ x0 x2 x3)) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u6 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ not (x0 x2 x3))) ⟶ ∀ x1 . x1 ∈ u18 ⟶ ∀ x2 . x2 ∈ {x3 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x3) (DirGraphOutNeighbors u18 x0 x1)) u2} ⟶ f14ce.. x0 x1 x2 = 4b3fa.. x0 x1 x2 ⟶ ∀ x3 : ο . x3 (proof)
Param inv^inv : ι → (ι → ι) → ι → ι
Definition 31e20.. := λ x0 : ι → ι → ο . λ x1 . inv {x2 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x2) (DirGraphOutNeighbors u18 x0 x1)) u1} (4b3fa.. x0 x1)
Known inj_linv^inj_linv : ∀ x0 . ∀ x1 : ι → ι . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 = x1 x3 ⟶ x2 = x3) ⟶ ∀ x2 . x2 ∈ x0 ⟶ inv x0 x1 (x1 x2) = x2
Theorem d70a5.. : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u3 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ x0 x2 x3)) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u6 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ not (x0 x2 x3))) ⟶ ∀ x1 . x1 ∈ u18 ⟶ ∀ x2 . x2 ∈ {x3 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x3) (DirGraphOutNeighbors u18 x0 x1)) u1} ⟶ 31e20.. x0 x1 (4b3fa.. x0 x1 x2) = x2 (proof)
Known cfabd.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 x3 . x1 x2 x3 ⟶ x1 x3 x2) ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ DirGraphOutNeighbors x0 x1 x2 ⟶ x2 ∈ DirGraphOutNeighbors x0 x1 x3
Theorem e1908.. : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u3 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ x0 x2 x3)) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u6 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ not (x0 x2 x3))) ⟶ ∀ x1 . x1 ∈ u18 ⟶ ∀ x2 . x2 ∈ DirGraphOutNeighbors u18 x0 x1 ⟶ ∀ x3 . x3 ∈ setminus (setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))) (DirGraphOutNeighbors u18 x0 x2) ⟶ 4b3fa.. x0 x1 x3 ∈ setminus (DirGraphOutNeighbors u18 x0 x1) (Sing x2) (proof)
Param setsum^setsum : ι → ι → ι
Param add_nat^add_nat : ι → ι → ι
Known 893fe.. : add_nat 4 1 = 5
Known c88e0.. : ∀ x0 x1 x2 x3 . nat_p x0 ⟶ nat_p x1 ⟶ equip x0 x2 ⟶ equip x1 x3 ⟶ equip (add_nat x0 x1) (setsum x2 x3)
Known nat_1^nat_1 : nat_p 1
Known equip_ref^equip_ref : ∀ x0 . equip x0 x0
Known 1fe14.. : ∀ x0 x1 x2 x3 . atleastp x0 x2 ⟶ atleastp x1 x3 ⟶ (∀ x4 . x4 ∈ x2 ⟶ nIn x4 x3) ⟶ atleastp (setsum x0 x1) (binunion x2 x3)
Param u8 : ι
Known 51de2.. : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u3 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ x0 x2 x3)) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u6 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ not (x0 x2 x3))) ⟶ ∀ x1 . x1 ∈ u18 ⟶ and (equip {x2 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x2) (DirGraphOutNeighbors u18 x0 x1)) u1} u4) (equip {x2 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x2) (DirGraphOutNeighbors u18 x0 x1)) u2} u8)
Known 04353.. : ∀ x0 x1 . x1 ∈ x0 ⟶ atleastp u1 x0
Known binunion_Subq_min^{binunion_Subq_min} : ∀ x0 x1 x2 . x0 ⊆ x2 ⟶ x1 ⊆ x2 ⟶ binunion x0 x1 ⊆ x2
Known 6cd03.. : ∀ x0 x1 . x1 ∈ x0 ⟶ Sing x1 ⊆ x0
Known b4538.. : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u3 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ x0 x2 x3)) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u6 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ not (x0 x2 x3))) ⟶ ∀ x1 . x1 ∈ u18 ⟶ equip (DirGraphOutNeighbors u18 x0 x1) u5
Theorem 9fceb.. : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u3 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ x0 x2 x3)) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u6 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ not (x0 x2 x3))) ⟶ ∀ x1 . x1 ∈ u18 ⟶ ∀ x2 . x2 ∈ DirGraphOutNeighbors u18 x0 x1 ⟶ (∀ x3 . x3 ∈ {x4 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x4) (DirGraphOutNeighbors u18 x0 x1)) u1} ⟶ not (x0 x2 x3)) ⟶ ∀ x3 . x3 ∈ setminus {x4 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x4) (DirGraphOutNeighbors u18 x0 x1)) u2} (DirGraphOutNeighbors u18 x0 x2) ⟶ 31e20.. x0 x1 (4b3fa.. x0 x1 x3) ∈ {x4 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x4) (DirGraphOutNeighbors u18 x0 x1)) u1} (proof)
Theorem 23d19.. : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u3 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ x0 x2 x3)) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u6 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ not (x0 x2 x3))) ⟶ ∀ x1 . x1 ∈ u18 ⟶ ∀ x2 . x2 ∈ DirGraphOutNeighbors u18 x0 x1 ⟶ ∀ x3 . x3 ∈ setminus {x4 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x4) (DirGraphOutNeighbors u18 x0 x1)) u2} (DirGraphOutNeighbors u18 x0 x2) ⟶ f14ce.. x0 x1 x3 ∈ setminus (DirGraphOutNeighbors u18 x0 x1) (Sing x2) (proof)
Theorem eb388.. : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u3 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ x0 x2 x3)) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u6 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ not (x0 x2 x3))) ⟶ ∀ x1 . x1 ∈ u18 ⟶ ∀ x2 . x2 ∈ DirGraphOutNeighbors u18 x0 x1 ⟶ (∀ x3 . x3 ∈ {x4 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x4) (DirGraphOutNeighbors u18 x0 x1)) u1} ⟶ not (x0 x2 x3)) ⟶ ∀ x3 . x3 ∈ setminus {x4 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x4) (DirGraphOutNeighbors u18 x0 x1)) u2} (DirGraphOutNeighbors u18 x0 x2) ⟶ 31e20.. x0 x1 (f14ce.. x0 x1 x3) ∈ {x4 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x4) (DirGraphOutNeighbors u18 x0 x1)) u1} (proof)
Known d03c6.. : ∀ x0 . atleastp u4 x0 ⟶ ∀ x1 : ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ (x2 = x3 ⟶ ∀ x6 : ο . x6) ⟶ (x2 = x4 ⟶ ∀ x6 : ο . x6) ⟶ (x2 = x5 ⟶ ∀ x6 : ο . x6) ⟶ (x3 = x4 ⟶ ∀ x6 : ο . x6) ⟶ (x3 = x5 ⟶ ∀ x6 : ο . x6) ⟶ (x4 = x5 ⟶ ∀ x6 : ο . x6) ⟶ x1) ⟶ x1
Known set_ext^set_ext : ∀ x0 x1 . x0 ⊆ x1 ⟶ x1 ⊆ x0 ⟶ x0 = x1
Known d8272.. : ∀ x0 x1 x2 x3 x4 . x0 ∈ SetAdjoin (SetAdjoin (SetAdjoin (UPair x0 x1) x2) x3) x4
Known cc191.. : ∀ x0 x1 x2 x3 x4 . x1 ∈ SetAdjoin (SetAdjoin (SetAdjoin (UPair x0 x1) x2) x3) x4
Known 181b3.. : ∀ x0 x1 x2 x3 x4 . x2 ∈ SetAdjoin (SetAdjoin (SetAdjoin (UPair x0 x1) x2) x3) x4
Known c9ec0.. : ∀ x0 x1 x2 x3 x4 . x3 ∈ SetAdjoin (SetAdjoin (SetAdjoin (UPair x0 x1) x2) x3) x4
Known 6143a.. : ∀ x0 x1 x2 x3 x4 . x4 ∈ SetAdjoin (SetAdjoin (SetAdjoin (UPair x0 x1) x2) x3) x4
Known 69a9c.. : ∀ x0 x1 x2 x3 . x0 ∈ SetAdjoin (SetAdjoin (UPair x0 x1) x2) x3
Known e588e.. : ∀ x0 x1 x2 x3 . x1 ∈ SetAdjoin (SetAdjoin (UPair x0 x1) x2) x3
Known 14338.. : ∀ x0 x1 x2 x3 . x2 ∈ SetAdjoin (SetAdjoin (UPair x0 x1) x2) x3
Known b253c.. : ∀ x0 x1 x2 x3 . x3 ∈ SetAdjoin (SetAdjoin (UPair x0 x1) x2) x3
Known 8698a.. : ∀ x0 x1 x2 x3 . ∀ x4 : ι → ο . x4 x0 ⟶ x4 x1 ⟶ x4 x2 ⟶ x4 x3 ⟶ ∀ x5 . x5 ∈ SetAdjoin (SetAdjoin (UPair x0 x1) x2) x3 ⟶ x4 x5
Known and3I^and3I : ∀ x0 x1 x2 : ο . x0 ⟶ x1 ⟶ x2 ⟶ and (and x0 x1) x2
Theorem 82836.. : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u3 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ x0 x2 x3)) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u6 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ not (x0 x2 x3))) ⟶ ∀ x1 . x1 ∈ u18 ⟶ ∀ x2 . x2 ∈ DirGraphOutNeighbors u18 x0 x1 ⟶ (∀ x3 . x3 ∈ {x4 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x4) (DirGraphOutNeighbors u18 x0 x1)) u1} ⟶ not (x0 x2 x3)) ⟶ ∀ x3 . x3 ∈ setminus (DirGraphOutNeighbors u18 x0 x1) (Sing x2) ⟶ and (and (31e20.. x0 x1 x3 ∈ {x4 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x4) (DirGraphOutNeighbors u18 x0 x1)) u1}) (binintersect (DirGraphOutNeighbors u18 x0 (31e20.. x0 x1 x3)) (DirGraphOutNeighbors u18 x0 x1) = Sing x3)) (4b3fa.. x0 x1 (31e20.. x0 x1 x3) = x3) (proof)
Theorem 68855.. : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u3 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ x0 x2 x3)) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u6 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ not (x0 x2 x3))) ⟶ ∀ x1 . x1 ∈ u18 ⟶ ∀ x2 . x2 ∈ DirGraphOutNeighbors u18 x0 x1 ⟶ (∀ x3 . x3 ∈ {x4 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x4) (DirGraphOutNeighbors u18 x0 x1)) u1} ⟶ not (x0 x2 x3)) ⟶ ∀ x3 . x3 ∈ setminus {x4 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x4) (DirGraphOutNeighbors u18 x0 x1)) u2} (DirGraphOutNeighbors u18 x0 x2) ⟶ 31e20.. x0 x1 (4b3fa.. x0 x1 x3) = 31e20.. x0 x1 (f14ce.. x0 x1 x3) ⟶ ∀ x4 : ο . x4 (proof)
Known Sep_Subq^Sep_Subq : ∀ x0 . ∀ x1 : ι → ο . Sep x0 x1 ⊆ x0
Known 008c0.. : add_nat u3 u3 = u6
Known 185e6.. : ∀ x0 x1 x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ equip x0 (ordsucc (ordsucc x1)) ⟶ equip (setminus x0 (UPair x2 x3)) x1
Known equip_tra^equip_tra : ∀ x0 x1 x2 . equip x0 x1 ⟶ equip x1 x2 ⟶ equip x0 x2
Known binunionE^binunionE : ∀ x0 x1 x2 . x2 ∈ binunion x0 x1 ⟶ or (x2 ∈ x0) (x2 ∈ x1)
Known 7fc90.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 x3 . x1 x2 x3 ⟶ x1 x3 x2) ⟶ (∀ x2 . x2 ⊆ x0 ⟶ atleastp u3 x2 ⟶ not (∀ x3 . x3 ∈ x2 ⟶ ∀ x4 . x4 ∈ x2 ⟶ (x3 = x4 ⟶ ∀ x5 : ο . x5) ⟶ x1 x3 x4)) ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ DirGraphOutNeighbors x0 x1 x2 ⟶ ∀ x4 . x4 ∈ DirGraphOutNeighbors x0 x1 x2 ⟶ (x3 = x4 ⟶ ∀ x5 : ο . x5) ⟶ not (x1 x3 x4)
Known nat_2^nat_2 : nat_p 2
Theorem 8a908.. : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u3 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ x0 x2 x3)) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u6 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ not (x0 x2 x3))) ⟶ ∀ x1 . x1 ∈ u18 ⟶ ∀ x2 . x2 ∈ DirGraphOutNeighbors u18 x0 x1 ⟶ (∀ x3 . x3 ∈ {x4 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x4) (DirGraphOutNeighbors u18 x0 x1)) u1} ⟶ not (x0 x2 x3)) ⟶ ∀ x3 . x3 ∈ setminus {x4 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x4) (DirGraphOutNeighbors u18 x0 x1)) u2} (DirGraphOutNeighbors u18 x0 x2) ⟶ x0 (31e20.. x0 x1 (4b3fa.. x0 x1 x3)) (31e20.. x0 x1 (f14ce.. x0 x1 x3)) (proof)