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

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