Theorem alephiso2

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	alephiso2	⊢ ℵ Isom E , ≺ ( On , { 𝑥 ∈ ran card ∣ ω ⊆ 𝑥 } )

Proof

Step	Hyp	Ref	Expression
1		alephiso	⊢ ℵ Isom E , E ( On , { 𝑥 ∣ ( ω ⊆ 𝑥 ∧ ( card ‘ 𝑥 ) = 𝑥 ) } )
2		iscard4	⊢ ( ( card ‘ 𝑥 ) = 𝑥 ↔ 𝑥 ∈ ran card )
3	2	anbi1ci	⊢ ( ( ω ⊆ 𝑥 ∧ ( card ‘ 𝑥 ) = 𝑥 ) ↔ ( 𝑥 ∈ ran card ∧ ω ⊆ 𝑥 ) )
4	3	abbii	⊢ { 𝑥 ∣ ( ω ⊆ 𝑥 ∧ ( card ‘ 𝑥 ) = 𝑥 ) } = { 𝑥 ∣ ( 𝑥 ∈ ran card ∧ ω ⊆ 𝑥 ) }
5		df-rab	⊢ { 𝑥 ∈ ran card ∣ ω ⊆ 𝑥 } = { 𝑥 ∣ ( 𝑥 ∈ ran card ∧ ω ⊆ 𝑥 ) }
6	4 5	eqtr4i	⊢ { 𝑥 ∣ ( ω ⊆ 𝑥 ∧ ( card ‘ 𝑥 ) = 𝑥 ) } = { 𝑥 ∈ ran card ∣ ω ⊆ 𝑥 }
7		f1oeq3	⊢ ( { 𝑥 ∣ ( ω ⊆ 𝑥 ∧ ( card ‘ 𝑥 ) = 𝑥 ) } = { 𝑥 ∈ ran card ∣ ω ⊆ 𝑥 } → ( ℵ : On –1-1-onto→ { 𝑥 ∣ ( ω ⊆ 𝑥 ∧ ( card ‘ 𝑥 ) = 𝑥 ) } ↔ ℵ : On –1-1-onto→ { 𝑥 ∈ ran card ∣ ω ⊆ 𝑥 } ) )
8	6 7	ax-mp	⊢ ( ℵ : On –1-1-onto→ { 𝑥 ∣ ( ω ⊆ 𝑥 ∧ ( card ‘ 𝑥 ) = 𝑥 ) } ↔ ℵ : On –1-1-onto→ { 𝑥 ∈ ran card ∣ ω ⊆ 𝑥 } )
9		alephon	⊢ ( ℵ ‘ 𝑧 ) ∈ On
10		epelg	⊢ ( ( ℵ ‘ 𝑧 ) ∈ On → ( ( ℵ ‘ 𝑦 ) E ( ℵ ‘ 𝑧 ) ↔ ( ℵ ‘ 𝑦 ) ∈ ( ℵ ‘ 𝑧 ) ) )
11	9 10	mp1i	⊢ ( ( 𝑦 ∈ On ∧ 𝑧 ∈ On ) → ( ( ℵ ‘ 𝑦 ) E ( ℵ ‘ 𝑧 ) ↔ ( ℵ ‘ 𝑦 ) ∈ ( ℵ ‘ 𝑧 ) ) )
12		alephord2	⊢ ( ( 𝑦 ∈ On ∧ 𝑧 ∈ On ) → ( 𝑦 ∈ 𝑧 ↔ ( ℵ ‘ 𝑦 ) ∈ ( ℵ ‘ 𝑧 ) ) )
13		alephord	⊢ ( ( 𝑦 ∈ On ∧ 𝑧 ∈ On ) → ( 𝑦 ∈ 𝑧 ↔ ( ℵ ‘ 𝑦 ) ≺ ( ℵ ‘ 𝑧 ) ) )
14	11 12 13	3bitr2d	⊢ ( ( 𝑦 ∈ On ∧ 𝑧 ∈ On ) → ( ( ℵ ‘ 𝑦 ) E ( ℵ ‘ 𝑧 ) ↔ ( ℵ ‘ 𝑦 ) ≺ ( ℵ ‘ 𝑧 ) ) )
15	14	bibi2d	⊢ ( ( 𝑦 ∈ On ∧ 𝑧 ∈ On ) → ( ( 𝑦 E 𝑧 ↔ ( ℵ ‘ 𝑦 ) E ( ℵ ‘ 𝑧 ) ) ↔ ( 𝑦 E 𝑧 ↔ ( ℵ ‘ 𝑦 ) ≺ ( ℵ ‘ 𝑧 ) ) ) )
16	15	ralbidva	⊢ ( 𝑦 ∈ On → ( ∀ 𝑧 ∈ On ( 𝑦 E 𝑧 ↔ ( ℵ ‘ 𝑦 ) E ( ℵ ‘ 𝑧 ) ) ↔ ∀ 𝑧 ∈ On ( 𝑦 E 𝑧 ↔ ( ℵ ‘ 𝑦 ) ≺ ( ℵ ‘ 𝑧 ) ) ) )
17	16	ralbiia	⊢ ( ∀ 𝑦 ∈ On ∀ 𝑧 ∈ On ( 𝑦 E 𝑧 ↔ ( ℵ ‘ 𝑦 ) E ( ℵ ‘ 𝑧 ) ) ↔ ∀ 𝑦 ∈ On ∀ 𝑧 ∈ On ( 𝑦 E 𝑧 ↔ ( ℵ ‘ 𝑦 ) ≺ ( ℵ ‘ 𝑧 ) ) )
18	8 17	anbi12i	⊢ ( ( ℵ : On –1-1-onto→ { 𝑥 ∣ ( ω ⊆ 𝑥 ∧ ( card ‘ 𝑥 ) = 𝑥 ) } ∧ ∀ 𝑦 ∈ On ∀ 𝑧 ∈ On ( 𝑦 E 𝑧 ↔ ( ℵ ‘ 𝑦 ) E ( ℵ ‘ 𝑧 ) ) ) ↔ ( ℵ : On –1-1-onto→ { 𝑥 ∈ ran card ∣ ω ⊆ 𝑥 } ∧ ∀ 𝑦 ∈ On ∀ 𝑧 ∈ On ( 𝑦 E 𝑧 ↔ ( ℵ ‘ 𝑦 ) ≺ ( ℵ ‘ 𝑧 ) ) ) )
19		df-isom	⊢ ( ℵ Isom E , E ( On , { 𝑥 ∣ ( ω ⊆ 𝑥 ∧ ( card ‘ 𝑥 ) = 𝑥 ) } ) ↔ ( ℵ : On –1-1-onto→ { 𝑥 ∣ ( ω ⊆ 𝑥 ∧ ( card ‘ 𝑥 ) = 𝑥 ) } ∧ ∀ 𝑦 ∈ On ∀ 𝑧 ∈ On ( 𝑦 E 𝑧 ↔ ( ℵ ‘ 𝑦 ) E ( ℵ ‘ 𝑧 ) ) ) )
20		df-isom	⊢ ( ℵ Isom E , ≺ ( On , { 𝑥 ∈ ran card ∣ ω ⊆ 𝑥 } ) ↔ ( ℵ : On –1-1-onto→ { 𝑥 ∈ ran card ∣ ω ⊆ 𝑥 } ∧ ∀ 𝑦 ∈ On ∀ 𝑧 ∈ On ( 𝑦 E 𝑧 ↔ ( ℵ ‘ 𝑦 ) ≺ ( ℵ ‘ 𝑧 ) ) ) )
21	18 19 20	3bitr4i	⊢ ( ℵ Isom E , E ( On , { 𝑥 ∣ ( ω ⊆ 𝑥 ∧ ( card ‘ 𝑥 ) = 𝑥 ) } ) ↔ ℵ Isom E , ≺ ( On , { 𝑥 ∈ ran card ∣ ω ⊆ 𝑥 } ) )
22	1 21	mpbi	⊢ ℵ Isom E , ≺ ( On , { 𝑥 ∈ ran card ∣ ω ⊆ 𝑥 } )