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 ‘ 𝐴 ) = 𝐴 ↔ ( 𝐴 ∈ On ∧ ∀ 𝑥 ∈ On ( 𝐴𝑥𝐴𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 cardon ( card ‘ 𝐴 ) ∈ On
2 eleq1 ( ( card ‘ 𝐴 ) = 𝐴 → ( ( card ‘ 𝐴 ) ∈ On ↔ 𝐴 ∈ On ) )
3 1 2 mpbii ( ( card ‘ 𝐴 ) = 𝐴𝐴 ∈ On )
4 eqss ( ( card ‘ 𝐴 ) = 𝐴 ↔ ( ( card ‘ 𝐴 ) ⊆ 𝐴𝐴 ⊆ ( card ‘ 𝐴 ) ) )
5 cardonle ( 𝐴 ∈ On → ( card ‘ 𝐴 ) ⊆ 𝐴 )
6 5 biantrurd ( 𝐴 ∈ On → ( 𝐴 ⊆ ( card ‘ 𝐴 ) ↔ ( ( card ‘ 𝐴 ) ⊆ 𝐴𝐴 ⊆ ( card ‘ 𝐴 ) ) ) )
7 4 6 bitr4id ( 𝐴 ∈ On → ( ( card ‘ 𝐴 ) = 𝐴𝐴 ⊆ ( card ‘ 𝐴 ) ) )
8 oncardval ( 𝐴 ∈ On → ( card ‘ 𝐴 ) = { 𝑦 ∈ On ∣ 𝑦𝐴 } )
9 8 sseq2d ( 𝐴 ∈ On → ( 𝐴 ⊆ ( card ‘ 𝐴 ) ↔ 𝐴 { 𝑦 ∈ On ∣ 𝑦𝐴 } ) )
10 7 9 bitrd ( 𝐴 ∈ On → ( ( card ‘ 𝐴 ) = 𝐴𝐴 { 𝑦 ∈ On ∣ 𝑦𝐴 } ) )
11 ssint ( 𝐴 { 𝑦 ∈ On ∣ 𝑦𝐴 } ↔ ∀ 𝑥 ∈ { 𝑦 ∈ On ∣ 𝑦𝐴 } 𝐴𝑥 )
12 breq1 ( 𝑦 = 𝑥 → ( 𝑦𝐴𝑥𝐴 ) )
13 12 elrab ( 𝑥 ∈ { 𝑦 ∈ On ∣ 𝑦𝐴 } ↔ ( 𝑥 ∈ On ∧ 𝑥𝐴 ) )
14 ensymb ( 𝑥𝐴𝐴𝑥 )
15 14 anbi2i ( ( 𝑥 ∈ On ∧ 𝑥𝐴 ) ↔ ( 𝑥 ∈ On ∧ 𝐴𝑥 ) )
16 13 15 bitri ( 𝑥 ∈ { 𝑦 ∈ On ∣ 𝑦𝐴 } ↔ ( 𝑥 ∈ On ∧ 𝐴𝑥 ) )
17 16 imbi1i ( ( 𝑥 ∈ { 𝑦 ∈ On ∣ 𝑦𝐴 } → 𝐴𝑥 ) ↔ ( ( 𝑥 ∈ On ∧ 𝐴𝑥 ) → 𝐴𝑥 ) )
18 impexp ( ( ( 𝑥 ∈ On ∧ 𝐴𝑥 ) → 𝐴𝑥 ) ↔ ( 𝑥 ∈ On → ( 𝐴𝑥𝐴𝑥 ) ) )
19 17 18 bitri ( ( 𝑥 ∈ { 𝑦 ∈ On ∣ 𝑦𝐴 } → 𝐴𝑥 ) ↔ ( 𝑥 ∈ On → ( 𝐴𝑥𝐴𝑥 ) ) )
20 19 ralbii2 ( ∀ 𝑥 ∈ { 𝑦 ∈ On ∣ 𝑦𝐴 } 𝐴𝑥 ↔ ∀ 𝑥 ∈ On ( 𝐴𝑥𝐴𝑥 ) )
21 11 20 bitri ( 𝐴 { 𝑦 ∈ On ∣ 𝑦𝐴 } ↔ ∀ 𝑥 ∈ On ( 𝐴𝑥𝐴𝑥 ) )
22 10 21 bitrdi ( 𝐴 ∈ On → ( ( card ‘ 𝐴 ) = 𝐴 ↔ ∀ 𝑥 ∈ On ( 𝐴𝑥𝐴𝑥 ) ) )
23 3 22 biadanii ( ( card ‘ 𝐴 ) = 𝐴 ↔ ( 𝐴 ∈ On ∧ ∀ 𝑥 ∈ On ( 𝐴𝑥𝐴𝑥 ) ) )