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 ⊢ A ∈ On → ℵ ⁡ suc ⁡ A ≈ x ∈ On | x ≈ ℵ ⁡ A

Proof

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