Proofgold Address

Known 24526..^nIn_E2 : ∀ x0 x1 . nIn x0 x1 ⟶ In x0 x1 ⟶ False
Known e85f6..^In_irref : ∀ x0 . nIn x0 x0
Theorem 2a3a3..^In_irref_b : ∀ x0 . In x0 x0 ⟶ False (proof)
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Known notE^notE : ∀ x0 : ο . not x0 ⟶ x0 ⟶ False
Theorem 73be6..^neq_i_E : ∀ x0 x1 . not (x0 = x1) ⟶ x0 = x1 ⟶ ∀ x2 : ο . x2 (proof)
Theorem d5300..^neq_i_sym_E : ∀ x0 x1 . not (x0 = x1) ⟶ x1 = x0 ⟶ ∀ x2 : ο . x2 (proof)
Known b515a..^beta : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . In x2 x0 ⟶ ap (lam x0 x1) x2 = x1 x2
Known 71a8d..^In_0_4 : In 0 4
Known 0d2f9..^If_i_1 : ∀ x0 : ο . ∀ x1 x2 . x0 ⟶ If_i x0 x1 x2 = x1
Theorem c2555..^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 (proof)
Known efe66..^In_1_4 : In 1 4
Known 81513..^If_i_0 : ∀ x0 : ο . ∀ x1 x2 . not x0 ⟶ If_i x0 x1 x2 = x2
Known a871f..^neq_1_0 : not (1 = 0)
Theorem 751a0..^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 (proof)
Known 884f0..^In_2_4 : In 2 4
Known db5d7..^neq_2_0 : not (2 = 0)
Known 56778..^neq_2_1 : not (2 = 1)
Theorem 0a38e..^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 (proof)
Known d9ca3..^In_3_4 : In 3 4
Known 97f79..^neq_3_0 : not (3 = 0)
Known 28881..^neq_3_1 : not (3 = 1)
Known f1fc4..^neq_3_2 : not (3 = 2)
Theorem 9ff59..^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 (proof)
Known 5ec9a..^In_0_5 : In 0 5
Theorem e53d3..^tuple_5_0_eq : ∀ x0 x1 x2 x3 x4 . ap (lam 5 (λ x6 . If_i (x6 = 0) x0 (If_i (x6 = 1) x1 (If_i (x6 = 2) x2 (If_i (x6 = 3) x3 x4))))) 0 = x0 (proof)
Known 53692..^In_1_5 : In 1 5
Theorem ad54e..^tuple_5_1_eq : ∀ x0 x1 x2 x3 x4 . ap (lam 5 (λ x6 . If_i (x6 = 0) x0 (If_i (x6 = 1) x1 (If_i (x6 = 2) x2 (If_i (x6 = 3) x3 x4))))) 1 = x1 (proof)
Known 7f632..^In_2_5 : In 2 5
Theorem 3b439..^tuple_5_2_eq : ∀ x0 x1 x2 x3 x4 . ap (lam 5 (λ x6 . If_i (x6 = 0) x0 (If_i (x6 = 1) x1 (If_i (x6 = 2) x2 (If_i (x6 = 3) x3 x4))))) 2 = x2 (proof)
Known c3428..^In_3_5 : In 3 5
Theorem 0bd54..^tuple_5_3_eq : ∀ x0 x1 x2 x3 x4 . ap (lam 5 (λ x6 . If_i (x6 = 0) x0 (If_i (x6 = 1) x1 (If_i (x6 = 2) x2 (If_i (x6 = 3) x3 x4))))) 3 = x3 (proof)
Known 55f57..^In_4_5 : In 4 5
Known fc9ff..^neq_4_0 : not (4 = 0)
Known 34131..^neq_4_1 : not (4 = 1)
Known 547fc..^neq_4_2 : not (4 = 2)
Known bfbcc..^neq_4_3 : not (4 = 3)
Theorem 75457..^tuple_5_4_eq : ∀ x0 x1 x2 x3 x4 . ap (lam 5 (λ x6 . If_i (x6 = 0) x0 (If_i (x6 = 1) x1 (If_i (x6 = 2) x2 (If_i (x6 = 3) x3 x4))))) 4 = x4 (proof)
Known 0f549..^In_0_6 : In 0 6
Theorem 1d767..^tuple_6_0_eq : ∀ x0 x1 x2 x3 x4 x5 . ap (lam 6 (λ x7 . If_i (x7 = 0) x0 (If_i (x7 = 1) x1 (If_i (x7 = 2) x2 (If_i (x7 = 3) x3 (If_i (x7 = 4) x4 x5)))))) 0 = x0 (proof)
Known e5e7b..^In_1_6 : In 1 6
Theorem 116b4..^tuple_6_1_eq : ∀ x0 x1 x2 x3 x4 x5 . ap (lam 6 (λ x7 . If_i (x7 = 0) x0 (If_i (x7 = 1) x1 (If_i (x7 = 2) x2 (If_i (x7 = 3) x3 (If_i (x7 = 4) x4 x5)))))) 1 = x1 (proof)
Known c6359..^In_2_6 : In 2 6
Theorem d72fb..^tuple_6_2_eq : ∀ x0 x1 x2 x3 x4 x5 . ap (lam 6 (λ x7 . If_i (x7 = 0) x0 (If_i (x7 = 1) x1 (If_i (x7 = 2) x2 (If_i (x7 = 3) x3 (If_i (x7 = 4) x4 x5)))))) 2 = x2 (proof)
Known d5bd4..^In_3_6 : In 3 6
Theorem f0215..^tuple_6_3_eq : ∀ x0 x1 x2 x3 x4 x5 . ap (lam 6 (λ x7 . If_i (x7 = 0) x0 (If_i (x7 = 1) x1 (If_i (x7 = 2) x2 (If_i (x7 = 3) x3 (If_i (x7 = 4) x4 x5)))))) 3 = x3 (proof)
Known 99a7f..^In_4_6 : In 4 6
Theorem 5d974..^tuple_6_4_eq : ∀ x0 x1 x2 x3 x4 x5 . ap (lam 6 (λ x7 . If_i (x7 = 0) x0 (If_i (x7 = 1) x1 (If_i (x7 = 2) x2 (If_i (x7 = 3) x3 (If_i (x7 = 4) x4 x5)))))) 4 = x4 (proof)
Known ad142..^In_5_6 : In 5 6
Known 3d58e..^neq_5_0 : not (5 = 0)
Known 03b32..^neq_5_1 : not (5 = 1)
Known b24f1..^neq_5_2 : not (5 = 2)
Known ab3a6..^neq_5_3 : not (5 = 3)
Known 8140f..^neq_5_4 : not (5 = 4)
Theorem 9b8de..^tuple_6_5_eq : ∀ x0 x1 x2 x3 x4 x5 . ap (lam 6 (λ x7 . If_i (x7 = 0) x0 (If_i (x7 = 1) x1 (If_i (x7 = 2) x2 (If_i (x7 = 3) x3 (If_i (x7 = 4) x4 x5)))))) 5 = x5 (proof)
Known 6516d..^In_0_7 : In 0 7
Theorem f0beb..^tuple_7_0_eq : ∀ x0 x1 x2 x3 x4 x5 x6 . ap (lam 7 (λ x8 . If_i (x8 = 0) x0 (If_i (x8 = 1) x1 (If_i (x8 = 2) x2 (If_i (x8 = 3) x3 (If_i (x8 = 4) x4 (If_i (x8 = 5) x5 x6))))))) 0 = x0 (proof)
Known ed9ed..^In_1_7 : In 1 7
Theorem 19883..^tuple_7_1_eq : ∀ x0 x1 x2 x3 x4 x5 x6 . ap (lam 7 (λ x8 . If_i (x8 = 0) x0 (If_i (x8 = 1) x1 (If_i (x8 = 2) x2 (If_i (x8 = 3) x3 (If_i (x8 = 4) x4 (If_i (x8 = 5) x5 x6))))))) 1 = x1 (proof)
Known e6c7c..^In_2_7 : In 2 7
Theorem e20cd..^tuple_7_2_eq : ∀ x0 x1 x2 x3 x4 x5 x6 . ap (lam 7 (λ x8 . If_i (x8 = 0) x0 (If_i (x8 = 1) x1 (If_i (x8 = 2) x2 (If_i (x8 = 3) x3 (If_i (x8 = 4) x4 (If_i (x8 = 5) x5 x6))))))) 2 = x2 (proof)
Known dc43c..^In_3_7 : In 3 7
Theorem 85904..^tuple_7_3_eq : ∀ x0 x1 x2 x3 x4 x5 x6 . ap (lam 7 (λ x8 . If_i (x8 = 0) x0 (If_i (x8 = 1) x1 (If_i (x8 = 2) x2 (If_i (x8 = 3) x3 (If_i (x8 = 4) x4 (If_i (x8 = 5) x5 x6))))))) 3 = x3 (proof)
Known fb74e..^In_4_7 : In 4 7
Theorem 5a2b7..^tuple_7_4_eq : ∀ x0 x1 x2 x3 x4 x5 x6 . ap (lam 7 (λ x8 . If_i (x8 = 0) x0 (If_i (x8 = 1) x1 (If_i (x8 = 2) x2 (If_i (x8 = 3) x3 (If_i (x8 = 4) x4 (If_i (x8 = 5) x5 x6))))))) 4 = x4 (proof)
Known 59629..^In_5_7 : In 5 7
Theorem 07dc0..^tuple_7_5_eq : ∀ x0 x1 x2 x3 x4 x5 x6 . ap (lam 7 (λ x8 . If_i (x8 = 0) x0 (If_i (x8 = 1) x1 (If_i (x8 = 2) x2 (If_i (x8 = 3) x3 (If_i (x8 = 4) x4 (If_i (x8 = 5) x5 x6))))))) 5 = x5 (proof)
Known 14a1c..^In_6_7 : In 6 7
Known 4193c..^neq_6_0 : not (6 = 0)
Known 53f92..^neq_6_1 : not (6 = 1)
Known f4b9c..^neq_6_2 : not (6 = 2)
Known 96787..^neq_6_3 : not (6 = 3)
Known 2a680..^neq_6_4 : not (6 = 4)
Known 3a5c9..^neq_6_5 : not (6 = 5)
Theorem 37a40..^tuple_7_6_eq : ∀ x0 x1 x2 x3 x4 x5 x6 . ap (lam 7 (λ x8 . If_i (x8 = 0) x0 (If_i (x8 = 1) x1 (If_i (x8 = 2) x2 (If_i (x8 = 3) x3 (If_i (x8 = 4) x4 (If_i (x8 = 5) x5 x6))))))) 6 = x6 (proof)
Known 57d5b..^In_0_8 : In 0 8
Theorem 0e230..^tuple_8_0_eq : ∀ x0 x1 x2 x3 x4 x5 x6 x7 . ap (lam 8 (λ x9 . If_i (x9 = 0) x0 (If_i (x9 = 1) x1 (If_i (x9 = 2) x2 (If_i (x9 = 3) x3 (If_i (x9 = 4) x4 (If_i (x9 = 5) x5 (If_i (x9 = 6) x6 x7)))))))) 0 = x0 (proof)
Known 4c0a3..^In_1_8 : In 1 8
Theorem c92ea..^tuple_8_1_eq : ∀ x0 x1 x2 x3 x4 x5 x6 x7 . ap (lam 8 (λ x9 . If_i (x9 = 0) x0 (If_i (x9 = 1) x1 (If_i (x9 = 2) x2 (If_i (x9 = 3) x3 (If_i (x9 = 4) x4 (If_i (x9 = 5) x5 (If_i (x9 = 6) x6 x7)))))))) 1 = x1 (proof)
Known b8348..^In_2_8 : In 2 8
Theorem bb098..^tuple_8_2_eq : ∀ x0 x1 x2 x3 x4 x5 x6 x7 . ap (lam 8 (λ x9 . If_i (x9 = 0) x0 (If_i (x9 = 1) x1 (If_i (x9 = 2) x2 (If_i (x9 = 3) x3 (If_i (x9 = 4) x4 (If_i (x9 = 5) x5 (If_i (x9 = 6) x6 x7)))))))) 2 = x2 (proof)
Known ace10..^In_3_8 : In 3 8
Theorem b932d..^tuple_8_3_eq : ∀ x0 x1 x2 x3 x4 x5 x6 x7 . ap (lam 8 (λ x9 . If_i (x9 = 0) x0 (If_i (x9 = 1) x1 (If_i (x9 = 2) x2 (If_i (x9 = 3) x3 (If_i (x9 = 4) x4 (If_i (x9 = 5) x5 (If_i (x9 = 6) x6 x7)))))))) 3 = x3 (proof)
Known e08a8..^In_4_8 : In 4 8
Theorem 34a8e..^tuple_8_4_eq : ∀ x0 x1 x2 x3 x4 x5 x6 x7 . ap (lam 8 (λ x9 . If_i (x9 = 0) x0 (If_i (x9 = 1) x1 (If_i (x9 = 2) x2 (If_i (x9 = 3) x3 (If_i (x9 = 4) x4 (If_i (x9 = 5) x5 (If_i (x9 = 6) x6 x7)))))))) 4 = x4 (proof)
Known 9ad9e..^In_5_8 : In 5 8
Theorem 721fb..^tuple_8_5_eq : ∀ x0 x1 x2 x3 x4 x5 x6 x7 . ap (lam 8 (λ x9 . If_i (x9 = 0) x0 (If_i (x9 = 1) x1 (If_i (x9 = 2) x2 (If_i (x9 = 3) x3 (If_i (x9 = 4) x4 (If_i (x9 = 5) x5 (If_i (x9 = 6) x6 x7)))))))) 5 = x5 (proof)
Known e821f..^In_6_8 : In 6 8
Theorem 8bc91..^tuple_8_6_eq : ∀ x0 x1 x2 x3 x4 x5 x6 x7 . ap (lam 8 (λ x9 . If_i (x9 = 0) x0 (If_i (x9 = 1) x1 (If_i (x9 = 2) x2 (If_i (x9 = 3) x3 (If_i (x9 = 4) x4 (If_i (x9 = 5) x5 (If_i (x9 = 6) x6 x7)))))))) 6 = x6 (proof)
Known 879be..^In_7_8 : In 7 8
Known ca789..^neq_7_0 : not (7 = 0)
Known 6a87a..^neq_7_1 : not (7 = 1)
Known 46692..^neq_7_2 : not (7 = 2)
Known c0553..^neq_7_3 : not (7 = 3)
Known 21c2e..^neq_7_4 : not (7 = 4)
Known fdff8..^neq_7_5 : not (7 = 5)
Known 0a1a6..^neq_7_6 : not (7 = 6)
Theorem c9eee..^tuple_8_7_eq : ∀ x0 x1 x2 x3 x4 x5 x6 x7 . ap (lam 8 (λ x9 . If_i (x9 = 0) x0 (If_i (x9 = 1) x1 (If_i (x9 = 2) x2 (If_i (x9 = 3) x3 (If_i (x9 = 4) x4 (If_i (x9 = 5) x5 (If_i (x9 = 6) x6 x7)))))))) 7 = x7 (proof)
Known fda50..^In_0_9 : In 0 9
Theorem 9110d..^tuple_9_0_eq : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 . ap (lam 9 (λ x10 . If_i (x10 = 0) x0 (If_i (x10 = 1) x1 (If_i (x10 = 2) x2 (If_i (x10 = 3) x3 (If_i (x10 = 4) x4 (If_i (x10 = 5) x5 (If_i (x10 = 6) x6 (If_i (x10 = 7) x7 x8))))))))) 0 = x0 (proof)
Known 9744a..^In_1_9 : In 1 9
Theorem ecdb1..^tuple_9_1_eq : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 . ap (lam 9 (λ x10 . If_i (x10 = 0) x0 (If_i (x10 = 1) x1 (If_i (x10 = 2) x2 (If_i (x10 = 3) x3 (If_i (x10 = 4) x4 (If_i (x10 = 5) x5 (If_i (x10 = 6) x6 (If_i (x10 = 7) x7 x8))))))))) 1 = x1 (proof)
Known 2df93..^In_2_9 : In 2 9
Theorem d8937..^tuple_9_2_eq : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 . ap (lam 9 (λ x10 . If_i (x10 = 0) x0 (If_i (x10 = 1) x1 (If_i (x10 = 2) x2 (If_i (x10 = 3) x3 (If_i (x10 = 4) x4 (If_i (x10 = 5) x5 (If_i (x10 = 6) x6 (If_i (x10 = 7) x7 x8))))))))) 2 = x2 (proof)
Known c585f..^In_3_9 : In 3 9
Theorem c1e22..^tuple_9_3_eq : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 . ap (lam 9 (λ x10 . If_i (x10 = 0) x0 (If_i (x10 = 1) x1 (If_i (x10 = 2) x2 (If_i (x10 = 3) x3 (If_i (x10 = 4) x4 (If_i (x10 = 5) x5 (If_i (x10 = 6) x6 (If_i (x10 = 7) x7 x8))))))))) 3 = x3 (proof)
Known 8ee2c..^In_4_9 : In 4 9
Theorem d7f59..^tuple_9_4_eq : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 . ap (lam 9 (λ x10 . If_i (x10 = 0) x0 (If_i (x10 = 1) x1 (If_i (x10 = 2) x2 (If_i (x10 = 3) x3 (If_i (x10 = 4) x4 (If_i (x10 = 5) x5 (If_i (x10 = 6) x6 (If_i (x10 = 7) x7 x8))))))))) 4 = x4 (proof)
Known e48d3..^In_5_9 : In 5 9
Theorem 9daae..^tuple_9_5_eq : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 . ap (lam 9 (λ x10 . If_i (x10 = 0) x0 (If_i (x10 = 1) x1 (If_i (x10 = 2) x2 (If_i (x10 = 3) x3 (If_i (x10 = 4) x4 (If_i (x10 = 5) x5 (If_i (x10 = 6) x6 (If_i (x10 = 7) x7 x8))))))))) 5 = x5 (proof)
Known 35438..^In_6_9 : In 6 9
Theorem 9fc15..^tuple_9_6_eq : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 . ap (lam 9 (λ x10 . If_i (x10 = 0) x0 (If_i (x10 = 1) x1 (If_i (x10 = 2) x2 (If_i (x10 = 3) x3 (If_i (x10 = 4) x4 (If_i (x10 = 5) x5 (If_i (x10 = 6) x6 (If_i (x10 = 7) x7 x8))))))))) 6 = x6 (proof)
Known 3f605..^In_7_9 : In 7 9
Theorem daaf4..^tuple_9_7_eq : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 . ap (lam 9 (λ x10 . If_i (x10 = 0) x0 (If_i (x10 = 1) x1 (If_i (x10 = 2) x2 (If_i (x10 = 3) x3 (If_i (x10 = 4) x4 (If_i (x10 = 5) x5 (If_i (x10 = 6) x6 (If_i (x10 = 7) x7 x8))))))))) 7 = x7 (proof)
Known dab47..^In_8_9 : In 8 9
Known c1d23..^neq_8_0 : not (8 = 0)
Known 3fd1f..^neq_8_1 : not (8 = 1)
Known 0aafe..^neq_8_2 : not (8 = 2)
Known 4862b..^neq_8_3 : not (8 = 3)
Known e99bd..^neq_8_4 : not (8 = 4)
Known c7589..^neq_8_5 : not (8 = 5)
Known 85418..^neq_8_6 : not (8 = 6)
Known 0ff51..^neq_8_7 : not (8 = 7)
Theorem 544fd..^tuple_9_8_eq : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 . ap (lam 9 (λ x10 . If_i (x10 = 0) x0 (If_i (x10 = 1) x1 (If_i (x10 = 2) x2 (If_i (x10 = 3) x3 (If_i (x10 = 4) x4 (If_i (x10 = 5) x5 (If_i (x10 = 6) x6 (If_i (x10 = 7) x7 x8))))))))) 8 = x8 (proof)
Known 2d998..^tuple_4_eta : ∀ x0 x1 x2 x3 . lam 4 (ap (lam 4 (λ x5 . If_i (x5 = 0) x0 (If_i (x5 = 1) x1 (If_i (x5 = 2) x2 x3))))) = lam 4 (λ x5 . If_i (x5 = 0) x0 (If_i (x5 = 1) x1 (If_i (x5 = 2) x2 x3)))
Known 3c3a9..^setexp_def : setexp = λ x1 x2 . Pi x2 (λ x3 . x1)
Known 25543..^lam_Pi : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . In x3 x0 ⟶ In (x2 x3) (x1 x3)) ⟶ In (lam x0 x2) (Pi x0 x1)
Known 8b3d1..^cases_4 : ∀ x0 . In x0 4 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 1 ⟶ x1 2 ⟶ x1 3 ⟶ x1 x0
Theorem 75bd6..^{tuple_4_in_A_4} : ∀ x0 x1 x2 x3 x4 . In x0 x4 ⟶ In x1 x4 ⟶ In x2 x4 ⟶ In x3 x4 ⟶ In (lam 4 (λ x5 . If_i (x5 = 0) x0 (If_i (x5 = 1) x1 (If_i (x5 = 2) x2 x3)))) (setexp x4 4) (proof)
Known 398e3..^{PigeonHole_nat_bij} : ∀ x0 . nat_p x0 ⟶ ∀ x1 : ι → ι . (∀ x2 . In x2 x0 ⟶ In (x1 x2) x0) ⟶ (∀ x2 . In x2 x0 ⟶ ∀ x3 . In x3 x0 ⟶ x1 x2 = x1 x3 ⟶ x2 = x3) ⟶ bij x0 x0 x1
Known 21479..^nat_ordsucc : ∀ x0 . nat_p x0 ⟶ nat_p (ordsucc x0)
Known 36841..^nat_2 : nat_p 2
Theorem e56d1..^{tuple_4_bij_4} : ∀ x0 x1 x2 x3 . In x0 4 ⟶ In x1 4 ⟶ In x2 4 ⟶ In x3 4 ⟶ not (x0 = x1) ⟶ not (x0 = x2) ⟶ not (x0 = x3) ⟶ not (x1 = x2) ⟶ not (x1 = x3) ⟶ not (x2 = x3) ⟶ bij 4 4 (ap (lam 4 (λ x4 . If_i (x4 = 0) x0 (If_i (x4 = 1) x1 (If_i (x4 = 2) x2 x3))))) (proof)
Known 7022c..^V__def : V_ = In_rec_poly_i (λ x1 . λ x2 : ι → ι . famunion x1 (λ x3 . Power (x2 x3)))
Known f78bc..^In_rec_i_eq : ∀ x0 : ι → (ι → ι) → ι . (∀ x1 . ∀ x2 x3 : ι → ι . (∀ x4 . In x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . In_rec_poly_i x0 x1 = x0 x1 (In_rec_poly_i x0)
Known b3824..^set_ext : ∀ x0 x1 . Subq x0 x1 ⟶ Subq x1 x0 ⟶ x0 = x1
Known b0dce..^SubqI : ∀ x0 x1 . (∀ x2 . In x2 x0 ⟶ In x2 x1) ⟶ Subq x0 x1
Known 390bb..^famunionE : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . In x2 (famunion x0 x1) ⟶ ∀ x3 : ο . (∀ x4 . and (In x4 x0) (In x2 (x1 x4)) ⟶ x3) ⟶ x3
Known andE^andE : ∀ x0 x1 : ο . and x0 x1 ⟶ ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Known 8f8c2..^famunionI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . In x2 x0 ⟶ In x3 (x1 x2) ⟶ In x3 (famunion x0 x1)
Theorem 8c6bb..^V_eq : ∀ x0 . V_ x0 = famunion x0 (λ x2 . Power (V_ x2)) (proof)
Known 2d44a..^PowerI : ∀ x0 x1 . Subq x1 x0 ⟶ In x1 (Power x0)
Theorem b5461..^V_I : ∀ x0 x1 x2 . In x1 x2 ⟶ Subq x0 (V_ x1) ⟶ In x0 (V_ x2) (proof)
Known ae89b..^PowerE : ∀ x0 x1 . In x1 (Power x0) ⟶ Subq x1 x0
Theorem 10ff6..^V_E : ∀ x0 x1 . In x0 (V_ x1) ⟶ ∀ x2 : ο . (∀ x3 . In x3 x1 ⟶ Subq x0 (V_ x3) ⟶ x2) ⟶ x2 (proof)
Known 61ad0..^In_ind : ∀ x0 : ι → ο . (∀ x1 . (∀ x2 . In x2 x1 ⟶ x0 x2) ⟶ x0 x1) ⟶ ∀ x1 . x0 x1
Theorem 081f3..^V_Subq : ∀ x0 . Subq x0 (V_ x0) (proof)
Known 2ad64..^Subq_tra : ∀ x0 x1 x2 . Subq x0 x1 ⟶ Subq x1 x2 ⟶ Subq x0 x2
Known 367e6..^SubqE : ∀ x0 x1 . Subq x0 x1 ⟶ ∀ x2 . In x2 x0 ⟶ In x2 x1
Theorem 212d0..^V_Subq_2 : ∀ x0 x1 . Subq x0 (V_ x1) ⟶ Subq (V_ x0) (V_ x1) (proof)
Theorem d7210..^V_In : ∀ x0 x1 . In x0 (V_ x1) ⟶ In (V_ x0) (V_ x1) (proof)
Known 3ab01..^xmcases_In : ∀ x0 x1 . ∀ x2 : ο . (In x0 x1 ⟶ x2) ⟶ (nIn x0 x1 ⟶ x2) ⟶ x2
Known dcbd9..^orIL : ∀ x0 x1 : ο . x0 ⟶ or x0 x1
Known eca40..^orIR : ∀ x0 x1 : ο . x1 ⟶ or x0 x1
Known 37124..^orE : ∀ x0 x1 : ο . or x0 x1 ⟶ ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known b4782..^contra : ∀ x0 : ο . (not x0 ⟶ False) ⟶ x0
Known 085e3..^contra_In : ∀ x0 x1 . (nIn x0 x1 ⟶ False) ⟶ In x0 x1
Known 7c02f..^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Theorem a0b35..^V_In_or_Subq : ∀ x0 x1 . or (In x0 (V_ x1)) (Subq (V_ x1) (V_ x0)) (proof)
Theorem f325d..^{V_In_or_Subq_2} : ∀ x0 x1 . or (In (V_ x0) (V_ x1)) (Subq (V_ x1) (V_ x0)) (proof)
Known 32c82..^iffI : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (x1 ⟶ x0) ⟶ iff x0 x1
Theorem 7b4cf..^iff_refl : ∀ x0 : ο . iff x0 x0 (proof)
Known 13bcd..^iff_def : iff = λ x1 x2 : ο . and (x1 ⟶ x2) (x2 ⟶ x1)
Theorem 3d208..^iff_sym : ∀ x0 x1 : ο . iff x0 x1 ⟶ iff x1 x0 (proof)
Theorem aced5..^iff_trans : ∀ x0 x1 x2 : ο . iff x0 x1 ⟶ iff x1 x2 ⟶ iff x0 x2 (proof)
Known 56b90..^PNoEq__def : PNoEq_ = λ x1 . λ x2 x3 : ι → ο . ∀ x4 . In x4 x1 ⟶ iff (x2 x4) (x3 x4)
Theorem 5d346..^PNoEq_ref_ : ∀ x0 . ∀ x1 : ι → ο . PNoEq_ x0 x1 x1 (proof)
Theorem b96d4..^PNoEq_sym_ : ∀ x0 . ∀ x1 x2 : ι → ο . PNoEq_ x0 x1 x2 ⟶ PNoEq_ x0 x2 x1 (proof)
Theorem f3029..^PNoEq_tra_ : ∀ x0 . ∀ x1 x2 x3 : ι → ο . PNoEq_ x0 x1 x2 ⟶ PNoEq_ x0 x2 x3 ⟶ PNoEq_ x0 x1 x3 (proof)
Known 1cf88..^{ordinal_TransSet_b} : ∀ x0 . ordinal x0 ⟶ ∀ x1 . In x1 x0 ⟶ ∀ x2 . In x2 x1 ⟶ In x2 x0
Theorem d26f4..^{PNoEq_antimon_} : ∀ x0 x1 : ι → ο . ∀ x2 . ordinal x2 ⟶ ∀ x3 . In x3 x2 ⟶ PNoEq_ x2 x0 x1 ⟶ PNoEq_ x3 x0 x1 (proof)
Known aebc2..^PNoLt__def : PNoLt_ = λ x1 . λ x2 x3 : ι → ο . ∀ x4 : ο . (∀ x5 . and (In x5 x1) (and (and (PNoEq_ x5 x2 x3) (not (x2 x5))) (x3 x5)) ⟶ x4) ⟶ x4
Known cd094..^and3E : ∀ x0 x1 x2 : ο . and (and x0 x1) x2 ⟶ ∀ x3 : ο . (x0 ⟶ x1 ⟶ x2 ⟶ x3) ⟶ x3
Theorem 44198..^PNoLt_E_ : ∀ x0 . ∀ x1 x2 : ι → ο . PNoLt_ x0 x1 x2 ⟶ ∀ x3 : ο . (∀ x4 . In x4 x0 ⟶ PNoEq_ x4 x1 x2 ⟶ not (x1 x4) ⟶ x2 x4 ⟶ x3) ⟶ x3 (proof)
Known 8106d..^notI : ∀ x0 : ο . (x0 ⟶ False) ⟶ not x0
Theorem 8b025..^PNoLt_irref_ : ∀ x0 . ∀ x1 : ι → ο . not (PNoLt_ x0 x1 x1) (proof)
Theorem f2efd..^{PNoLt_irref__b} : ∀ x0 . ∀ x1 : ι → ο . PNoLt_ x0 x1 x1 ⟶ False (proof)
Theorem 527c6..^PNoLt_mon_ : ∀ x0 x1 : ι → ο . ∀ x2 . ordinal x2 ⟶ ∀ x3 . In x3 x2 ⟶ PNoLt_ x3 x0 x1 ⟶ PNoLt_ x2 x0 x1 (proof)
Theorem 5f823..^{not_ex_all_demorgan_i} : ∀ x0 : ι → ο . not (∀ x1 : ο . (∀ x2 . x0 x2 ⟶ x1) ⟶ x1) ⟶ ∀ x1 . not (x0 x1) (proof)
Theorem fcbcf..^{not_all_ex_demorgan_i} : ∀ x0 : ι → ο . not (∀ x1 . x0 x1) ⟶ ∀ x1 : ο . (∀ x2 . not (x0 x2) ⟶ x1) ⟶ x1 (proof)
Known 68454..^ordinal_ind : ∀ x0 : ι → ο . (∀ x1 . ordinal x1 ⟶ (∀ x2 . In x2 x1 ⟶ x0 x2) ⟶ x0 x1) ⟶ ∀ x1 . ordinal x1 ⟶ x0 x1
Known 47706..^xmcases : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (not x0 ⟶ x1) ⟶ x1
Known 8cb38..^or3E : ∀ x0 x1 x2 : ο . or (or x0 x1) x2 ⟶ ∀ x3 : ο . (x0 ⟶ x3) ⟶ (x1 ⟶ x3) ⟶ (x2 ⟶ x3) ⟶ x3
Known f6404..^and3I : ∀ x0 x1 x2 : ο . x0 ⟶ x1 ⟶ x2 ⟶ and (and x0 x1) x2
Theorem 68860..^{PNoLt_trichotomy_or_} : ∀ x0 x1 : ι → ο . ∀ x2 . ordinal x2 ⟶ or (or (PNoLt_ x2 x0 x1) (PNoEq_ x2 x0 x1)) (PNoLt_ x2 x1 x0) (proof)
Theorem d37fd..^{PNoLt_trichotomy_or__impred} : ∀ x0 x1 : ι → ο . ∀ x2 . ordinal x2 ⟶ ∀ x3 : ο . (PNoLt_ x2 x0 x1 ⟶ x3) ⟶ (PNoEq_ x2 x0 x1 ⟶ x3) ⟶ (PNoLt_ x2 x1 x0 ⟶ x3) ⟶ x3 (proof)
Known 42117..^{ordinal_trichotomy_or_impred} : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ ∀ x2 : ο . (In x0 x1 ⟶ x2) ⟶ (x0 = x1 ⟶ x2) ⟶ (In x1 x0 ⟶ x2) ⟶ x2
Known 50594..^iffEL : ∀ x0 x1 : ο . iff x0 x1 ⟶ x0 ⟶ x1
Known 14977..^{ordinal_Hered} : ∀ x0 . ordinal x0 ⟶ ∀ x1 . In x1 x0 ⟶ ordinal x1
Theorem d2d81..^PNoLt_tra_ : ∀ x0 . ordinal x0 ⟶ ∀ x1 x2 x3 : ι → ο . PNoLt_ x0 x1 x2 ⟶ PNoLt_ x0 x2 x3 ⟶ PNoLt_ x0 x1 x3 (proof)
Known 60e7a..^PNoLt_def : PNoLt = λ x1 . λ x2 : ι → ο . λ x3 . λ x4 : ι → ο . or (or (PNoLt_ (binintersect x1 x3) x2 x4) (and (and (In x1 x3) (PNoEq_ x1 x2 x4)) (x4 x1))) (and (and (In x3 x1) (PNoEq_ x3 x2 x4)) (not (x2 x3)))
Known cb243..^or3I1 : ∀ x0 x1 x2 : ο . x0 ⟶ or (or x0 x1) x2
Theorem 0851f..^PNoLtI1 : ∀ x0 x1 . ∀ x2 x3 : ι → ο . PNoLt_ (binintersect x0 x1) x2 x3 ⟶ PNoLt x0 x2 x1 x3 (proof)
Known 8aff3..^or3I2 : ∀ x0 x1 x2 : ο . x1 ⟶ or (or x0 x1) x2
Theorem 67fa1..^PNoLtI2 : ∀ x0 x1 . ∀ x2 x3 : ι → ο . In x0 x1 ⟶ PNoEq_ x0 x2 x3 ⟶ x3 x0 ⟶ PNoLt x0 x2 x1 x3 (proof)
Known a4277..^or3I3 : ∀ x0 x1 x2 : ο . x2 ⟶ or (or x0 x1) x2
Theorem ae95b..^PNoLtI3 : ∀ x0 x1 . ∀ x2 x3 : ι → ο . In x1 x0 ⟶ PNoEq_ x1 x2 x3 ⟶ not (x2 x1) ⟶ PNoLt x0 x2 x1 x3 (proof)
Theorem e0ec6..^PNoLtE : ∀ x0 x1 . ∀ x2 x3 : ι → ο . PNoLt x0 x2 x1 x3 ⟶ ∀ x4 : ο . (PNoLt_ (binintersect x0 x1) x2 x3 ⟶ x4) ⟶ (In x0 x1 ⟶ PNoEq_ x0 x2 x3 ⟶ x3 x0 ⟶ x4) ⟶ (In x1 x0 ⟶ PNoEq_ x1 x2 x3 ⟶ not (x2 x1) ⟶ x4) ⟶ x4 (proof)
Known 8ca5a..^{binintersect_idem} : ∀ x0 . binintersect x0 x0 = x0
Theorem 2e96e..^PNoLtE2 : ∀ x0 . ∀ x1 x2 : ι → ο . PNoLt x0 x1 x0 x2 ⟶ PNoLt_ x0 x1 x2 (proof)
Theorem 96df0..^PNoLt_irref : ∀ x0 . ∀ x1 : ι → ο . not (PNoLt x0 x1 x0 x1) (proof)
Theorem 289e1..^{PNoLt_irref_b} : ∀ x0 . ∀ x1 : ι → ο . PNoLt x0 x1 x0 x1 ⟶ False (proof)
Known 485cd..^{binintersect_Subq_eq_1} : ∀ x0 x1 . Subq x0 x1 ⟶ binintersect x0 x1 = x0
Known 6696a..^Subq_ref : ∀ x0 . Subq x0 x0
Known 6b560..^{binintersect_com} : ∀ x0 x1 . binintersect x0 x1 = binintersect x1 x0
Known 4ebb9..^{ordinal_binintersect} : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ ordinal (binintersect x0 x1)
Known 5f38d..^TransSet_def : TransSet = λ x1 . ∀ x2 . In x2 x1 ⟶ Subq x2 x1
Known 339db..^{ordinal_TransSet} : ∀ x0 . ordinal x0 ⟶ TransSet x0
Theorem 7adfb..^{PNoLt_trichotomy_or} : ∀ x0 x1 . ∀ x2 x3 : ι → ο . ordinal x0 ⟶ ordinal x1 ⟶ or (or (PNoLt x0 x2 x1 x3) (and (x0 = x1) (PNoEq_ x0 x2 x3))) (PNoLt x1 x3 x0 x2) (proof)
Known 9c451..^{binintersectE_impred} : ∀ x0 x1 x2 . In x2 (binintersect x0 x1) ⟶ ∀ x3 : ο . (In x2 x0 ⟶ In x2 x1 ⟶ x3) ⟶ x3
Theorem 76102..^PNoLtEq_tra : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ ∀ x2 x3 x4 : ι → ο . PNoLt x0 x2 x1 x3 ⟶ PNoEq_ x1 x3 x4 ⟶ PNoLt x0 x2 x1 x4 (proof)
Theorem 492f5..^PNoEqLt_tra : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ ∀ x2 x3 x4 : ι → ο . PNoEq_ x0 x2 x3 ⟶ PNoLt x0 x3 x1 x4 ⟶ PNoLt x0 x2 x1 x4 (proof)
Known dd25c..^{binintersectI} : ∀ x0 x1 x2 . In x2 x0 ⟶ In x2 x1 ⟶ In x2 (binintersect x0 x1)
Theorem a6669..^PNoLt_tra : ∀ x0 x1 x2 . ordinal x0 ⟶ ordinal x1 ⟶ ordinal x2 ⟶ ∀ x3 x4 x5 : ι → ο . PNoLt x0 x3 x1 x4 ⟶ PNoLt x1 x4 x2 x5 ⟶ PNoLt x0 x3 x2 x5 (proof)
Known 37ff8..^PNoLe_def : PNoLe = λ x1 . λ x2 : ι → ο . λ x3 . λ x4 : ι → ο . or (PNoLt x1 x2 x3 x4) (and (x1 = x3) (PNoEq_ x1 x2 x4))
Theorem 478b3..^PNoLeI1 : ∀ x0 x1 . ∀ x2 x3 : ι → ο . PNoLt x0 x2 x1 x3 ⟶ PNoLe x0 x2 x1 x3 (proof)
Theorem 13ed3..^PNoLeI2 : ∀ x0 . ∀ x1 x2 : ι → ο . PNoEq_ x0 x1 x2 ⟶ PNoLe x0 x1 x0 x2 (proof)
Theorem 806be..^PNoLeE : ∀ x0 x1 . ∀ x2 x3 : ι → ο . PNoLe x0 x2 x1 x3 ⟶ ∀ x4 : ο . (PNoLt x0 x2 x1 x3 ⟶ x4) ⟶ (x0 = x1 ⟶ PNoEq_ x0 x2 x3 ⟶ x4) ⟶ x4 (proof)
Theorem ae672..^PNoLe_ref : ∀ x0 . ∀ x1 : ι → ο . PNoLe x0 x1 x0 x1 (proof)
Theorem 22e4a..^{PNoLe_antisym} : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ ∀ x2 x3 : ι → ο . PNoLe x0 x2 x1 x3 ⟶ PNoLe x1 x3 x0 x2 ⟶ and (x0 = x1) (PNoEq_ x0 x2 x3) (proof)
Theorem d0c10..^PNoLtLe_tra : ∀ x0 x1 x2 . ordinal x0 ⟶ ordinal x1 ⟶ ordinal x2 ⟶ ∀ x3 x4 x5 : ι → ο . PNoLt x0 x3 x1 x4 ⟶ PNoLe x1 x4 x2 x5 ⟶ PNoLt x0 x3 x2 x5 (proof)
Theorem 3c4f3..^PNoLeLt_tra : ∀ x0 x1 x2 . ordinal x0 ⟶ ordinal x1 ⟶ ordinal x2 ⟶ ∀ x3 x4 x5 : ι → ο . PNoLe x0 x3 x1 x4 ⟶ PNoLt x1 x4 x2 x5 ⟶ PNoLt x0 x3 x2 x5 (proof)
Theorem 3bb25..^PNoEqLe_tra : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ ∀ x2 x3 x4 : ι → ο . PNoEq_ x0 x2 x3 ⟶ PNoLe x0 x3 x1 x4 ⟶ PNoLe x0 x2 x1 x4 (proof)
Theorem 3a240..^PNoLeEq_tra : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ ∀ x2 x3 x4 : ι → ο . PNoLe x0 x2 x1 x3 ⟶ PNoEq_ x1 x3 x4 ⟶ PNoLe x0 x2 x1 x4 (proof)
Theorem e23c1..^PNoLe_tra : ∀ x0 x1 x2 . ordinal x0 ⟶ ordinal x1 ⟶ ordinal x2 ⟶ ∀ x3 x4 x5 : ι → ο . PNoLe x0 x3 x1 x4 ⟶ PNoLe x1 x4 x2 x5 ⟶ PNoLe x0 x3 x2 x5 (proof)