Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  pwcfsdom Structured version   Visualization version   GIF version

Theorem pwcfsdom 9617
 Description: A corollary of Konig's Theorem konigth 9603. Theorem 11.28 of [TakeutiZaring] p. 108. (Contributed by Mario Carneiro, 20-Mar-2013.)
Hypothesis
Ref Expression
pwcfsdom.1 𝐻 = (𝑦 ∈ (cf‘(ℵ‘𝐴)) ↦ (har‘(𝑓𝑦)))
Assertion
Ref Expression
pwcfsdom (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑𝑚 (cf‘(ℵ‘𝐴)))
Distinct variable group:   𝐴,𝑓,𝑦
Allowed substitution hints:   𝐻(𝑦,𝑓)

Proof of Theorem pwcfsdom
Dummy variables 𝑤 𝑧 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 onzsl 7212 . . . 4 (𝐴 ∈ On ↔ (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ (𝐴 ∈ V ∧ Lim 𝐴)))
21biimpi 206 . . 3 (𝐴 ∈ On → (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ (𝐴 ∈ V ∧ Lim 𝐴)))
3 cfom 9298 . . . . . . 7 (cf‘ω) = ω
4 aleph0 9099 . . . . . . . 8 (ℵ‘∅) = ω
54fveq2i 6356 . . . . . . 7 (cf‘(ℵ‘∅)) = (cf‘ω)
63, 5, 43eqtr4i 2792 . . . . . 6 (cf‘(ℵ‘∅)) = (ℵ‘∅)
7 fveq2 6353 . . . . . . 7 (𝐴 = ∅ → (ℵ‘𝐴) = (ℵ‘∅))
87fveq2d 6357 . . . . . 6 (𝐴 = ∅ → (cf‘(ℵ‘𝐴)) = (cf‘(ℵ‘∅)))
96, 8, 73eqtr4a 2820 . . . . 5 (𝐴 = ∅ → (cf‘(ℵ‘𝐴)) = (ℵ‘𝐴))
10 fvex 6363 . . . . . . . . 9 (ℵ‘𝐴) ∈ V
1110canth2 8280 . . . . . . . 8 (ℵ‘𝐴) ≺ 𝒫 (ℵ‘𝐴)
1210pw2en 8234 . . . . . . . 8 𝒫 (ℵ‘𝐴) ≈ (2𝑜𝑚 (ℵ‘𝐴))
13 sdomentr 8261 . . . . . . . 8 (((ℵ‘𝐴) ≺ 𝒫 (ℵ‘𝐴) ∧ 𝒫 (ℵ‘𝐴) ≈ (2𝑜𝑚 (ℵ‘𝐴))) → (ℵ‘𝐴) ≺ (2𝑜𝑚 (ℵ‘𝐴)))
1411, 12, 13mp2an 710 . . . . . . 7 (ℵ‘𝐴) ≺ (2𝑜𝑚 (ℵ‘𝐴))
15 alephon 9102 . . . . . . . . 9 (ℵ‘𝐴) ∈ On
16 alephgeom 9115 . . . . . . . . . 10 (𝐴 ∈ On ↔ ω ⊆ (ℵ‘𝐴))
17 omelon 8718 . . . . . . . . . . . 12 ω ∈ On
18 2onn 7891 . . . . . . . . . . . 12 2𝑜 ∈ ω
19 onelss 5927 . . . . . . . . . . . 12 (ω ∈ On → (2𝑜 ∈ ω → 2𝑜 ⊆ ω))
2017, 18, 19mp2 9 . . . . . . . . . . 11 2𝑜 ⊆ ω
21 sstr 3752 . . . . . . . . . . 11 ((2𝑜 ⊆ ω ∧ ω ⊆ (ℵ‘𝐴)) → 2𝑜 ⊆ (ℵ‘𝐴))
2220, 21mpan 708 . . . . . . . . . 10 (ω ⊆ (ℵ‘𝐴) → 2𝑜 ⊆ (ℵ‘𝐴))
2316, 22sylbi 207 . . . . . . . . 9 (𝐴 ∈ On → 2𝑜 ⊆ (ℵ‘𝐴))
24 ssdomg 8169 . . . . . . . . 9 ((ℵ‘𝐴) ∈ On → (2𝑜 ⊆ (ℵ‘𝐴) → 2𝑜 ≼ (ℵ‘𝐴)))
2515, 23, 24mpsyl 68 . . . . . . . 8 (𝐴 ∈ On → 2𝑜 ≼ (ℵ‘𝐴))
26 mapdom1 8292 . . . . . . . 8 (2𝑜 ≼ (ℵ‘𝐴) → (2𝑜𝑚 (ℵ‘𝐴)) ≼ ((ℵ‘𝐴) ↑𝑚 (ℵ‘𝐴)))
2725, 26syl 17 . . . . . . 7 (𝐴 ∈ On → (2𝑜𝑚 (ℵ‘𝐴)) ≼ ((ℵ‘𝐴) ↑𝑚 (ℵ‘𝐴)))
28 sdomdomtr 8260 . . . . . . 7 (((ℵ‘𝐴) ≺ (2𝑜𝑚 (ℵ‘𝐴)) ∧ (2𝑜𝑚 (ℵ‘𝐴)) ≼ ((ℵ‘𝐴) ↑𝑚 (ℵ‘𝐴))) → (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑𝑚 (ℵ‘𝐴)))
2914, 27, 28sylancr 698 . . . . . 6 (𝐴 ∈ On → (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑𝑚 (ℵ‘𝐴)))
30 oveq2 6822 . . . . . . 7 ((cf‘(ℵ‘𝐴)) = (ℵ‘𝐴) → ((ℵ‘𝐴) ↑𝑚 (cf‘(ℵ‘𝐴))) = ((ℵ‘𝐴) ↑𝑚 (ℵ‘𝐴)))
3130breq2d 4816 . . . . . 6 ((cf‘(ℵ‘𝐴)) = (ℵ‘𝐴) → ((ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑𝑚 (cf‘(ℵ‘𝐴))) ↔ (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑𝑚 (ℵ‘𝐴))))
3229, 31syl5ibrcom 237 . . . . 5 (𝐴 ∈ On → ((cf‘(ℵ‘𝐴)) = (ℵ‘𝐴) → (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑𝑚 (cf‘(ℵ‘𝐴)))))
339, 32syl5 34 . . . 4 (𝐴 ∈ On → (𝐴 = ∅ → (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑𝑚 (cf‘(ℵ‘𝐴)))))
34 alephreg 9616 . . . . . . 7 (cf‘(ℵ‘suc 𝑥)) = (ℵ‘suc 𝑥)
35 fveq2 6353 . . . . . . . 8 (𝐴 = suc 𝑥 → (ℵ‘𝐴) = (ℵ‘suc 𝑥))
3635fveq2d 6357 . . . . . . 7 (𝐴 = suc 𝑥 → (cf‘(ℵ‘𝐴)) = (cf‘(ℵ‘suc 𝑥)))
3734, 36, 353eqtr4a 2820 . . . . . 6 (𝐴 = suc 𝑥 → (cf‘(ℵ‘𝐴)) = (ℵ‘𝐴))
3837rexlimivw 3167 . . . . 5 (∃𝑥 ∈ On 𝐴 = suc 𝑥 → (cf‘(ℵ‘𝐴)) = (ℵ‘𝐴))
3938, 32syl5 34 . . . 4 (𝐴 ∈ On → (∃𝑥 ∈ On 𝐴 = suc 𝑥 → (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑𝑚 (cf‘(ℵ‘𝐴)))))
40 cfsmo 9305 . . . . . 6 ((ℵ‘𝐴) ∈ On → ∃𝑓(𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ Smo 𝑓 ∧ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓𝑤)))
41 limelon 5949 . . . . . . . . . . 11 ((𝐴 ∈ V ∧ Lim 𝐴) → 𝐴 ∈ On)
42 ffn 6206 . . . . . . . . . . . . . . . 16 (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) → 𝑓 Fn (cf‘(ℵ‘𝐴)))
43 fnrnfv 6405 . . . . . . . . . . . . . . . . 17 (𝑓 Fn (cf‘(ℵ‘𝐴)) → ran 𝑓 = {𝑦 ∣ ∃𝑥 ∈ (cf‘(ℵ‘𝐴))𝑦 = (𝑓𝑥)})
4443unieqd 4598 . . . . . . . . . . . . . . . 16 (𝑓 Fn (cf‘(ℵ‘𝐴)) → ran 𝑓 = {𝑦 ∣ ∃𝑥 ∈ (cf‘(ℵ‘𝐴))𝑦 = (𝑓𝑥)})
4542, 44syl 17 . . . . . . . . . . . . . . 15 (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) → ran 𝑓 = {𝑦 ∣ ∃𝑥 ∈ (cf‘(ℵ‘𝐴))𝑦 = (𝑓𝑥)})
46 fvex 6363 . . . . . . . . . . . . . . . 16 (𝑓𝑥) ∈ V
4746dfiun2 4706 . . . . . . . . . . . . . . 15 𝑥 ∈ (cf‘(ℵ‘𝐴))(𝑓𝑥) = {𝑦 ∣ ∃𝑥 ∈ (cf‘(ℵ‘𝐴))𝑦 = (𝑓𝑥)}
4845, 47syl6eqr 2812 . . . . . . . . . . . . . 14 (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) → ran 𝑓 = 𝑥 ∈ (cf‘(ℵ‘𝐴))(𝑓𝑥))
4948ad2antrl 766 . . . . . . . . . . . . 13 ((𝐴 ∈ On ∧ (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓𝑤))) → ran 𝑓 = 𝑥 ∈ (cf‘(ℵ‘𝐴))(𝑓𝑥))
50 fnfvelrn 6520 . . . . . . . . . . . . . . . . . . . . 21 ((𝑓 Fn (cf‘(ℵ‘𝐴)) ∧ 𝑤 ∈ (cf‘(ℵ‘𝐴))) → (𝑓𝑤) ∈ ran 𝑓)
5142, 50sylan 489 . . . . . . . . . . . . . . . . . . . 20 ((𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ 𝑤 ∈ (cf‘(ℵ‘𝐴))) → (𝑓𝑤) ∈ ran 𝑓)
52 sseq2 3768 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = (𝑓𝑤) → (𝑧𝑦𝑧 ⊆ (𝑓𝑤)))
5352rspcev 3449 . . . . . . . . . . . . . . . . . . . 20 (((𝑓𝑤) ∈ ran 𝑓𝑧 ⊆ (𝑓𝑤)) → ∃𝑦 ∈ ran 𝑓 𝑧𝑦)
5451, 53sylan 489 . . . . . . . . . . . . . . . . . . 19 (((𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ 𝑤 ∈ (cf‘(ℵ‘𝐴))) ∧ 𝑧 ⊆ (𝑓𝑤)) → ∃𝑦 ∈ ran 𝑓 𝑧𝑦)
5554ex 449 . . . . . . . . . . . . . . . . . 18 ((𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ 𝑤 ∈ (cf‘(ℵ‘𝐴))) → (𝑧 ⊆ (𝑓𝑤) → ∃𝑦 ∈ ran 𝑓 𝑧𝑦))
5655rexlimdva 3169 . . . . . . . . . . . . . . . . 17 (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) → (∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓𝑤) → ∃𝑦 ∈ ran 𝑓 𝑧𝑦))
5756ralimdv 3101 . . . . . . . . . . . . . . . 16 (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) → (∀𝑧 ∈ (ℵ‘𝐴)∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓𝑤) → ∀𝑧 ∈ (ℵ‘𝐴)∃𝑦 ∈ ran 𝑓 𝑧𝑦))
5857imp 444 . . . . . . . . . . . . . . 15 ((𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓𝑤)) → ∀𝑧 ∈ (ℵ‘𝐴)∃𝑦 ∈ ran 𝑓 𝑧𝑦)
5958adantl 473 . . . . . . . . . . . . . 14 ((𝐴 ∈ On ∧ (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓𝑤))) → ∀𝑧 ∈ (ℵ‘𝐴)∃𝑦 ∈ ran 𝑓 𝑧𝑦)
60 alephislim 9116 . . . . . . . . . . . . . . . 16 (𝐴 ∈ On ↔ Lim (ℵ‘𝐴))
6160biimpi 206 . . . . . . . . . . . . . . 15 (𝐴 ∈ On → Lim (ℵ‘𝐴))
62 frn 6214 . . . . . . . . . . . . . . . 16 (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) → ran 𝑓 ⊆ (ℵ‘𝐴))
6362adantr 472 . . . . . . . . . . . . . . 15 ((𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓𝑤)) → ran 𝑓 ⊆ (ℵ‘𝐴))
64 coflim 9295 . . . . . . . . . . . . . . 15 ((Lim (ℵ‘𝐴) ∧ ran 𝑓 ⊆ (ℵ‘𝐴)) → ( ran 𝑓 = (ℵ‘𝐴) ↔ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑦 ∈ ran 𝑓 𝑧𝑦))
6561, 63, 64syl2an 495 . . . . . . . . . . . . . 14 ((𝐴 ∈ On ∧ (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓𝑤))) → ( ran 𝑓 = (ℵ‘𝐴) ↔ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑦 ∈ ran 𝑓 𝑧𝑦))
6659, 65mpbird 247 . . . . . . . . . . . . 13 ((𝐴 ∈ On ∧ (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓𝑤))) → ran 𝑓 = (ℵ‘𝐴))
6749, 66eqtr3d 2796 . . . . . . . . . . . 12 ((𝐴 ∈ On ∧ (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓𝑤))) → 𝑥 ∈ (cf‘(ℵ‘𝐴))(𝑓𝑥) = (ℵ‘𝐴))
68 ffvelrn 6521 . . . . . . . . . . . . . . . . 17 ((𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ 𝑥 ∈ (cf‘(ℵ‘𝐴))) → (𝑓𝑥) ∈ (ℵ‘𝐴))
6915oneli 5996 . . . . . . . . . . . . . . . . 17 ((𝑓𝑥) ∈ (ℵ‘𝐴) → (𝑓𝑥) ∈ On)
70 harcard 9014 . . . . . . . . . . . . . . . . . . 19 (card‘(har‘(𝑓𝑥))) = (har‘(𝑓𝑥))
71 iscard 9011 . . . . . . . . . . . . . . . . . . . 20 ((card‘(har‘(𝑓𝑥))) = (har‘(𝑓𝑥)) ↔ ((har‘(𝑓𝑥)) ∈ On ∧ ∀𝑦 ∈ (har‘(𝑓𝑥))𝑦 ≺ (har‘(𝑓𝑥))))
7271simprbi 483 . . . . . . . . . . . . . . . . . . 19 ((card‘(har‘(𝑓𝑥))) = (har‘(𝑓𝑥)) → ∀𝑦 ∈ (har‘(𝑓𝑥))𝑦 ≺ (har‘(𝑓𝑥)))
7370, 72ax-mp 5 . . . . . . . . . . . . . . . . . 18 𝑦 ∈ (har‘(𝑓𝑥))𝑦 ≺ (har‘(𝑓𝑥))
74 domrefg 8158 . . . . . . . . . . . . . . . . . . . 20 ((𝑓𝑥) ∈ V → (𝑓𝑥) ≼ (𝑓𝑥))
7546, 74ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (𝑓𝑥) ≼ (𝑓𝑥)
76 elharval 8635 . . . . . . . . . . . . . . . . . . . 20 ((𝑓𝑥) ∈ (har‘(𝑓𝑥)) ↔ ((𝑓𝑥) ∈ On ∧ (𝑓𝑥) ≼ (𝑓𝑥)))
7776biimpri 218 . . . . . . . . . . . . . . . . . . 19 (((𝑓𝑥) ∈ On ∧ (𝑓𝑥) ≼ (𝑓𝑥)) → (𝑓𝑥) ∈ (har‘(𝑓𝑥)))
7875, 77mpan2 709 . . . . . . . . . . . . . . . . . 18 ((𝑓𝑥) ∈ On → (𝑓𝑥) ∈ (har‘(𝑓𝑥)))
79 breq1 4807 . . . . . . . . . . . . . . . . . . 19 (𝑦 = (𝑓𝑥) → (𝑦 ≺ (har‘(𝑓𝑥)) ↔ (𝑓𝑥) ≺ (har‘(𝑓𝑥))))
8079rspccv 3446 . . . . . . . . . . . . . . . . . 18 (∀𝑦 ∈ (har‘(𝑓𝑥))𝑦 ≺ (har‘(𝑓𝑥)) → ((𝑓𝑥) ∈ (har‘(𝑓𝑥)) → (𝑓𝑥) ≺ (har‘(𝑓𝑥))))
8173, 78, 80mpsyl 68 . . . . . . . . . . . . . . . . 17 ((𝑓𝑥) ∈ On → (𝑓𝑥) ≺ (har‘(𝑓𝑥)))
8268, 69, 813syl 18 . . . . . . . . . . . . . . . 16 ((𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ 𝑥 ∈ (cf‘(ℵ‘𝐴))) → (𝑓𝑥) ≺ (har‘(𝑓𝑥)))
83 harcl 8633 . . . . . . . . . . . . . . . . . . 19 (har‘(𝑓𝑥)) ∈ On
84 fveq2 6353 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = 𝑥 → (𝑓𝑦) = (𝑓𝑥))
8584fveq2d 6357 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑥 → (har‘(𝑓𝑦)) = (har‘(𝑓𝑥)))
86 pwcfsdom.1 . . . . . . . . . . . . . . . . . . . 20 𝐻 = (𝑦 ∈ (cf‘(ℵ‘𝐴)) ↦ (har‘(𝑓𝑦)))
8785, 86fvmptg 6443 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (cf‘(ℵ‘𝐴)) ∧ (har‘(𝑓𝑥)) ∈ On) → (𝐻𝑥) = (har‘(𝑓𝑥)))
8883, 87mpan2 709 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (cf‘(ℵ‘𝐴)) → (𝐻𝑥) = (har‘(𝑓𝑥)))
8988breq2d 4816 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (cf‘(ℵ‘𝐴)) → ((𝑓𝑥) ≺ (𝐻𝑥) ↔ (𝑓𝑥) ≺ (har‘(𝑓𝑥))))
9089adantl 473 . . . . . . . . . . . . . . . 16 ((𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ 𝑥 ∈ (cf‘(ℵ‘𝐴))) → ((𝑓𝑥) ≺ (𝐻𝑥) ↔ (𝑓𝑥) ≺ (har‘(𝑓𝑥))))
9182, 90mpbird 247 . . . . . . . . . . . . . . 15 ((𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ 𝑥 ∈ (cf‘(ℵ‘𝐴))) → (𝑓𝑥) ≺ (𝐻𝑥))
9291ralrimiva 3104 . . . . . . . . . . . . . 14 (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) → ∀𝑥 ∈ (cf‘(ℵ‘𝐴))(𝑓𝑥) ≺ (𝐻𝑥))
93 fvex 6363 . . . . . . . . . . . . . . 15 (cf‘(ℵ‘𝐴)) ∈ V
94 eqid 2760 . . . . . . . . . . . . . . 15 𝑥 ∈ (cf‘(ℵ‘𝐴))(𝑓𝑥) = 𝑥 ∈ (cf‘(ℵ‘𝐴))(𝑓𝑥)
95 eqid 2760 . . . . . . . . . . . . . . 15 X𝑥 ∈ (cf‘(ℵ‘𝐴))(𝐻𝑥) = X𝑥 ∈ (cf‘(ℵ‘𝐴))(𝐻𝑥)
9693, 94, 95konigth 9603 . . . . . . . . . . . . . 14 (∀𝑥 ∈ (cf‘(ℵ‘𝐴))(𝑓𝑥) ≺ (𝐻𝑥) → 𝑥 ∈ (cf‘(ℵ‘𝐴))(𝑓𝑥) ≺ X𝑥 ∈ (cf‘(ℵ‘𝐴))(𝐻𝑥))
9792, 96syl 17 . . . . . . . . . . . . 13 (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) → 𝑥 ∈ (cf‘(ℵ‘𝐴))(𝑓𝑥) ≺ X𝑥 ∈ (cf‘(ℵ‘𝐴))(𝐻𝑥))
9897ad2antrl 766 . . . . . . . . . . . 12 ((𝐴 ∈ On ∧ (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓𝑤))) → 𝑥 ∈ (cf‘(ℵ‘𝐴))(𝑓𝑥) ≺ X𝑥 ∈ (cf‘(ℵ‘𝐴))(𝐻𝑥))
9967, 98eqbrtrrd 4828 . . . . . . . . . . 11 ((𝐴 ∈ On ∧ (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓𝑤))) → (ℵ‘𝐴) ≺ X𝑥 ∈ (cf‘(ℵ‘𝐴))(𝐻𝑥))
10041, 99sylan 489 . . . . . . . . . 10 (((𝐴 ∈ V ∧ Lim 𝐴) ∧ (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓𝑤))) → (ℵ‘𝐴) ≺ X𝑥 ∈ (cf‘(ℵ‘𝐴))(𝐻𝑥))
101 ovex 6842 . . . . . . . . . . . 12 ((ℵ‘𝐴) ↑𝑚 (cf‘(ℵ‘𝐴))) ∈ V
10268ex 449 . . . . . . . . . . . . . . . 16 (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) → (𝑥 ∈ (cf‘(ℵ‘𝐴)) → (𝑓𝑥) ∈ (ℵ‘𝐴)))
103 alephlim 9100 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ V ∧ Lim 𝐴) → (ℵ‘𝐴) = 𝑦𝐴 (ℵ‘𝑦))
104103eleq2d 2825 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ V ∧ Lim 𝐴) → ((𝑓𝑥) ∈ (ℵ‘𝐴) ↔ (𝑓𝑥) ∈ 𝑦𝐴 (ℵ‘𝑦)))
105 eliun 4676 . . . . . . . . . . . . . . . . . . 19 ((𝑓𝑥) ∈ 𝑦𝐴 (ℵ‘𝑦) ↔ ∃𝑦𝐴 (𝑓𝑥) ∈ (ℵ‘𝑦))
106 alephcard 9103 . . . . . . . . . . . . . . . . . . . . . . . . 25 (card‘(ℵ‘𝑦)) = (ℵ‘𝑦)
107106eleq2i 2831 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑓𝑥) ∈ (card‘(ℵ‘𝑦)) ↔ (𝑓𝑥) ∈ (ℵ‘𝑦))
108 cardsdomelir 9009 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑓𝑥) ∈ (card‘(ℵ‘𝑦)) → (𝑓𝑥) ≺ (ℵ‘𝑦))
109107, 108sylbir 225 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑓𝑥) ∈ (ℵ‘𝑦) → (𝑓𝑥) ≺ (ℵ‘𝑦))
110 elharval 8635 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((ℵ‘𝑦) ∈ (har‘(𝑓𝑥)) ↔ ((ℵ‘𝑦) ∈ On ∧ (ℵ‘𝑦) ≼ (𝑓𝑥)))
111110simprbi 483 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((ℵ‘𝑦) ∈ (har‘(𝑓𝑥)) → (ℵ‘𝑦) ≼ (𝑓𝑥))
112 domnsym 8253 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((ℵ‘𝑦) ≼ (𝑓𝑥) → ¬ (𝑓𝑥) ≺ (ℵ‘𝑦))
113111, 112syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((ℵ‘𝑦) ∈ (har‘(𝑓𝑥)) → ¬ (𝑓𝑥) ≺ (ℵ‘𝑦))
114113con2i 134 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑓𝑥) ≺ (ℵ‘𝑦) → ¬ (ℵ‘𝑦) ∈ (har‘(𝑓𝑥)))
115 alephon 9102 . . . . . . . . . . . . . . . . . . . . . . . . 25 (ℵ‘𝑦) ∈ On
116 ontri1 5918 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((har‘(𝑓𝑥)) ∈ On ∧ (ℵ‘𝑦) ∈ On) → ((har‘(𝑓𝑥)) ⊆ (ℵ‘𝑦) ↔ ¬ (ℵ‘𝑦) ∈ (har‘(𝑓𝑥))))
11783, 115, 116mp2an 710 . . . . . . . . . . . . . . . . . . . . . . . 24 ((har‘(𝑓𝑥)) ⊆ (ℵ‘𝑦) ↔ ¬ (ℵ‘𝑦) ∈ (har‘(𝑓𝑥)))
118114, 117sylibr 224 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑓𝑥) ≺ (ℵ‘𝑦) → (har‘(𝑓𝑥)) ⊆ (ℵ‘𝑦))
119109, 118syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓𝑥) ∈ (ℵ‘𝑦) → (har‘(𝑓𝑥)) ⊆ (ℵ‘𝑦))
120 alephord2i 9110 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐴 ∈ On → (𝑦𝐴 → (ℵ‘𝑦) ∈ (ℵ‘𝐴)))
121120imp 444 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 ∈ On ∧ 𝑦𝐴) → (ℵ‘𝑦) ∈ (ℵ‘𝐴))
122 ontr2 5933 . . . . . . . . . . . . . . . . . . . . . . 23 (((har‘(𝑓𝑥)) ∈ On ∧ (ℵ‘𝐴) ∈ On) → (((har‘(𝑓𝑥)) ⊆ (ℵ‘𝑦) ∧ (ℵ‘𝑦) ∈ (ℵ‘𝐴)) → (har‘(𝑓𝑥)) ∈ (ℵ‘𝐴)))
12383, 15, 122mp2an 710 . . . . . . . . . . . . . . . . . . . . . 22 (((har‘(𝑓𝑥)) ⊆ (ℵ‘𝑦) ∧ (ℵ‘𝑦) ∈ (ℵ‘𝐴)) → (har‘(𝑓𝑥)) ∈ (ℵ‘𝐴))
124119, 121, 123syl2anr 496 . . . . . . . . . . . . . . . . . . . . 21 (((𝐴 ∈ On ∧ 𝑦𝐴) ∧ (𝑓𝑥) ∈ (ℵ‘𝑦)) → (har‘(𝑓𝑥)) ∈ (ℵ‘𝐴))
125124exp31 631 . . . . . . . . . . . . . . . . . . . 20 (𝐴 ∈ On → (𝑦𝐴 → ((𝑓𝑥) ∈ (ℵ‘𝑦) → (har‘(𝑓𝑥)) ∈ (ℵ‘𝐴))))
126125rexlimdv 3168 . . . . . . . . . . . . . . . . . . 19 (𝐴 ∈ On → (∃𝑦𝐴 (𝑓𝑥) ∈ (ℵ‘𝑦) → (har‘(𝑓𝑥)) ∈ (ℵ‘𝐴)))
127105, 126syl5bi 232 . . . . . . . . . . . . . . . . . 18 (𝐴 ∈ On → ((𝑓𝑥) ∈ 𝑦𝐴 (ℵ‘𝑦) → (har‘(𝑓𝑥)) ∈ (ℵ‘𝐴)))
12841, 127syl 17 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ V ∧ Lim 𝐴) → ((𝑓𝑥) ∈ 𝑦𝐴 (ℵ‘𝑦) → (har‘(𝑓𝑥)) ∈ (ℵ‘𝐴)))
129104, 128sylbid 230 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ V ∧ Lim 𝐴) → ((𝑓𝑥) ∈ (ℵ‘𝐴) → (har‘(𝑓𝑥)) ∈ (ℵ‘𝐴)))
130102, 129sylan9r 693 . . . . . . . . . . . . . . 15 (((𝐴 ∈ V ∧ Lim 𝐴) ∧ 𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴)) → (𝑥 ∈ (cf‘(ℵ‘𝐴)) → (har‘(𝑓𝑥)) ∈ (ℵ‘𝐴)))
131130imp 444 . . . . . . . . . . . . . 14 ((((𝐴 ∈ V ∧ Lim 𝐴) ∧ 𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴)) ∧ 𝑥 ∈ (cf‘(ℵ‘𝐴))) → (har‘(𝑓𝑥)) ∈ (ℵ‘𝐴))
13285cbvmptv 4902 . . . . . . . . . . . . . . 15 (𝑦 ∈ (cf‘(ℵ‘𝐴)) ↦ (har‘(𝑓𝑦))) = (𝑥 ∈ (cf‘(ℵ‘𝐴)) ↦ (har‘(𝑓𝑥)))
13386, 132eqtri 2782 . . . . . . . . . . . . . 14 𝐻 = (𝑥 ∈ (cf‘(ℵ‘𝐴)) ↦ (har‘(𝑓𝑥)))
134131, 133fmptd 6549 . . . . . . . . . . . . 13 (((𝐴 ∈ V ∧ Lim 𝐴) ∧ 𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴)) → 𝐻:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴))
135 ffvelrn 6521 . . . . . . . . . . . . . . 15 ((𝐻:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ 𝑥 ∈ (cf‘(ℵ‘𝐴))) → (𝐻𝑥) ∈ (ℵ‘𝐴))
136 onelss 5927 . . . . . . . . . . . . . . 15 ((ℵ‘𝐴) ∈ On → ((𝐻𝑥) ∈ (ℵ‘𝐴) → (𝐻𝑥) ⊆ (ℵ‘𝐴)))
13715, 135, 136mpsyl 68 . . . . . . . . . . . . . 14 ((𝐻:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ 𝑥 ∈ (cf‘(ℵ‘𝐴))) → (𝐻𝑥) ⊆ (ℵ‘𝐴))
138137ralrimiva 3104 . . . . . . . . . . . . 13 (𝐻:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) → ∀𝑥 ∈ (cf‘(ℵ‘𝐴))(𝐻𝑥) ⊆ (ℵ‘𝐴))
139 ss2ixp 8089 . . . . . . . . . . . . . 14 (∀𝑥 ∈ (cf‘(ℵ‘𝐴))(𝐻𝑥) ⊆ (ℵ‘𝐴) → X𝑥 ∈ (cf‘(ℵ‘𝐴))(𝐻𝑥) ⊆ X𝑥 ∈ (cf‘(ℵ‘𝐴))(ℵ‘𝐴))
14093, 10ixpconst 8086 . . . . . . . . . . . . . 14 X𝑥 ∈ (cf‘(ℵ‘𝐴))(ℵ‘𝐴) = ((ℵ‘𝐴) ↑𝑚 (cf‘(ℵ‘𝐴)))
141139, 140syl6sseq 3792 . . . . . . . . . . . . 13 (∀𝑥 ∈ (cf‘(ℵ‘𝐴))(𝐻𝑥) ⊆ (ℵ‘𝐴) → X𝑥 ∈ (cf‘(ℵ‘𝐴))(𝐻𝑥) ⊆ ((ℵ‘𝐴) ↑𝑚 (cf‘(ℵ‘𝐴))))
142134, 138, 1413syl 18 . . . . . . . . . . . 12 (((𝐴 ∈ V ∧ Lim 𝐴) ∧ 𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴)) → X𝑥 ∈ (cf‘(ℵ‘𝐴))(𝐻𝑥) ⊆ ((ℵ‘𝐴) ↑𝑚 (cf‘(ℵ‘𝐴))))
143 ssdomg 8169 . . . . . . . . . . . 12 (((ℵ‘𝐴) ↑𝑚 (cf‘(ℵ‘𝐴))) ∈ V → (X𝑥 ∈ (cf‘(ℵ‘𝐴))(𝐻𝑥) ⊆ ((ℵ‘𝐴) ↑𝑚 (cf‘(ℵ‘𝐴))) → X𝑥 ∈ (cf‘(ℵ‘𝐴))(𝐻𝑥) ≼ ((ℵ‘𝐴) ↑𝑚 (cf‘(ℵ‘𝐴)))))
144101, 142, 143mpsyl 68 . . . . . . . . . . 11 (((𝐴 ∈ V ∧ Lim 𝐴) ∧ 𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴)) → X𝑥 ∈ (cf‘(ℵ‘𝐴))(𝐻𝑥) ≼ ((ℵ‘𝐴) ↑𝑚 (cf‘(ℵ‘𝐴))))
145144adantrr 755 . . . . . . . . . 10 (((𝐴 ∈ V ∧ Lim 𝐴) ∧ (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓𝑤))) → X𝑥 ∈ (cf‘(ℵ‘𝐴))(𝐻𝑥) ≼ ((ℵ‘𝐴) ↑𝑚 (cf‘(ℵ‘𝐴))))
146 sdomdomtr 8260 . . . . . . . . . 10 (((ℵ‘𝐴) ≺ X𝑥 ∈ (cf‘(ℵ‘𝐴))(𝐻𝑥) ∧ X𝑥 ∈ (cf‘(ℵ‘𝐴))(𝐻𝑥) ≼ ((ℵ‘𝐴) ↑𝑚 (cf‘(ℵ‘𝐴)))) → (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑𝑚 (cf‘(ℵ‘𝐴))))
147100, 145, 146syl2anc 696 . . . . . . . . 9 (((𝐴 ∈ V ∧ Lim 𝐴) ∧ (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓𝑤))) → (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑𝑚 (cf‘(ℵ‘𝐴))))
148147expcom 450 . . . . . . . 8 ((𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓𝑤)) → ((𝐴 ∈ V ∧ Lim 𝐴) → (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑𝑚 (cf‘(ℵ‘𝐴)))))
1491483adant2 1126 . . . . . . 7 ((𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ Smo 𝑓 ∧ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓𝑤)) → ((𝐴 ∈ V ∧ Lim 𝐴) → (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑𝑚 (cf‘(ℵ‘𝐴)))))
150149exlimiv 2007 . . . . . 6 (∃𝑓(𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ Smo 𝑓 ∧ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓𝑤)) → ((𝐴 ∈ V ∧ Lim 𝐴) → (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑𝑚 (cf‘(ℵ‘𝐴)))))
15115, 40, 150mp2b 10 . . . . 5 ((𝐴 ∈ V ∧ Lim 𝐴) → (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑𝑚 (cf‘(ℵ‘𝐴))))
152151a1i 11 . . . 4 (𝐴 ∈ On → ((𝐴 ∈ V ∧ Lim 𝐴) → (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑𝑚 (cf‘(ℵ‘𝐴)))))
15333, 39, 1523jaod 1541 . . 3 (𝐴 ∈ On → ((𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ (𝐴 ∈ V ∧ Lim 𝐴)) → (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑𝑚 (cf‘(ℵ‘𝐴)))))
1542, 153mpd 15 . 2 (𝐴 ∈ On → (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑𝑚 (cf‘(ℵ‘𝐴))))
155 alephfnon 9098 . . . . 5 ℵ Fn On
156 fndm 6151 . . . . 5 (ℵ Fn On → dom ℵ = On)
157155, 156ax-mp 5 . . . 4 dom ℵ = On
158157eleq2i 2831 . . 3 (𝐴 ∈ dom ℵ ↔ 𝐴 ∈ On)
159 ndmfv 6380 . . . 4 𝐴 ∈ dom ℵ → (ℵ‘𝐴) = ∅)
160 1n0 7746 . . . . . 6 1𝑜 ≠ ∅
161 1oex 7738 . . . . . . 7 1𝑜 ∈ V
1621610sdom 8258 . . . . . 6 (∅ ≺ 1𝑜 ↔ 1𝑜 ≠ ∅)
163160, 162mpbir 221 . . . . 5 ∅ ≺ 1𝑜
164 id 22 . . . . . 6 ((ℵ‘𝐴) = ∅ → (ℵ‘𝐴) = ∅)
165 fveq2 6353 . . . . . . . . 9 ((ℵ‘𝐴) = ∅ → (cf‘(ℵ‘𝐴)) = (cf‘∅))
166 cf0 9285 . . . . . . . . 9 (cf‘∅) = ∅
167165, 166syl6eq 2810 . . . . . . . 8 ((ℵ‘𝐴) = ∅ → (cf‘(ℵ‘𝐴)) = ∅)
168164, 167oveq12d 6832 . . . . . . 7 ((ℵ‘𝐴) = ∅ → ((ℵ‘𝐴) ↑𝑚 (cf‘(ℵ‘𝐴))) = (∅ ↑𝑚 ∅))
169 0ex 4942 . . . . . . . 8 ∅ ∈ V
170 map0e 8063 . . . . . . . 8 (∅ ∈ V → (∅ ↑𝑚 ∅) = 1𝑜)
171169, 170ax-mp 5 . . . . . . 7 (∅ ↑𝑚 ∅) = 1𝑜
172168, 171syl6eq 2810 . . . . . 6 ((ℵ‘𝐴) = ∅ → ((ℵ‘𝐴) ↑𝑚 (cf‘(ℵ‘𝐴))) = 1𝑜)
173164, 172breq12d 4817 . . . . 5 ((ℵ‘𝐴) = ∅ → ((ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑𝑚 (cf‘(ℵ‘𝐴))) ↔ ∅ ≺ 1𝑜))
174163, 173mpbiri 248 . . . 4 ((ℵ‘𝐴) = ∅ → (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑𝑚 (cf‘(ℵ‘𝐴))))
175159, 174syl 17 . . 3 𝐴 ∈ dom ℵ → (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑𝑚 (cf‘(ℵ‘𝐴))))
176158, 175sylnbir 320 . 2 𝐴 ∈ On → (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑𝑚 (cf‘(ℵ‘𝐴))))
177154, 176pm2.61i 176 1 (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑𝑚 (cf‘(ℵ‘𝐴)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 383   ∨ w3o 1071   ∧ w3a 1072   = wceq 1632  ∃wex 1853   ∈ wcel 2139  {cab 2746   ≠ wne 2932  ∀wral 3050  ∃wrex 3051  Vcvv 3340   ⊆ wss 3715  ∅c0 4058  𝒫 cpw 4302  ∪ cuni 4588  ∪ ciun 4672   class class class wbr 4804   ↦ cmpt 4881  dom cdm 5266  ran crn 5267  Oncon0 5884  Lim wlim 5885  suc csuc 5886   Fn wfn 6044  ⟶wf 6045  ‘cfv 6049  (class class class)co 6814  ωcom 7231  Smo wsmo 7612  1𝑜c1o 7723  2𝑜c2o 7724   ↑𝑚 cmap 8025  Xcixp 8076   ≈ cen 8120   ≼ cdom 8121   ≺ csdm 8122  harchar 8628  cardccrd 8971  ℵcale 8972  cfccf 8973 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7115  ax-inf2 8713  ax-ac2 9497 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-int 4628  df-iun 4674  df-iin 4675  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-se 5226  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-isom 6058  df-riota 6775  df-ov 6817  df-oprab 6818  df-mpt2 6819  df-om 7232  df-1st 7334  df-2nd 7335  df-wrecs 7577  df-smo 7613  df-recs 7638  df-rdg 7676  df-1o 7730  df-2o 7731  df-oadd 7734  df-er 7913  df-map 8027  df-ixp 8077  df-en 8124  df-dom 8125  df-sdom 8126  df-fin 8127  df-oi 8582  df-har 8630  df-card 8975  df-aleph 8976  df-cf 8977  df-acn 8978  df-ac 9149 This theorem is referenced by:  cfpwsdom  9618  tskcard  9815  bj-pwcfsdom  33346
 Copyright terms: Public domain W3C validator