Theorem alephiso2 39991

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

Assertion

Ref	Expression
alephiso2	⊢ ℵ Isom E , ≺ (On, {𝑥 ∈ ran card ∣ ω ⊆ 𝑥})

Proof of Theorem alephiso2

Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		alephiso 9521	. 2 ⊢ ℵ Isom E , E (On, {𝑥 ∣ (ω ⊆ 𝑥 ∧ (card‘𝑥) = 𝑥)})
2		iscard4 39974	. . . . . . . 8 ⊢ ((card‘𝑥) = 𝑥 ↔ 𝑥 ∈ ran card)
3	2	anbi1ci 627	. . . . . . 7 ⊢ ((ω ⊆ 𝑥 ∧ (card‘𝑥) = 𝑥) ↔ (𝑥 ∈ ran card ∧ ω ⊆ 𝑥))
4	3	abbii 2885	. . . . . 6 ⊢ {𝑥 ∣ (ω ⊆ 𝑥 ∧ (card‘𝑥) = 𝑥)} = {𝑥 ∣ (𝑥 ∈ ran card ∧ ω ⊆ 𝑥)}
5		df-rab 3146	. . . . . 6 ⊢ {𝑥 ∈ ran card ∣ ω ⊆ 𝑥} = {𝑥 ∣ (𝑥 ∈ ran card ∧ ω ⊆ 𝑥)}
6	4, 5	eqtr4i 2846	. . . . 5 ⊢ {𝑥 ∣ (ω ⊆ 𝑥 ∧ (card‘𝑥) = 𝑥)} = {𝑥 ∈ ran card ∣ ω ⊆ 𝑥}
7		f1oeq3 6603	. . . . 5 ⊢ ({𝑥 ∣ (ω ⊆ 𝑥 ∧ (card‘𝑥) = 𝑥)} = {𝑥 ∈ ran card ∣ ω ⊆ 𝑥} → (ℵ:On–1-1-onto→{𝑥 ∣ (ω ⊆ 𝑥 ∧ (card‘𝑥) = 𝑥)} ↔ ℵ:On–1-1-onto→{𝑥 ∈ ran card ∣ ω ⊆ 𝑥}))
8	6, 7	ax-mp 5	. . . 4 ⊢ (ℵ:On–1-1-onto→{𝑥 ∣ (ω ⊆ 𝑥 ∧ (card‘𝑥) = 𝑥)} ↔ ℵ:On–1-1-onto→{𝑥 ∈ ran card ∣ ω ⊆ 𝑥})
9		alephon 9492	. . . . . . . . 9 ⊢ (ℵ‘𝑧) ∈ On
10		epelg 5463	. . . . . . . . 9 ⊢ ((ℵ‘𝑧) ∈ On → ((ℵ‘𝑦) E (ℵ‘𝑧) ↔ (ℵ‘𝑦) ∈ (ℵ‘𝑧)))
11	9, 10	mp1i 13	. . . . . . . 8 ⊢ ((𝑦 ∈ On ∧ 𝑧 ∈ On) → ((ℵ‘𝑦) E (ℵ‘𝑧) ↔ (ℵ‘𝑦) ∈ (ℵ‘𝑧)))
12		alephord2 9499	. . . . . . . 8 ⊢ ((𝑦 ∈ On ∧ 𝑧 ∈ On) → (𝑦 ∈ 𝑧 ↔ (ℵ‘𝑦) ∈ (ℵ‘𝑧)))
13		alephord 9498	. . . . . . . 8 ⊢ ((𝑦 ∈ On ∧ 𝑧 ∈ On) → (𝑦 ∈ 𝑧 ↔ (ℵ‘𝑦) ≺ (ℵ‘𝑧)))
14	11, 12, 13	3bitr2d 309	. . . . . . 7 ⊢ ((𝑦 ∈ On ∧ 𝑧 ∈ On) → ((ℵ‘𝑦) E (ℵ‘𝑧) ↔ (ℵ‘𝑦) ≺ (ℵ‘𝑧)))
15	14	bibi2d 345	. . . . . 6 ⊢ ((𝑦 ∈ On ∧ 𝑧 ∈ On) → ((𝑦 E 𝑧 ↔ (ℵ‘𝑦) E (ℵ‘𝑧)) ↔ (𝑦 E 𝑧 ↔ (ℵ‘𝑦) ≺ (ℵ‘𝑧))))
16	15	ralbidva 3195	. . . . 5 ⊢ (𝑦 ∈ On → (∀𝑧 ∈ On (𝑦 E 𝑧 ↔ (ℵ‘𝑦) E (ℵ‘𝑧)) ↔ ∀𝑧 ∈ On (𝑦 E 𝑧 ↔ (ℵ‘𝑦) ≺ (ℵ‘𝑧))))
17	16	ralbiia 3163	. . . 4 ⊢ (∀𝑦 ∈ On ∀𝑧 ∈ On (𝑦 E 𝑧 ↔ (ℵ‘𝑦) E (ℵ‘𝑧)) ↔ ∀𝑦 ∈ On ∀𝑧 ∈ On (𝑦 E 𝑧 ↔ (ℵ‘𝑦) ≺ (ℵ‘𝑧)))
18	8, 17	anbi12i 628	. . 3 ⊢ ((ℵ:On–1-1-onto→{𝑥 ∣ (ω ⊆ 𝑥 ∧ (card‘𝑥) = 𝑥)} ∧ ∀𝑦 ∈ On ∀𝑧 ∈ On (𝑦 E 𝑧 ↔ (ℵ‘𝑦) E (ℵ‘𝑧))) ↔ (ℵ:On–1-1-onto→{𝑥 ∈ ran card ∣ ω ⊆ 𝑥} ∧ ∀𝑦 ∈ On ∀𝑧 ∈ On (𝑦 E 𝑧 ↔ (ℵ‘𝑦) ≺ (ℵ‘𝑧))))
19		df-isom 6361	. . 3 ⊢ (ℵ Isom E , E (On, {𝑥 ∣ (ω ⊆ 𝑥 ∧ (card‘𝑥) = 𝑥)}) ↔ (ℵ:On–1-1-onto→{𝑥 ∣ (ω ⊆ 𝑥 ∧ (card‘𝑥) = 𝑥)} ∧ ∀𝑦 ∈ On ∀𝑧 ∈ On (𝑦 E 𝑧 ↔ (ℵ‘𝑦) E (ℵ‘𝑧))))
20		df-isom 6361	. . 3 ⊢ (ℵ Isom E , ≺ (On, {𝑥 ∈ ran card ∣ ω ⊆ 𝑥}) ↔ (ℵ:On–1-1-onto→{𝑥 ∈ ran card ∣ ω ⊆ 𝑥} ∧ ∀𝑦 ∈ On ∀𝑧 ∈ On (𝑦 E 𝑧 ↔ (ℵ‘𝑦) ≺ (ℵ‘𝑧))))
21	18, 19, 20	3bitr4i 305	. 2 ⊢ (ℵ Isom E , E (On, {𝑥 ∣ (ω ⊆ 𝑥 ∧ (card‘𝑥) = 𝑥)}) ↔ ℵ Isom E , ≺ (On, {𝑥 ∈ ran card ∣ ω ⊆ 𝑥}))
22	1, 21	mpbi 232	1 ⊢ ℵ Isom E , ≺ (On, {𝑥 ∈ ran card ∣ ω ⊆ 𝑥})

