Metamath Proof Explorer

Theorem iscard2

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)

Ref Expression
Assertion iscard2 ⊢card⁡A=A↔A∈On∧∀x∈OnA≈x→A⊆x

Proof

Step Hyp Ref Expression
1 cardon ⊢card⁡A∈On
2 eleq1 ⊢card⁡A=A→card⁡A∈On↔A∈On
3 1 2 mpbii ⊢card⁡A=A→A∈On
4 eqss ⊢card⁡A=A↔card⁡A⊆A∧A⊆card⁡A
5 cardonle ⊢A∈On→card⁡A⊆A
6 5 biantrurd ⊢A∈On→A⊆card⁡A↔card⁡A⊆A∧A⊆card⁡A
7 4 6 bitr4id ⊢A∈On→card⁡A=A↔A⊆card⁡A
8 oncardval ⊢A∈On→card⁡A=⋂y∈On|y≈A
9 8 sseq2d ⊢A∈On→A⊆card⁡A↔A⊆⋂y∈On|y≈A
10 7 9 bitrd ⊢A∈On→card⁡A=A↔A⊆⋂y∈On|y≈A
11 ssint ⊢A⊆⋂y∈On|y≈A↔∀x∈y∈On|y≈AA⊆x
12 breq1 ⊢y=x→y≈A↔x≈A
13 12 elrab ⊢x∈y∈On|y≈A↔x∈On∧x≈A
14 ensymb ⊢x≈A↔A≈x
15 14 anbi2i ⊢x∈On∧x≈A↔x∈On∧A≈x
16 13 15 bitri ⊢x∈y∈On|y≈A↔x∈On∧A≈x
17 16 imbi1i ⊢x∈y∈On|y≈A→A⊆x↔x∈On∧A≈x→A⊆x
18 impexp ⊢x∈On∧A≈x→A⊆x↔x∈On→A≈x→A⊆x
19 17 18 bitri ⊢x∈y∈On|y≈A→A⊆x↔x∈On→A≈x→A⊆x
20 19 ralbii2 ⊢∀x∈y∈On|y≈AA⊆x↔∀x∈OnA≈x→A⊆x
21 11 20 bitri ⊢A⊆⋂y∈On|y≈A↔∀x∈OnA≈x→A⊆x
22 10 21 bitrdi ⊢A∈On→card⁡A=A↔∀x∈OnA≈x→A⊆x
23 3 22 biadanii ⊢card⁡A=A↔A∈On∧∀x∈OnA≈x→A⊆x