Metamath Proof Explorer


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 sucelon ( 𝐴 ∈ 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 ∣ 𝑥 ≈ ( ℵ ‘ 𝐴 ) } )