Theorem cardalephex

Description: Every transfinite cardinal is an aleph and vice-versa. Theorem 8A(b) of Enderton p. 213 and its converse. (Contributed by NM, 5-Nov-2003)

	Ref	Expression
Assertion	cardalephex	⊢ ( ω ⊆ 𝐴 → ( ( card ‘ 𝐴 ) = 𝐴 ↔ ∃ 𝑥 ∈ On 𝐴 = ( ℵ ‘ 𝑥 ) ) )

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( ω ⊆ 𝐴 ∧ ( card ‘ 𝐴 ) = 𝐴 ) → ω ⊆ 𝐴 )
2		cardaleph	⊢ ( ( ω ⊆ 𝐴 ∧ ( card ‘ 𝐴 ) = 𝐴 ) → 𝐴 = ( ℵ ‘ ∩ { 𝑦 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑦 ) } ) )
3	2	sseq2d	⊢ ( ( ω ⊆ 𝐴 ∧ ( card ‘ 𝐴 ) = 𝐴 ) → ( ω ⊆ 𝐴 ↔ ω ⊆ ( ℵ ‘ ∩ { 𝑦 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑦 ) } ) ) )
4		alephgeom	⊢ ( ∩ { 𝑦 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑦 ) } ∈ On ↔ ω ⊆ ( ℵ ‘ ∩ { 𝑦 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑦 ) } ) )
5	3 4	bitr4di	⊢ ( ( ω ⊆ 𝐴 ∧ ( card ‘ 𝐴 ) = 𝐴 ) → ( ω ⊆ 𝐴 ↔ ∩ { 𝑦 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑦 ) } ∈ On ) )
6	1 5	mpbid	⊢ ( ( ω ⊆ 𝐴 ∧ ( card ‘ 𝐴 ) = 𝐴 ) → ∩ { 𝑦 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑦 ) } ∈ On )
7		fveq2	⊢ ( 𝑥 = ∩ { 𝑦 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑦 ) } → ( ℵ ‘ 𝑥 ) = ( ℵ ‘ ∩ { 𝑦 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑦 ) } ) )
8	7	rspceeqv	⊢ ( ( ∩ { 𝑦 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑦 ) } ∈ On ∧ 𝐴 = ( ℵ ‘ ∩ { 𝑦 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑦 ) } ) ) → ∃ 𝑥 ∈ On 𝐴 = ( ℵ ‘ 𝑥 ) )
9	6 2 8	syl2anc	⊢ ( ( ω ⊆ 𝐴 ∧ ( card ‘ 𝐴 ) = 𝐴 ) → ∃ 𝑥 ∈ On 𝐴 = ( ℵ ‘ 𝑥 ) )
10	9	ex	⊢ ( ω ⊆ 𝐴 → ( ( card ‘ 𝐴 ) = 𝐴 → ∃ 𝑥 ∈ On 𝐴 = ( ℵ ‘ 𝑥 ) ) )
11		alephcard	⊢ ( card ‘ ( ℵ ‘ 𝑥 ) ) = ( ℵ ‘ 𝑥 )
12		fveq2	⊢ ( 𝐴 = ( ℵ ‘ 𝑥 ) → ( card ‘ 𝐴 ) = ( card ‘ ( ℵ ‘ 𝑥 ) ) )
13		id	⊢ ( 𝐴 = ( ℵ ‘ 𝑥 ) → 𝐴 = ( ℵ ‘ 𝑥 ) )
14	11 12 13	3eqtr4a	⊢ ( 𝐴 = ( ℵ ‘ 𝑥 ) → ( card ‘ 𝐴 ) = 𝐴 )
15	14	rexlimivw	⊢ ( ∃ 𝑥 ∈ On 𝐴 = ( ℵ ‘ 𝑥 ) → ( card ‘ 𝐴 ) = 𝐴 )
16	10 15	impbid1	⊢ ( ω ⊆ 𝐴 → ( ( card ‘ 𝐴 ) = 𝐴 ↔ ∃ 𝑥 ∈ On 𝐴 = ( ℵ ‘ 𝑥 ) ) )