Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  iscard2 Structured version   Visualization version   Unicode version

Theorem iscard2 8428
 Description: Two ways to express the property of being a cardinal number. Definition 8 of [Suppes] p. 225. (Contributed by Mario Carneiro, 15-Jan-2013.)
Assertion
Ref Expression
iscard2
Distinct variable group:   ,

Proof of Theorem iscard2
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 cardon 8396 . . 3
2 eleq1 2537 . . 3
31, 2mpbii 216 . 2
4 cardonle 8409 . . . . . 6
54biantrurd 516 . . . . 5
6 eqss 3433 . . . . 5
75, 6syl6rbbr 272 . . . 4
8 oncardval 8407 . . . . 5
98sseq2d 3446 . . . 4
107, 9bitrd 261 . . 3
11 ssint 4242 . . . 4
12 breq1 4398 . . . . . . . . 9
1312elrab 3184 . . . . . . . 8
14 ensymb 7635 . . . . . . . . 9
1514anbi2i 708 . . . . . . . 8
1613, 15bitri 257 . . . . . . 7
1716imbi1i 332 . . . . . 6
18 impexp 453 . . . . . 6
1917, 18bitri 257 . . . . 5
2019ralbii2 2821 . . . 4
2111, 20bitri 257 . . 3
2210, 21syl6bb 269 . 2