Theorem alephsuc3

Description: An alternate representation of a successor aleph. Compare alephsuc and alephsuc2 . Equality can be obtained by taking the card of the right-hand side then using alephcard and carden . (Contributed by NM, 23-Oct-2004)

	Ref	Expression
Assertion	alephsuc3	⊢ ( 𝐴 ∈ On → ( ℵ ‘ suc 𝐴 ) ≈ { 𝑥 ∈ On ∣ 𝑥 ≈ ( ℵ ‘ 𝐴 ) } )

Proof

Step	Hyp	Ref	Expression
1		alephsuc2	⊢ ( 𝐴 ∈ On → ( ℵ ‘ suc 𝐴 ) = { 𝑥 ∈ On ∣ 𝑥 ≼ ( ℵ ‘ 𝐴 ) } )
2		alephcard	⊢ ( card ‘ ( ℵ ‘ 𝐴 ) ) = ( ℵ ‘ 𝐴 )
3		alephon	⊢ ( ℵ ‘ 𝐴 ) ∈ On
4		onenon	⊢ ( ( ℵ ‘ 𝐴 ) ∈ On → ( ℵ ‘ 𝐴 ) ∈ dom card )
5	3 4	ax-mp	⊢ ( ℵ ‘ 𝐴 ) ∈ dom card
6		cardval2	⊢ ( ( ℵ ‘ 𝐴 ) ∈ dom card → ( card ‘ ( ℵ ‘ 𝐴 ) ) = { 𝑥 ∈ On ∣ 𝑥 ≺ ( ℵ ‘ 𝐴 ) } )
7	5 6	ax-mp	⊢ ( card ‘ ( ℵ ‘ 𝐴 ) ) = { 𝑥 ∈ On ∣ 𝑥 ≺ ( ℵ ‘ 𝐴 ) }
8	2 7	eqtr3i	⊢ ( ℵ ‘ 𝐴 ) = { 𝑥 ∈ On ∣ 𝑥 ≺ ( ℵ ‘ 𝐴 ) }
9	8	a1i	⊢ ( 𝐴 ∈ On → ( ℵ ‘ 𝐴 ) = { 𝑥 ∈ On ∣ 𝑥 ≺ ( ℵ ‘ 𝐴 ) } )
10	1 9	difeq12d	⊢ ( 𝐴 ∈ On → ( ( ℵ ‘ suc 𝐴 ) ∖ ( ℵ ‘ 𝐴 ) ) = ( { 𝑥 ∈ On ∣ 𝑥 ≼ ( ℵ ‘ 𝐴 ) } ∖ { 𝑥 ∈ On ∣ 𝑥 ≺ ( ℵ ‘ 𝐴 ) } ) )
11		difrab	⊢ ( { 𝑥 ∈ On ∣ 𝑥 ≼ ( ℵ ‘ 𝐴 ) } ∖ { 𝑥 ∈ On ∣ 𝑥 ≺ ( ℵ ‘ 𝐴 ) } ) = { 𝑥 ∈ On ∣ ( 𝑥 ≼ ( ℵ ‘ 𝐴 ) ∧ ¬ 𝑥 ≺ ( ℵ ‘ 𝐴 ) ) }
12		bren2	⊢ ( 𝑥 ≈ ( ℵ ‘ 𝐴 ) ↔ ( 𝑥 ≼ ( ℵ ‘ 𝐴 ) ∧ ¬ 𝑥 ≺ ( ℵ ‘ 𝐴 ) ) )
13	12	rabbii	⊢ { 𝑥 ∈ On ∣ 𝑥 ≈ ( ℵ ‘ 𝐴 ) } = { 𝑥 ∈ On ∣ ( 𝑥 ≼ ( ℵ ‘ 𝐴 ) ∧ ¬ 𝑥 ≺ ( ℵ ‘ 𝐴 ) ) }
14	11 13	eqtr4i	⊢ ( { 𝑥 ∈ On ∣ 𝑥 ≼ ( ℵ ‘ 𝐴 ) } ∖ { 𝑥 ∈ On ∣ 𝑥 ≺ ( ℵ ‘ 𝐴 ) } ) = { 𝑥 ∈ On ∣ 𝑥 ≈ ( ℵ ‘ 𝐴 ) }
15	10 14	eqtr2di	⊢ ( 𝐴 ∈ On → { 𝑥 ∈ On ∣ 𝑥 ≈ ( ℵ ‘ 𝐴 ) } = ( ( ℵ ‘ suc 𝐴 ) ∖ ( ℵ ‘ 𝐴 ) ) )
16		alephon	⊢ ( ℵ ‘ suc 𝐴 ) ∈ On
17		onenon	⊢ ( ( ℵ ‘ suc 𝐴 ) ∈ On → ( ℵ ‘ suc 𝐴 ) ∈ dom card )
18	16 17	mp1i	⊢ ( 𝐴 ∈ On → ( ℵ ‘ suc 𝐴 ) ∈ dom card )
19		onsucb	⊢ ( 𝐴 ∈ On ↔ suc 𝐴 ∈ On )
20		alephgeom	⊢ ( suc 𝐴 ∈ On ↔ ω ⊆ ( ℵ ‘ suc 𝐴 ) )
21	19 20	bitri	⊢ ( 𝐴 ∈ On ↔ ω ⊆ ( ℵ ‘ suc 𝐴 ) )
22		fvex	⊢ ( ℵ ‘ suc 𝐴 ) ∈ V
23		ssdomg	⊢ ( ( ℵ ‘ suc 𝐴 ) ∈ V → ( ω ⊆ ( ℵ ‘ suc 𝐴 ) → ω ≼ ( ℵ ‘ suc 𝐴 ) ) )
24	22 23	ax-mp	⊢ ( ω ⊆ ( ℵ ‘ suc 𝐴 ) → ω ≼ ( ℵ ‘ suc 𝐴 ) )
25	21 24	sylbi	⊢ ( 𝐴 ∈ On → ω ≼ ( ℵ ‘ suc 𝐴 ) )
26		alephordilem1	⊢ ( 𝐴 ∈ On → ( ℵ ‘ 𝐴 ) ≺ ( ℵ ‘ suc 𝐴 ) )
27		infdif	⊢ ( ( ( ℵ ‘ suc 𝐴 ) ∈ dom card ∧ ω ≼ ( ℵ ‘ suc 𝐴 ) ∧ ( ℵ ‘ 𝐴 ) ≺ ( ℵ ‘ suc 𝐴 ) ) → ( ( ℵ ‘ suc 𝐴 ) ∖ ( ℵ ‘ 𝐴 ) ) ≈ ( ℵ ‘ suc 𝐴 ) )
28	18 25 26 27	syl3anc	⊢ ( 𝐴 ∈ On → ( ( ℵ ‘ suc 𝐴 ) ∖ ( ℵ ‘ 𝐴 ) ) ≈ ( ℵ ‘ suc 𝐴 ) )
29	15 28	eqbrtrd	⊢ ( 𝐴 ∈ On → { 𝑥 ∈ On ∣ 𝑥 ≈ ( ℵ ‘ 𝐴 ) } ≈ ( ℵ ‘ suc 𝐴 ) )
30	29	ensymd	⊢ ( 𝐴 ∈ On → ( ℵ ‘ suc 𝐴 ) ≈ { 𝑥 ∈ On ∣ 𝑥 ≈ ( ℵ ‘ 𝐴 ) } )