This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐴 ≈ 𝑥 → 𝐴 ⊆ 𝑥 ) ) )