Theorem alephiso3

Description: aleph is a strictly order-preserving mapping of On onto the class of all infinite cardinal numbers. (Contributed by RP, 18-Nov-2023)

	Ref	Expression
Assertion	alephiso3	⊢ ℵ Isom E , ≺ ( On , ( ran card ∖ ω ) )

Proof

Step	Hyp	Ref	Expression
1		alephiso2	⊢ ℵ Isom E , ≺ ( On , { 𝑥 ∈ ran card ∣ ω ⊆ 𝑥 } )
2		omelon	⊢ ω ∈ On
3		elrncard	⊢ ( 𝑥 ∈ ran card ↔ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ¬ 𝑦 ≈ 𝑥 ) )
4	3	simplbi	⊢ ( 𝑥 ∈ ran card → 𝑥 ∈ On )
5		ontri1	⊢ ( ( ω ∈ On ∧ 𝑥 ∈ On ) → ( ω ⊆ 𝑥 ↔ ¬ 𝑥 ∈ ω ) )
6	2 4 5	sylancr	⊢ ( 𝑥 ∈ ran card → ( ω ⊆ 𝑥 ↔ ¬ 𝑥 ∈ ω ) )
7	6	rabbiia	⊢ { 𝑥 ∈ ran card ∣ ω ⊆ 𝑥 } = { 𝑥 ∈ ran card ∣ ¬ 𝑥 ∈ ω }
8		dfdif2	⊢ ( ran card ∖ ω ) = { 𝑥 ∈ ran card ∣ ¬ 𝑥 ∈ ω }
9	7 8	eqtr4i	⊢ { 𝑥 ∈ ran card ∣ ω ⊆ 𝑥 } = ( ran card ∖ ω )
10		isoeq5	⊢ ( { 𝑥 ∈ ran card ∣ ω ⊆ 𝑥 } = ( ran card ∖ ω ) → ( ℵ Isom E , ≺ ( On , { 𝑥 ∈ ran card ∣ ω ⊆ 𝑥 } ) ↔ ℵ Isom E , ≺ ( On , ( ran card ∖ ω ) ) ) )
11	9 10	ax-mp	⊢ ( ℵ Isom E , ≺ ( On , { 𝑥 ∈ ran card ∣ ω ⊆ 𝑥 } ) ↔ ℵ Isom E , ≺ ( On , ( ran card ∖ ω ) ) )
12	1 11	mpbi	⊢ ℵ Isom E , ≺ ( On , ( ran card ∖ ω ) )