Syntax hints:   ↔ wb 208   ∧ wa 398   = wceq 1536   ∈ wcel 2113  {cab 2798  ∀wral 3137  {crab 3141   ⊆ wss 3933   class class class wbr 5063   E cep 5461  ran crn 5553  Oncon0 6188  –1-1-onto→wf1o 6351  ‘cfv 6352   Isom wiso 6353  ωcom 7577   ≺ csdm 8505  cardccrd 9361  ℵcale 9362

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2792  ax-rep 5187  ax-sep 5200  ax-nul 5207  ax-pow 5263  ax-pr 5327  ax-un 7458  ax-inf2 9101

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1083  df-3an 1084  df-tru 1539  df-fal 1549  df-ex 1780  df-nf 1784  df-sb 2069  df-mo 2621  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2892  df-nfc 2962  df-ne 3016  df-ral 3142  df-rex 3143  df-reu 3144  df-rmo 3145  df-rab 3146  df-v 3495  df-sbc 3771  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4465  df-pw 4538  df-sn 4565  df-pr 4567  df-tp 4569  df-op 4571  df-uni 4836  df-int 4874  df-iun 4918  df-br 5064  df-opab 5126  df-mpt 5144  df-tr 5170  df-id 5457  df-eprel 5462  df-po 5471  df-so 5472  df-fr 5511  df-se 5512  df-we 5513  df-xp 5558  df-rel 5559  df-cnv 5560  df-co 5561  df-dm 5562  df-rn 5563  df-res 5564  df-ima 5565  df-pred 6145  df-ord 6191  df-on 6192  df-lim 6193  df-suc 6194  df-iota 6311  df-fun 6354  df-fn 6355  df-f 6356  df-f1 6357  df-fo 6358  df-f1o 6359  df-fv 6360  df-isom 6361  df-riota 7111  df-om 7578  df-wrecs 7944  df-recs 8005  df-rdg 8043  df-er 8286  df-en 8507  df-dom 8508  df-sdom 8509  df-fin 8510  df-oi 8971  df-har 9019  df-card 9365  df-aleph 9366

This theorem is referenced by:  alephiso3  39992