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

Theorem pwcfsdom 9998
Description: A corollary of Konig's Theorem konigth 9984. 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 (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑m (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 7545 . . . 4 (𝐴 ∈ On ↔ (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ (𝐴 ∈ V ∧ Lim 𝐴)))
21biimpi 219 . . 3 (𝐴 ∈ On → (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ (𝐴 ∈ V ∧ Lim 𝐴)))
3 cfom 9679 . . . . . . 7 (cf‘ω) = ω
4 aleph0 9481 . . . . . . . 8 (ℵ‘∅) = ω
54fveq2i 6652 . . . . . . 7 (cf‘(ℵ‘∅)) = (cf‘ω)
63, 5, 43eqtr4i 2834 . . . . . 6 (cf‘(ℵ‘∅)) = (ℵ‘∅)
7 2fveq3 6654 . . . . . 6 (𝐴 = ∅ → (cf‘(ℵ‘𝐴)) = (cf‘(ℵ‘∅)))
8 fveq2 6649 . . . . . 6 (𝐴 = ∅ → (ℵ‘𝐴) = (ℵ‘∅))
96, 7, 83eqtr4a 2862 . . . . 5 (𝐴 = ∅ → (cf‘(ℵ‘𝐴)) = (ℵ‘𝐴))
10 fvex 6662 . . . . . . . . 9 (ℵ‘𝐴) ∈ V
1110canth2 8658 . . . . . . . 8 (ℵ‘𝐴) ≺ 𝒫 (ℵ‘𝐴)
1210pw2en 8611 . . . . . . . 8 𝒫 (ℵ‘𝐴) ≈ (2om (ℵ‘𝐴))
13 sdomentr 8639 . . . . . . . 8 (((ℵ‘𝐴) ≺ 𝒫 (ℵ‘𝐴) ∧ 𝒫 (ℵ‘𝐴) ≈ (2om (ℵ‘𝐴))) → (ℵ‘𝐴) ≺ (2om (ℵ‘𝐴)))
1411, 12, 13mp2an 691 . . . . . . 7 (ℵ‘𝐴) ≺ (2om (ℵ‘𝐴))
15 alephon 9484 . . . . . . . . 9 (ℵ‘𝐴) ∈ On
16 alephgeom 9497 . . . . . . . . . 10 (𝐴 ∈ On ↔ ω ⊆ (ℵ‘𝐴))
17 omelon 9097 . . . . . . . . . . . 12 ω ∈ On
18 2onn 8253 . . . . . . . . . . . 12 2o ∈ ω
19 onelss 6205 . . . . . . . . . . . 12 (ω ∈ On → (2o ∈ ω → 2o ⊆ ω))
2017, 18, 19mp2 9 . . . . . . . . . . 11 2o ⊆ ω
21 sstr 3926 . . . . . . . . . . 11 ((2o ⊆ ω ∧ ω ⊆ (ℵ‘𝐴)) → 2o ⊆ (ℵ‘𝐴))
2220, 21mpan 689 . . . . . . . . . 10 (ω ⊆ (ℵ‘𝐴) → 2o ⊆ (ℵ‘𝐴))
2316, 22sylbi 220 . . . . . . . . 9 (𝐴 ∈ On → 2o ⊆ (ℵ‘𝐴))
24 ssdomg 8542 . . . . . . . . 9 ((ℵ‘𝐴) ∈ On → (2o ⊆ (ℵ‘𝐴) → 2o ≼ (ℵ‘𝐴)))
2515, 23, 24mpsyl 68 . . . . . . . 8 (𝐴 ∈ On → 2o ≼ (ℵ‘𝐴))
26 mapdom1 8670 . . . . . . . 8 (2o ≼ (ℵ‘𝐴) → (2om (ℵ‘𝐴)) ≼ ((ℵ‘𝐴) ↑m (ℵ‘𝐴)))
2725, 26syl 17 . . . . . . 7 (𝐴 ∈ On → (2om (ℵ‘𝐴)) ≼ ((ℵ‘𝐴) ↑m (ℵ‘𝐴)))
28 sdomdomtr 8638 . . . . . . 7 (((ℵ‘𝐴) ≺ (2om (ℵ‘𝐴)) ∧ (2om (ℵ‘𝐴)) ≼ ((ℵ‘𝐴) ↑m (ℵ‘𝐴))) → (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑m (ℵ‘𝐴)))
2914, 27, 28sylancr 590 . . . . . 6 (𝐴 ∈ On → (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑m (ℵ‘𝐴)))
30 oveq2 7147 . . . . . . 7 ((cf‘(ℵ‘𝐴)) = (ℵ‘𝐴) → ((ℵ‘𝐴) ↑m (cf‘(ℵ‘𝐴))) = ((ℵ‘𝐴) ↑m (ℵ‘𝐴)))
3130breq2d 5045 . . . . . 6 ((cf‘(ℵ‘𝐴)) = (ℵ‘𝐴) → ((ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑m (cf‘(ℵ‘𝐴))) ↔ (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑m (ℵ‘𝐴))))
3229, 31syl5ibrcom 250 . . . . 5 (𝐴 ∈ On → ((cf‘(ℵ‘𝐴)) = (ℵ‘𝐴) → (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑m (cf‘(ℵ‘𝐴)))))
339, 32syl5 34 . . . 4 (𝐴 ∈ On → (𝐴 = ∅ → (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑m (cf‘(ℵ‘𝐴)))))
34 alephreg 9997 . . . . . . 7 (cf‘(ℵ‘suc 𝑥)) = (ℵ‘suc 𝑥)
35 2fveq3 6654 . . . . . . 7 (𝐴 = suc 𝑥 → (cf‘(ℵ‘𝐴)) = (cf‘(ℵ‘suc 𝑥)))
36 fveq2 6649 . . . . . . 7 (𝐴 = suc 𝑥 → (ℵ‘𝐴) = (ℵ‘suc 𝑥))
3734, 35, 363eqtr4a 2862 . . . . . 6 (𝐴 = suc 𝑥 → (cf‘(ℵ‘𝐴)) = (ℵ‘𝐴))
3837rexlimivw 3244 . . . . 5 (∃𝑥 ∈ On 𝐴 = suc 𝑥 → (cf‘(ℵ‘𝐴)) = (ℵ‘𝐴))
3938, 32syl5 34 . . . 4 (𝐴 ∈ On → (∃𝑥 ∈ On 𝐴 = suc 𝑥 → (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑m (cf‘(ℵ‘𝐴)))))
40 cfsmo 9686 . . . . . 6 ((ℵ‘𝐴) ∈ On → ∃𝑓(𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ Smo 𝑓 ∧ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓𝑤)))
41 limelon 6226 . . . . . . . . . . 11 ((𝐴 ∈ V ∧ Lim 𝐴) → 𝐴 ∈ On)
42 ffn 6491 . . . . . . . . . . . . . . . 16 (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) → 𝑓 Fn (cf‘(ℵ‘𝐴)))
43 fnrnfv 6704 . . . . . . . . . . . . . . . . 17 (𝑓 Fn (cf‘(ℵ‘𝐴)) → ran 𝑓 = {𝑦 ∣ ∃𝑥 ∈ (cf‘(ℵ‘𝐴))𝑦 = (𝑓𝑥)})
4443unieqd 4817 . . . . . . . . . . . . . . . 16 (𝑓 Fn (cf‘(ℵ‘𝐴)) → ran 𝑓 = {𝑦 ∣ ∃𝑥 ∈ (cf‘(ℵ‘𝐴))𝑦 = (𝑓𝑥)})
4542, 44syl 17 . . . . . . . . . . . . . . 15 (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) → ran 𝑓 = {𝑦 ∣ ∃𝑥 ∈ (cf‘(ℵ‘𝐴))𝑦 = (𝑓𝑥)})
46 fvex 6662 . . . . . . . . . . . . . . . 16 (𝑓𝑥) ∈ V
4746dfiun2 4923 . . . . . . . . . . . . . . 15 𝑥 ∈ (cf‘(ℵ‘𝐴))(𝑓𝑥) = {𝑦 ∣ ∃𝑥 ∈ (cf‘(ℵ‘𝐴))𝑦 = (𝑓𝑥)}
4845, 47eqtr4di 2854 . . . . . . . . . . . . . 14 (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) → ran 𝑓 = 𝑥 ∈ (cf‘(ℵ‘𝐴))(𝑓𝑥))
4948ad2antrl 727 . . . . . . . . . . . . 13 ((𝐴 ∈ On ∧ (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓𝑤))) → ran 𝑓 = 𝑥 ∈ (cf‘(ℵ‘𝐴))(𝑓𝑥))
50 fnfvelrn 6829 . . . . . . . . . . . . . . . . . . . 20 ((𝑓 Fn (cf‘(ℵ‘𝐴)) ∧ 𝑤 ∈ (cf‘(ℵ‘𝐴))) → (𝑓𝑤) ∈ ran 𝑓)
5142, 50sylan 583 . . . . . . . . . . . . . . . . . . 19 ((𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ 𝑤 ∈ (cf‘(ℵ‘𝐴))) → (𝑓𝑤) ∈ ran 𝑓)
52 sseq2 3944 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (𝑓𝑤) → (𝑧𝑦𝑧 ⊆ (𝑓𝑤)))
5352rspcev 3574 . . . . . . . . . . . . . . . . . . 19 (((𝑓𝑤) ∈ ran 𝑓𝑧 ⊆ (𝑓𝑤)) → ∃𝑦 ∈ ran 𝑓 𝑧𝑦)
5451, 53sylan 583 . . . . . . . . . . . . . . . . . 18 (((𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ 𝑤 ∈ (cf‘(ℵ‘𝐴))) ∧ 𝑧 ⊆ (𝑓𝑤)) → ∃𝑦 ∈ ran 𝑓 𝑧𝑦)
5554rexlimdva2 3249 . . . . . . . . . . . . . . . . 17 (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) → (∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓𝑤) → ∃𝑦 ∈ ran 𝑓 𝑧𝑦))
5655ralimdv 3148 . . . . . . . . . . . . . . . 16 (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) → (∀𝑧 ∈ (ℵ‘𝐴)∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓𝑤) → ∀𝑧 ∈ (ℵ‘𝐴)∃𝑦 ∈ ran 𝑓 𝑧𝑦))
5756imp 410 . . . . . . . . . . . . . . 15 ((𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓𝑤)) → ∀𝑧 ∈ (ℵ‘𝐴)∃𝑦 ∈ ran 𝑓 𝑧𝑦)
5857adantl 485 . . . . . . . . . . . . . 14 ((𝐴 ∈ On ∧ (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓𝑤))) → ∀𝑧 ∈ (ℵ‘𝐴)∃𝑦 ∈ ran 𝑓 𝑧𝑦)
59 alephislim 9498 . . . . . . . . . . . . . . . 16 (𝐴 ∈ On ↔ Lim (ℵ‘𝐴))
6059biimpi 219 . . . . . . . . . . . . . . 15 (𝐴 ∈ On → Lim (ℵ‘𝐴))
61 frn 6497 . . . . . . . . . . . . . . . 16 (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) → ran 𝑓 ⊆ (ℵ‘𝐴))
6261adantr 484 . . . . . . . . . . . . . . 15 ((𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓𝑤)) → ran 𝑓 ⊆ (ℵ‘𝐴))
63 coflim 9676 . . . . . . . . . . . . . . 15 ((Lim (ℵ‘𝐴) ∧ ran 𝑓 ⊆ (ℵ‘𝐴)) → ( ran 𝑓 = (ℵ‘𝐴) ↔ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑦 ∈ ran 𝑓 𝑧𝑦))
6460, 62, 63syl2an 598 . . . . . . . . . . . . . 14 ((𝐴 ∈ On ∧ (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓𝑤))) → ( ran 𝑓 = (ℵ‘𝐴) ↔ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑦 ∈ ran 𝑓 𝑧𝑦))
6558, 64mpbird 260 . . . . . . . . . . . . 13 ((𝐴 ∈ On ∧ (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓𝑤))) → ran 𝑓 = (ℵ‘𝐴))
6649, 65eqtr3d 2838 . . . . . . . . . . . 12 ((𝐴 ∈ On ∧ (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓𝑤))) → 𝑥 ∈ (cf‘(ℵ‘𝐴))(𝑓𝑥) = (ℵ‘𝐴))
67 ffvelrn 6830 . . . . . . . . . . . . . . . . 17 ((𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ 𝑥 ∈ (cf‘(ℵ‘𝐴))) → (𝑓𝑥) ∈ (ℵ‘𝐴))
6815oneli 6270 . . . . . . . . . . . . . . . . 17 ((𝑓𝑥) ∈ (ℵ‘𝐴) → (𝑓𝑥) ∈ On)
69 harcard 9395 . . . . . . . . . . . . . . . . . . 19 (card‘(har‘(𝑓𝑥))) = (har‘(𝑓𝑥))
70 iscard 9392 . . . . . . . . . . . . . . . . . . . 20 ((card‘(har‘(𝑓𝑥))) = (har‘(𝑓𝑥)) ↔ ((har‘(𝑓𝑥)) ∈ On ∧ ∀𝑦 ∈ (har‘(𝑓𝑥))𝑦 ≺ (har‘(𝑓𝑥))))
7170simprbi 500 . . . . . . . . . . . . . . . . . . 19 ((card‘(har‘(𝑓𝑥))) = (har‘(𝑓𝑥)) → ∀𝑦 ∈ (har‘(𝑓𝑥))𝑦 ≺ (har‘(𝑓𝑥)))
7269, 71ax-mp 5 . . . . . . . . . . . . . . . . . 18 𝑦 ∈ (har‘(𝑓𝑥))𝑦 ≺ (har‘(𝑓𝑥))
73 domrefg 8531 . . . . . . . . . . . . . . . . . . . 20 ((𝑓𝑥) ∈ V → (𝑓𝑥) ≼ (𝑓𝑥))
7446, 73ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (𝑓𝑥) ≼ (𝑓𝑥)
75 elharval 9013 . . . . . . . . . . . . . . . . . . . 20 ((𝑓𝑥) ∈ (har‘(𝑓𝑥)) ↔ ((𝑓𝑥) ∈ On ∧ (𝑓𝑥) ≼ (𝑓𝑥)))
7675biimpri 231 . . . . . . . . . . . . . . . . . . 19 (((𝑓𝑥) ∈ On ∧ (𝑓𝑥) ≼ (𝑓𝑥)) → (𝑓𝑥) ∈ (har‘(𝑓𝑥)))
7774, 76mpan2 690 . . . . . . . . . . . . . . . . . 18 ((𝑓𝑥) ∈ On → (𝑓𝑥) ∈ (har‘(𝑓𝑥)))
78 breq1 5036 . . . . . . . . . . . . . . . . . . 19 (𝑦 = (𝑓𝑥) → (𝑦 ≺ (har‘(𝑓𝑥)) ↔ (𝑓𝑥) ≺ (har‘(𝑓𝑥))))
7978rspccv 3571 . . . . . . . . . . . . . . . . . 18 (∀𝑦 ∈ (har‘(𝑓𝑥))𝑦 ≺ (har‘(𝑓𝑥)) → ((𝑓𝑥) ∈ (har‘(𝑓𝑥)) → (𝑓𝑥) ≺ (har‘(𝑓𝑥))))
8072, 77, 79mpsyl 68 . . . . . . . . . . . . . . . . 17 ((𝑓𝑥) ∈ On → (𝑓𝑥) ≺ (har‘(𝑓𝑥)))
8167, 68, 803syl 18 . . . . . . . . . . . . . . . 16 ((𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ 𝑥 ∈ (cf‘(ℵ‘𝐴))) → (𝑓𝑥) ≺ (har‘(𝑓𝑥)))
82 harcl 9011 . . . . . . . . . . . . . . . . . . 19 (har‘(𝑓𝑥)) ∈ On
83 2fveq3 6654 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑥 → (har‘(𝑓𝑦)) = (har‘(𝑓𝑥)))
84 pwcfsdom.1 . . . . . . . . . . . . . . . . . . . 20 𝐻 = (𝑦 ∈ (cf‘(ℵ‘𝐴)) ↦ (har‘(𝑓𝑦)))
8583, 84fvmptg 6747 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (cf‘(ℵ‘𝐴)) ∧ (har‘(𝑓𝑥)) ∈ On) → (𝐻𝑥) = (har‘(𝑓𝑥)))
8682, 85mpan2 690 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (cf‘(ℵ‘𝐴)) → (𝐻𝑥) = (har‘(𝑓𝑥)))
8786breq2d 5045 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (cf‘(ℵ‘𝐴)) → ((𝑓𝑥) ≺ (𝐻𝑥) ↔ (𝑓𝑥) ≺ (har‘(𝑓𝑥))))
8887adantl 485 . . . . . . . . . . . . . . . 16 ((𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ 𝑥 ∈ (cf‘(ℵ‘𝐴))) → ((𝑓𝑥) ≺ (𝐻𝑥) ↔ (𝑓𝑥) ≺ (har‘(𝑓𝑥))))
8981, 88mpbird 260 . . . . . . . . . . . . . . 15 ((𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ 𝑥 ∈ (cf‘(ℵ‘𝐴))) → (𝑓𝑥) ≺ (𝐻𝑥))
9089ralrimiva 3152 . . . . . . . . . . . . . 14 (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) → ∀𝑥 ∈ (cf‘(ℵ‘𝐴))(𝑓𝑥) ≺ (𝐻𝑥))
91 fvex 6662 . . . . . . . . . . . . . . 15 (cf‘(ℵ‘𝐴)) ∈ V
92 eqid 2801 . . . . . . . . . . . . . . 15 𝑥 ∈ (cf‘(ℵ‘𝐴))(𝑓𝑥) = 𝑥 ∈ (cf‘(ℵ‘𝐴))(𝑓𝑥)
93 eqid 2801 . . . . . . . . . . . . . . 15 X𝑥 ∈ (cf‘(ℵ‘𝐴))(𝐻𝑥) = X𝑥 ∈ (cf‘(ℵ‘𝐴))(𝐻𝑥)
9491, 92, 93konigth 9984 . . . . . . . . . . . . . 14 (∀𝑥 ∈ (cf‘(ℵ‘𝐴))(𝑓𝑥) ≺ (𝐻𝑥) → 𝑥 ∈ (cf‘(ℵ‘𝐴))(𝑓𝑥) ≺ X𝑥 ∈ (cf‘(ℵ‘𝐴))(𝐻𝑥))
9590, 94syl 17 . . . . . . . . . . . . 13 (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) → 𝑥 ∈ (cf‘(ℵ‘𝐴))(𝑓𝑥) ≺ X𝑥 ∈ (cf‘(ℵ‘𝐴))(𝐻𝑥))
9695ad2antrl 727 . . . . . . . . . . . 12 ((𝐴 ∈ On ∧ (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓𝑤))) → 𝑥 ∈ (cf‘(ℵ‘𝐴))(𝑓𝑥) ≺ X𝑥 ∈ (cf‘(ℵ‘𝐴))(𝐻𝑥))
9766, 96eqbrtrrd 5057 . . . . . . . . . . 11 ((𝐴 ∈ On ∧ (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓𝑤))) → (ℵ‘𝐴) ≺ X𝑥 ∈ (cf‘(ℵ‘𝐴))(𝐻𝑥))
9841, 97sylan 583 . . . . . . . . . 10 (((𝐴 ∈ V ∧ Lim 𝐴) ∧ (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓𝑤))) → (ℵ‘𝐴) ≺ X𝑥 ∈ (cf‘(ℵ‘𝐴))(𝐻𝑥))
99 ovex 7172 . . . . . . . . . . . 12 ((ℵ‘𝐴) ↑m (cf‘(ℵ‘𝐴))) ∈ V
10067ex 416 . . . . . . . . . . . . . . . 16 (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) → (𝑥 ∈ (cf‘(ℵ‘𝐴)) → (𝑓𝑥) ∈ (ℵ‘𝐴)))
101 alephlim 9482 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ V ∧ Lim 𝐴) → (ℵ‘𝐴) = 𝑦𝐴 (ℵ‘𝑦))
102101eleq2d 2878 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ V ∧ Lim 𝐴) → ((𝑓𝑥) ∈ (ℵ‘𝐴) ↔ (𝑓𝑥) ∈ 𝑦𝐴 (ℵ‘𝑦)))
103 eliun 4888 . . . . . . . . . . . . . . . . . . 19 ((𝑓𝑥) ∈ 𝑦𝐴 (ℵ‘𝑦) ↔ ∃𝑦𝐴 (𝑓𝑥) ∈ (ℵ‘𝑦))
104 alephcard 9485 . . . . . . . . . . . . . . . . . . . . . . . 24 (card‘(ℵ‘𝑦)) = (ℵ‘𝑦)
105104eleq2i 2884 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑓𝑥) ∈ (card‘(ℵ‘𝑦)) ↔ (𝑓𝑥) ∈ (ℵ‘𝑦))
106 cardsdomelir 9390 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑓𝑥) ∈ (card‘(ℵ‘𝑦)) → (𝑓𝑥) ≺ (ℵ‘𝑦))
107105, 106sylbir 238 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓𝑥) ∈ (ℵ‘𝑦) → (𝑓𝑥) ≺ (ℵ‘𝑦))
108 elharval 9013 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((ℵ‘𝑦) ∈ (har‘(𝑓𝑥)) ↔ ((ℵ‘𝑦) ∈ On ∧ (ℵ‘𝑦) ≼ (𝑓𝑥)))
109108simprbi 500 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((ℵ‘𝑦) ∈ (har‘(𝑓𝑥)) → (ℵ‘𝑦) ≼ (𝑓𝑥))
110 domnsym 8631 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((ℵ‘𝑦) ≼ (𝑓𝑥) → ¬ (𝑓𝑥) ≺ (ℵ‘𝑦))
111109, 110syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((ℵ‘𝑦) ∈ (har‘(𝑓𝑥)) → ¬ (𝑓𝑥) ≺ (ℵ‘𝑦))
112111con2i 141 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑓𝑥) ≺ (ℵ‘𝑦) → ¬ (ℵ‘𝑦) ∈ (har‘(𝑓𝑥)))
113 alephon 9484 . . . . . . . . . . . . . . . . . . . . . . . 24 (ℵ‘𝑦) ∈ On
114 ontri1 6197 . . . . . . . . . . . . . . . . . . . . . . . 24 (((har‘(𝑓𝑥)) ∈ On ∧ (ℵ‘𝑦) ∈ On) → ((har‘(𝑓𝑥)) ⊆ (ℵ‘𝑦) ↔ ¬ (ℵ‘𝑦) ∈ (har‘(𝑓𝑥))))
11582, 113, 114mp2an 691 . . . . . . . . . . . . . . . . . . . . . . 23 ((har‘(𝑓𝑥)) ⊆ (ℵ‘𝑦) ↔ ¬ (ℵ‘𝑦) ∈ (har‘(𝑓𝑥)))
116112, 115sylibr 237 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓𝑥) ≺ (ℵ‘𝑦) → (har‘(𝑓𝑥)) ⊆ (ℵ‘𝑦))
117107, 116syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝑓𝑥) ∈ (ℵ‘𝑦) → (har‘(𝑓𝑥)) ⊆ (ℵ‘𝑦))
118 alephord2i 9492 . . . . . . . . . . . . . . . . . . . . . 22 (𝐴 ∈ On → (𝑦𝐴 → (ℵ‘𝑦) ∈ (ℵ‘𝐴)))
119118imp 410 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴 ∈ On ∧ 𝑦𝐴) → (ℵ‘𝑦) ∈ (ℵ‘𝐴))
120 ontr2 6210 . . . . . . . . . . . . . . . . . . . . . 22 (((har‘(𝑓𝑥)) ∈ On ∧ (ℵ‘𝐴) ∈ On) → (((har‘(𝑓𝑥)) ⊆ (ℵ‘𝑦) ∧ (ℵ‘𝑦) ∈ (ℵ‘𝐴)) → (har‘(𝑓𝑥)) ∈ (ℵ‘𝐴)))
12182, 15, 120mp2an 691 . . . . . . . . . . . . . . . . . . . . 21 (((har‘(𝑓𝑥)) ⊆ (ℵ‘𝑦) ∧ (ℵ‘𝑦) ∈ (ℵ‘𝐴)) → (har‘(𝑓𝑥)) ∈ (ℵ‘𝐴))
122117, 119, 121syl2anr 599 . . . . . . . . . . . . . . . . . . . 20 (((𝐴 ∈ On ∧ 𝑦𝐴) ∧ (𝑓𝑥) ∈ (ℵ‘𝑦)) → (har‘(𝑓𝑥)) ∈ (ℵ‘𝐴))
123122rexlimdva2 3249 . . . . . . . . . . . . . . . . . . 19 (𝐴 ∈ On → (∃𝑦𝐴 (𝑓𝑥) ∈ (ℵ‘𝑦) → (har‘(𝑓𝑥)) ∈ (ℵ‘𝐴)))
124103, 123syl5bi 245 . . . . . . . . . . . . . . . . . 18 (𝐴 ∈ On → ((𝑓𝑥) ∈ 𝑦𝐴 (ℵ‘𝑦) → (har‘(𝑓𝑥)) ∈ (ℵ‘𝐴)))
12541, 124syl 17 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ V ∧ Lim 𝐴) → ((𝑓𝑥) ∈ 𝑦𝐴 (ℵ‘𝑦) → (har‘(𝑓𝑥)) ∈ (ℵ‘𝐴)))
126102, 125sylbid 243 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ V ∧ Lim 𝐴) → ((𝑓𝑥) ∈ (ℵ‘𝐴) → (har‘(𝑓𝑥)) ∈ (ℵ‘𝐴)))
127100, 126sylan9r 512 . . . . . . . . . . . . . . 15 (((𝐴 ∈ V ∧ Lim 𝐴) ∧ 𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴)) → (𝑥 ∈ (cf‘(ℵ‘𝐴)) → (har‘(𝑓𝑥)) ∈ (ℵ‘𝐴)))
128127imp 410 . . . . . . . . . . . . . 14 ((((𝐴 ∈ V ∧ Lim 𝐴) ∧ 𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴)) ∧ 𝑥 ∈ (cf‘(ℵ‘𝐴))) → (har‘(𝑓𝑥)) ∈ (ℵ‘𝐴))
12983cbvmptv 5136 . . . . . . . . . . . . . . 15 (𝑦 ∈ (cf‘(ℵ‘𝐴)) ↦ (har‘(𝑓𝑦))) = (𝑥 ∈ (cf‘(ℵ‘𝐴)) ↦ (har‘(𝑓𝑥)))
13084, 129eqtri 2824 . . . . . . . . . . . . . 14 𝐻 = (𝑥 ∈ (cf‘(ℵ‘𝐴)) ↦ (har‘(𝑓𝑥)))
131128, 130fmptd 6859 . . . . . . . . . . . . 13 (((𝐴 ∈ V ∧ Lim 𝐴) ∧ 𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴)) → 𝐻:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴))
132 ffvelrn 6830 . . . . . . . . . . . . . . 15 ((𝐻:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ 𝑥 ∈ (cf‘(ℵ‘𝐴))) → (𝐻𝑥) ∈ (ℵ‘𝐴))
133 onelss 6205 . . . . . . . . . . . . . . 15 ((ℵ‘𝐴) ∈ On → ((𝐻𝑥) ∈ (ℵ‘𝐴) → (𝐻𝑥) ⊆ (ℵ‘𝐴)))
13415, 132, 133mpsyl 68 . . . . . . . . . . . . . 14 ((𝐻:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ 𝑥 ∈ (cf‘(ℵ‘𝐴))) → (𝐻𝑥) ⊆ (ℵ‘𝐴))
135134ralrimiva 3152 . . . . . . . . . . . . 13 (𝐻:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) → ∀𝑥 ∈ (cf‘(ℵ‘𝐴))(𝐻𝑥) ⊆ (ℵ‘𝐴))
136 ss2ixp 8461 . . . . . . . . . . . . . 14 (∀𝑥 ∈ (cf‘(ℵ‘𝐴))(𝐻𝑥) ⊆ (ℵ‘𝐴) → X𝑥 ∈ (cf‘(ℵ‘𝐴))(𝐻𝑥) ⊆ X𝑥 ∈ (cf‘(ℵ‘𝐴))(ℵ‘𝐴))
13791, 10ixpconst 8458 . . . . . . . . . . . . . 14 X𝑥 ∈ (cf‘(ℵ‘𝐴))(ℵ‘𝐴) = ((ℵ‘𝐴) ↑m (cf‘(ℵ‘𝐴)))
138136, 137sseqtrdi 3968 . . . . . . . . . . . . 13 (∀𝑥 ∈ (cf‘(ℵ‘𝐴))(𝐻𝑥) ⊆ (ℵ‘𝐴) → X𝑥 ∈ (cf‘(ℵ‘𝐴))(𝐻𝑥) ⊆ ((ℵ‘𝐴) ↑m (cf‘(ℵ‘𝐴))))
139131, 135, 1383syl 18 . . . . . . . . . . . 12 (((𝐴 ∈ V ∧ Lim 𝐴) ∧ 𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴)) → X𝑥 ∈ (cf‘(ℵ‘𝐴))(𝐻𝑥) ⊆ ((ℵ‘𝐴) ↑m (cf‘(ℵ‘𝐴))))
140 ssdomg 8542 . . . . . . . . . . . 12 (((ℵ‘𝐴) ↑m (cf‘(ℵ‘𝐴))) ∈ V → (X𝑥 ∈ (cf‘(ℵ‘𝐴))(𝐻𝑥) ⊆ ((ℵ‘𝐴) ↑m (cf‘(ℵ‘𝐴))) → X𝑥 ∈ (cf‘(ℵ‘𝐴))(𝐻𝑥) ≼ ((ℵ‘𝐴) ↑m (cf‘(ℵ‘𝐴)))))
14199, 139, 140mpsyl 68 . . . . . . . . . . 11 (((𝐴 ∈ V ∧ Lim 𝐴) ∧ 𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴)) → X𝑥 ∈ (cf‘(ℵ‘𝐴))(𝐻𝑥) ≼ ((ℵ‘𝐴) ↑m (cf‘(ℵ‘𝐴))))
142141adantrr 716 . . . . . . . . . 10 (((𝐴 ∈ V ∧ Lim 𝐴) ∧ (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓𝑤))) → X𝑥 ∈ (cf‘(ℵ‘𝐴))(𝐻𝑥) ≼ ((ℵ‘𝐴) ↑m (cf‘(ℵ‘𝐴))))
143 sdomdomtr 8638 . . . . . . . . . 10 (((ℵ‘𝐴) ≺ X𝑥 ∈ (cf‘(ℵ‘𝐴))(𝐻𝑥) ∧ X𝑥 ∈ (cf‘(ℵ‘𝐴))(𝐻𝑥) ≼ ((ℵ‘𝐴) ↑m (cf‘(ℵ‘𝐴)))) → (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑m (cf‘(ℵ‘𝐴))))
14498, 142, 143syl2anc 587 . . . . . . . . 9 (((𝐴 ∈ V ∧ Lim 𝐴) ∧ (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓𝑤))) → (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑m (cf‘(ℵ‘𝐴))))
145144expcom 417 . . . . . . . 8 ((𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓𝑤)) → ((𝐴 ∈ V ∧ Lim 𝐴) → (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑m (cf‘(ℵ‘𝐴)))))
1461453adant2 1128 . . . . . . 7 ((𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ Smo 𝑓 ∧ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓𝑤)) → ((𝐴 ∈ V ∧ Lim 𝐴) → (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑m (cf‘(ℵ‘𝐴)))))
147146exlimiv 1931 . . . . . 6 (∃𝑓(𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ Smo 𝑓 ∧ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓𝑤)) → ((𝐴 ∈ V ∧ Lim 𝐴) → (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑m (cf‘(ℵ‘𝐴)))))
14815, 40, 147mp2b 10 . . . . 5 ((𝐴 ∈ V ∧ Lim 𝐴) → (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑m (cf‘(ℵ‘𝐴))))
149148a1i 11 . . . 4 (𝐴 ∈ On → ((𝐴 ∈ V ∧ Lim 𝐴) → (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑m (cf‘(ℵ‘𝐴)))))
15033, 39, 1493jaod 1425 . . 3 (𝐴 ∈ On → ((𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ (𝐴 ∈ V ∧ Lim 𝐴)) → (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑m (cf‘(ℵ‘𝐴)))))
1512, 150mpd 15 . 2 (𝐴 ∈ On → (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑m (cf‘(ℵ‘𝐴))))
152 alephfnon 9480 . . . . 5 ℵ Fn On
153152fndmi 6430 . . . 4 dom ℵ = On
154153eleq2i 2884 . . 3 (𝐴 ∈ dom ℵ ↔ 𝐴 ∈ On)
155 ndmfv 6679 . . . 4 𝐴 ∈ dom ℵ → (ℵ‘𝐴) = ∅)
156 1n0 8106 . . . . . 6 1o ≠ ∅
157 1oex 8097 . . . . . . 7 1o ∈ V
1581570sdom 8636 . . . . . 6 (∅ ≺ 1o ↔ 1o ≠ ∅)
159156, 158mpbir 234 . . . . 5 ∅ ≺ 1o
160 id 22 . . . . . 6 ((ℵ‘𝐴) = ∅ → (ℵ‘𝐴) = ∅)
161 fveq2 6649 . . . . . . . . 9 ((ℵ‘𝐴) = ∅ → (cf‘(ℵ‘𝐴)) = (cf‘∅))
162 cf0 9666 . . . . . . . . 9 (cf‘∅) = ∅
163161, 162eqtrdi 2852 . . . . . . . 8 ((ℵ‘𝐴) = ∅ → (cf‘(ℵ‘𝐴)) = ∅)
164160, 163oveq12d 7157 . . . . . . 7 ((ℵ‘𝐴) = ∅ → ((ℵ‘𝐴) ↑m (cf‘(ℵ‘𝐴))) = (∅ ↑m ∅))
165 0ex 5178 . . . . . . . 8 ∅ ∈ V
166 map0e 8433 . . . . . . . 8 (∅ ∈ V → (∅ ↑m ∅) = 1o)
167165, 166ax-mp 5 . . . . . . 7 (∅ ↑m ∅) = 1o
168164, 167eqtrdi 2852 . . . . . 6 ((ℵ‘𝐴) = ∅ → ((ℵ‘𝐴) ↑m (cf‘(ℵ‘𝐴))) = 1o)
169160, 168breq12d 5046 . . . . 5 ((ℵ‘𝐴) = ∅ → ((ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑m (cf‘(ℵ‘𝐴))) ↔ ∅ ≺ 1o))
170159, 169mpbiri 261 . . . 4 ((ℵ‘𝐴) = ∅ → (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑m (cf‘(ℵ‘𝐴))))
171155, 170syl 17 . . 3 𝐴 ∈ dom ℵ → (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑m (cf‘(ℵ‘𝐴))))
172154, 171sylnbir 334 . 2 𝐴 ∈ On → (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑m (cf‘(ℵ‘𝐴))))
173151, 172pm2.61i 185 1 (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑m (cf‘(ℵ‘𝐴)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  w3o 1083  w3a 1084   = wceq 1538  wex 1781  wcel 2112  {cab 2779  wne 2990  wral 3109  wrex 3110  Vcvv 3444  wss 3884  c0 4246  𝒫 cpw 4500   cuni 4803   ciun 4884   class class class wbr 5033  cmpt 5113  dom cdm 5523  ran crn 5524  Oncon0 6163  Lim wlim 6164  suc csuc 6165   Fn wfn 6323  wf 6324  cfv 6328  (class class class)co 7139  ωcom 7564  Smo wsmo 7969  1oc1o 8082  2oc2o 8083  m cmap 8393  Xcixp 8448  cen 8493  cdom 8494  csdm 8495  harchar 9008  cardccrd 9352  cale 9353  cfccf 9354
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445  ax-inf2 9092  ax-ac2 9878
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-ral 3114  df-rex 3115  df-reu 3116  df-rmo 3117  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4804  df-int 4842  df-iun 4886  df-iin 4887  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5442  df-so 5443  df-fr 5482  df-se 5483  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6120  df-ord 6166  df-on 6167  df-lim 6168  df-suc 6169  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-isom 6337  df-riota 7097  df-ov 7142  df-oprab 7143  df-mpo 7144  df-om 7565  df-1st 7675  df-2nd 7676  df-wrecs 7934  df-smo 7970  df-recs 7995  df-rdg 8033  df-1o 8089  df-2o 8090  df-oadd 8093  df-er 8276  df-map 8395  df-ixp 8449  df-en 8497  df-dom 8498  df-sdom 8499  df-fin 8500  df-oi 8962  df-har 9009  df-card 9356  df-aleph 9357  df-cf 9358  df-acn 9359  df-ac 9531
This theorem is referenced by:  cfpwsdom  9999  tskcard  10196  bj-pwcfsdom  34474
  Copyright terms: Public domain W3C validator