New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  0lt1c GIF version

Theorem 0lt1c 6258
 Description: Cardinal one is strictly greater than cardinal zero. (Contributed by Scott Fenton, 1-Aug-2019.)
Assertion
Ref Expression
0lt1c 0c <c 1c

Proof of Theorem 0lt1c
StepHypRef Expression
1 df0c2 6137 . . . 4 0c = Nc
2 0ss 3579 . . . . 5 {x}
3 0ex 4110 . . . . . 6 V
4 snex 4111 . . . . . 6 {x} V
53, 4nclec 6195 . . . . 5 ( {x} → Nc c Nc {x})
62, 5ax-mp 8 . . . 4 Nc c Nc {x}
71, 6eqbrtri 4658 . . 3 0cc Nc {x}
8 vex 2862 . . . . . . 7 x V
98snnz 3834 . . . . . 6 {x} ≠
10 df-ne 2518 . . . . . 6 ({x} ≠ ↔ ¬ {x} = )
119, 10mpbi 199 . . . . 5 ¬ {x} =
124ncid 6123 . . . . . . 7 {x} Nc {x}
13 eleq2 2414 . . . . . . 7 (0c = Nc {x} → ({x} 0c ↔ {x} Nc {x}))
1412, 13mpbiri 224 . . . . . 6 (0c = Nc {x} → {x} 0c)
15 el0c 4421 . . . . . 6 ({x} 0c ↔ {x} = )
1614, 15sylib 188 . . . . 5 (0c = Nc {x} → {x} = )
1711, 16mto 167 . . . 4 ¬ 0c = Nc {x}
18 df-ne 2518 . . . 4 (0cNc {x} ↔ ¬ 0c = Nc {x})
1917, 18mpbir 200 . . 3 0cNc {x}
20 brltc 6114 . . 3 (0c <c Nc {x} ↔ (0cc Nc {x} 0cNc {x}))
217, 19, 20mpbir2an 886 . 2 0c <c Nc {x}
228df1c3 6140 . 2 1c = Nc {x}
2321, 22breqtrri 4664 1 0c <c 1c
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   = wceq 1642   ∈ wcel 1710   ≠ wne 2516   ⊆ wss 3257  ∅c0 3550  {csn 3737  1cc1c 4134  0cc0c 4374   class class class wbr 4639   ≤c clec 6089
 Copyright terms: Public domain W3C validator