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		cardonle	⊢ ( 𝐴 ∈ On → ( card ‘ 𝐴 ) ⊆ 𝐴 )
5	4	biantrurd	⊢ ( 𝐴 ∈ On → ( 𝐴 ⊆ ( card ‘ 𝐴 ) ↔ ( ( card ‘ 𝐴 ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( card ‘ 𝐴 ) ) ) )
6		eqss	⊢ ( ( card ‘ 𝐴 ) = 𝐴 ↔ ( ( card ‘ 𝐴 ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( card ‘ 𝐴 ) ) )
7	5 6	syl6rbbr	⊢ ( 𝐴 ∈ 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	syl6bb	⊢ ( 𝐴 ∈ On → ( ( card ‘ 𝐴 ) = 𝐴 ↔ ∀ 𝑥 ∈ On ( 𝐴 ≈ 𝑥 → 𝐴 ⊆ 𝑥 ) ) )
23	3 22	biadanii	⊢ ( ( card ‘ 𝐴 ) = 𝐴 ↔ ( 𝐴 ∈ On ∧ ∀ 𝑥 ∈ On ( 𝐴 ≈ 𝑥 → 𝐴 ⊆ 𝑥 ) ) )