Step | Hyp | Ref
| Expression |
1 | | reldom 7961 |
. . 3
⊢ Rel
≼ |
2 | 1 | brrelex2i 5159 |
. 2
⊢ (ω
≼ 𝐴 → 𝐴 ∈ V) |
3 | | domeng 7969 |
. . 3
⊢ (𝐴 ∈ V → (ω
≼ 𝐴 ↔
∃𝑡(ω ≈
𝑡 ∧ 𝑡 ⊆ 𝐴))) |
4 | | bren 7964 |
. . . . . 6
⊢ (ω
≈ 𝑡 ↔
∃ℎ ℎ:ω–1-1-onto→𝑡) |
5 | | harcl 8466 |
. . . . . . . . . 10
⊢
(har‘𝒫 𝐴) ∈ On |
6 | | infxpenc2 8845 |
. . . . . . . . . 10
⊢
((har‘𝒫 𝐴) ∈ On → ∃𝑚∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) |
7 | 5, 6 | ax-mp 5 |
. . . . . . . . 9
⊢
∃𝑚∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏) |
8 | | simpr 477 |
. . . . . . . . . . . . . . . 16
⊢ ((((ℎ:ω–1-1-onto→𝑡 ∧ 𝑡 ⊆ 𝐴) ∧ ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) ∧ 𝑔:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑𝑚
𝑛)) → 𝑔:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑𝑚
𝑛)) |
9 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑘 → (𝐴 ↑𝑚 𝑛) = (𝐴 ↑𝑚 𝑘)) |
10 | 9 | cbviunv 4559 |
. . . . . . . . . . . . . . . . 17
⊢ ∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛) = ∪ 𝑘 ∈ ω (𝐴 ↑𝑚 𝑘) |
11 | | f1eq3 6098 |
. . . . . . . . . . . . . . . . 17
⊢ (∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛) = ∪ 𝑘 ∈ ω (𝐴 ↑𝑚 𝑘) → (𝑔:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑𝑚
𝑛) ↔ 𝑔:𝒫 𝐴–1-1→∪ 𝑘 ∈ ω (𝐴 ↑𝑚
𝑘))) |
12 | 10, 11 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑𝑚
𝑛) ↔ 𝑔:𝒫 𝐴–1-1→∪ 𝑘 ∈ ω (𝐴 ↑𝑚
𝑘)) |
13 | 8, 12 | sylib 208 |
. . . . . . . . . . . . . . 15
⊢ ((((ℎ:ω–1-1-onto→𝑡 ∧ 𝑡 ⊆ 𝐴) ∧ ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) ∧ 𝑔:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑𝑚
𝑛)) → 𝑔:𝒫 𝐴–1-1→∪ 𝑘 ∈ ω (𝐴 ↑𝑚
𝑘)) |
14 | | simpllr 799 |
. . . . . . . . . . . . . . 15
⊢ ((((ℎ:ω–1-1-onto→𝑡 ∧ 𝑡 ⊆ 𝐴) ∧ ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) ∧ 𝑔:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑𝑚
𝑛)) → 𝑡 ⊆ 𝐴) |
15 | | simplll 798 |
. . . . . . . . . . . . . . 15
⊢ ((((ℎ:ω–1-1-onto→𝑡 ∧ 𝑡 ⊆ 𝐴) ∧ ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) ∧ 𝑔:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑𝑚
𝑛)) → ℎ:ω–1-1-onto→𝑡) |
16 | | biid 251 |
. . . . . . . . . . . . . . 15
⊢ (((𝑢 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑢 × 𝑢) ∧ 𝑟 We 𝑢) ∧ ω ≼ 𝑢) ↔ ((𝑢 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑢 × 𝑢) ∧ 𝑟 We 𝑢) ∧ ω ≼ 𝑢)) |
17 | | simplr 792 |
. . . . . . . . . . . . . . . 16
⊢ ((((ℎ:ω–1-1-onto→𝑡 ∧ 𝑡 ⊆ 𝐴) ∧ ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) ∧ 𝑔:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑𝑚
𝑛)) → ∀𝑏 ∈ (har‘𝒫
𝐴)(ω ⊆ 𝑏 → (𝑚‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) |
18 | | sseq2 3627 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 = 𝑤 → (ω ⊆ 𝑏 ↔ ω ⊆ 𝑤)) |
19 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑏 = 𝑤 → (𝑚‘𝑏) = (𝑚‘𝑤)) |
20 | | f1oeq1 6127 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑚‘𝑏) = (𝑚‘𝑤) → ((𝑚‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏 ↔ (𝑚‘𝑤):(𝑏 × 𝑏)–1-1-onto→𝑏)) |
21 | 19, 20 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑏 = 𝑤 → ((𝑚‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏 ↔ (𝑚‘𝑤):(𝑏 × 𝑏)–1-1-onto→𝑏)) |
22 | | xpeq12 5134 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑏 = 𝑤 ∧ 𝑏 = 𝑤) → (𝑏 × 𝑏) = (𝑤 × 𝑤)) |
23 | 22 | anidms 677 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑏 = 𝑤 → (𝑏 × 𝑏) = (𝑤 × 𝑤)) |
24 | | f1oeq2 6128 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑏 × 𝑏) = (𝑤 × 𝑤) → ((𝑚‘𝑤):(𝑏 × 𝑏)–1-1-onto→𝑏 ↔ (𝑚‘𝑤):(𝑤 × 𝑤)–1-1-onto→𝑏)) |
25 | 23, 24 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑏 = 𝑤 → ((𝑚‘𝑤):(𝑏 × 𝑏)–1-1-onto→𝑏 ↔ (𝑚‘𝑤):(𝑤 × 𝑤)–1-1-onto→𝑏)) |
26 | | f1oeq3 6129 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑏 = 𝑤 → ((𝑚‘𝑤):(𝑤 × 𝑤)–1-1-onto→𝑏 ↔ (𝑚‘𝑤):(𝑤 × 𝑤)–1-1-onto→𝑤)) |
27 | 21, 25, 26 | 3bitrd 294 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 = 𝑤 → ((𝑚‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏 ↔ (𝑚‘𝑤):(𝑤 × 𝑤)–1-1-onto→𝑤)) |
28 | 18, 27 | imbi12d 334 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = 𝑤 → ((ω ⊆ 𝑏 → (𝑚‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏) ↔ (ω ⊆ 𝑤 → (𝑚‘𝑤):(𝑤 × 𝑤)–1-1-onto→𝑤))) |
29 | 28 | cbvralv 3171 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑏 ∈
(har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏) ↔ ∀𝑤 ∈ (har‘𝒫
𝐴)(ω ⊆ 𝑤 → (𝑚‘𝑤):(𝑤 × 𝑤)–1-1-onto→𝑤)) |
30 | 17, 29 | sylib 208 |
. . . . . . . . . . . . . . 15
⊢ ((((ℎ:ω–1-1-onto→𝑡 ∧ 𝑡 ⊆ 𝐴) ∧ ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) ∧ 𝑔:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑𝑚
𝑛)) → ∀𝑤 ∈ (har‘𝒫
𝐴)(ω ⊆ 𝑤 → (𝑚‘𝑤):(𝑤 × 𝑤)–1-1-onto→𝑤)) |
31 | | eqid 2622 |
. . . . . . . . . . . . . . 15
⊢
OrdIso(𝑟, 𝑢) = OrdIso(𝑟, 𝑢) |
32 | | eqid 2622 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 ∈ dom OrdIso(𝑟, 𝑢), 𝑧 ∈ dom OrdIso(𝑟, 𝑢) ↦ 〈(OrdIso(𝑟, 𝑢)‘𝑠), (OrdIso(𝑟, 𝑢)‘𝑧)〉) = (𝑠 ∈ dom OrdIso(𝑟, 𝑢), 𝑧 ∈ dom OrdIso(𝑟, 𝑢) ↦ 〈(OrdIso(𝑟, 𝑢)‘𝑠), (OrdIso(𝑟, 𝑢)‘𝑧)〉) |
33 | | eqid 2622 |
. . . . . . . . . . . . . . 15
⊢
((OrdIso(𝑟, 𝑢) ∘ (𝑚‘dom OrdIso(𝑟, 𝑢))) ∘ ◡(𝑠 ∈ dom OrdIso(𝑟, 𝑢), 𝑧 ∈ dom OrdIso(𝑟, 𝑢) ↦ 〈(OrdIso(𝑟, 𝑢)‘𝑠), (OrdIso(𝑟, 𝑢)‘𝑧)〉)) = ((OrdIso(𝑟, 𝑢) ∘ (𝑚‘dom OrdIso(𝑟, 𝑢))) ∘ ◡(𝑠 ∈ dom OrdIso(𝑟, 𝑢), 𝑧 ∈ dom OrdIso(𝑟, 𝑢) ↦ 〈(OrdIso(𝑟, 𝑢)‘𝑠), (OrdIso(𝑟, 𝑢)‘𝑧)〉)) |
34 | | eqid 2622 |
. . . . . . . . . . . . . . 15
⊢
seq𝜔((𝑝 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝑢 ↑𝑚 suc 𝑝) ↦ ((𝑓‘(𝑥 ↾ 𝑝))((OrdIso(𝑟, 𝑢) ∘ (𝑚‘dom OrdIso(𝑟, 𝑢))) ∘ ◡(𝑠 ∈ dom OrdIso(𝑟, 𝑢), 𝑧 ∈ dom OrdIso(𝑟, 𝑢) ↦ 〈(OrdIso(𝑟, 𝑢)‘𝑠), (OrdIso(𝑟, 𝑢)‘𝑧)〉))(𝑥‘𝑝)))), {〈∅, (OrdIso(𝑟, 𝑢)‘∅)〉}) =
seq𝜔((𝑝
∈ V, 𝑓 ∈ V
↦ (𝑥 ∈ (𝑢 ↑𝑚 suc
𝑝) ↦ ((𝑓‘(𝑥 ↾ 𝑝))((OrdIso(𝑟, 𝑢) ∘ (𝑚‘dom OrdIso(𝑟, 𝑢))) ∘ ◡(𝑠 ∈ dom OrdIso(𝑟, 𝑢), 𝑧 ∈ dom OrdIso(𝑟, 𝑢) ↦ 〈(OrdIso(𝑟, 𝑢)‘𝑠), (OrdIso(𝑟, 𝑢)‘𝑧)〉))(𝑥‘𝑝)))), {〈∅, (OrdIso(𝑟, 𝑢)‘∅)〉}) |
35 | | oveq2 6658 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑘 → (𝑢 ↑𝑚 𝑛) = (𝑢 ↑𝑚 𝑘)) |
36 | 35 | cbviunv 4559 |
. . . . . . . . . . . . . . . 16
⊢ ∪ 𝑛 ∈ ω (𝑢 ↑𝑚 𝑛) = ∪ 𝑘 ∈ ω (𝑢 ↑𝑚 𝑘) |
37 | | mpteq1 4737 |
. . . . . . . . . . . . . . . 16
⊢ (∪ 𝑛 ∈ ω (𝑢 ↑𝑚 𝑛) = ∪ 𝑘 ∈ ω (𝑢 ↑𝑚 𝑘) → (𝑦 ∈ ∪
𝑛 ∈ ω (𝑢 ↑𝑚
𝑛) ↦ 〈dom 𝑦,
((seq𝜔((𝑝 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝑢 ↑𝑚 suc 𝑝) ↦ ((𝑓‘(𝑥 ↾ 𝑝))((OrdIso(𝑟, 𝑢) ∘ (𝑚‘dom OrdIso(𝑟, 𝑢))) ∘ ◡(𝑠 ∈ dom OrdIso(𝑟, 𝑢), 𝑧 ∈ dom OrdIso(𝑟, 𝑢) ↦ 〈(OrdIso(𝑟, 𝑢)‘𝑠), (OrdIso(𝑟, 𝑢)‘𝑧)〉))(𝑥‘𝑝)))), {〈∅, (OrdIso(𝑟, 𝑢)‘∅)〉})‘dom 𝑦)‘𝑦)〉) = (𝑦 ∈ ∪
𝑘 ∈ ω (𝑢 ↑𝑚
𝑘) ↦ 〈dom 𝑦,
((seq𝜔((𝑝 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝑢 ↑𝑚 suc 𝑝) ↦ ((𝑓‘(𝑥 ↾ 𝑝))((OrdIso(𝑟, 𝑢) ∘ (𝑚‘dom OrdIso(𝑟, 𝑢))) ∘ ◡(𝑠 ∈ dom OrdIso(𝑟, 𝑢), 𝑧 ∈ dom OrdIso(𝑟, 𝑢) ↦ 〈(OrdIso(𝑟, 𝑢)‘𝑠), (OrdIso(𝑟, 𝑢)‘𝑧)〉))(𝑥‘𝑝)))), {〈∅, (OrdIso(𝑟, 𝑢)‘∅)〉})‘dom 𝑦)‘𝑦)〉)) |
38 | 36, 37 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ∪ 𝑛 ∈ ω (𝑢 ↑𝑚 𝑛) ↦ 〈dom 𝑦,
((seq𝜔((𝑝 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝑢 ↑𝑚 suc 𝑝) ↦ ((𝑓‘(𝑥 ↾ 𝑝))((OrdIso(𝑟, 𝑢) ∘ (𝑚‘dom OrdIso(𝑟, 𝑢))) ∘ ◡(𝑠 ∈ dom OrdIso(𝑟, 𝑢), 𝑧 ∈ dom OrdIso(𝑟, 𝑢) ↦ 〈(OrdIso(𝑟, 𝑢)‘𝑠), (OrdIso(𝑟, 𝑢)‘𝑧)〉))(𝑥‘𝑝)))), {〈∅, (OrdIso(𝑟, 𝑢)‘∅)〉})‘dom 𝑦)‘𝑦)〉) = (𝑦 ∈ ∪
𝑘 ∈ ω (𝑢 ↑𝑚
𝑘) ↦ 〈dom 𝑦,
((seq𝜔((𝑝 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝑢 ↑𝑚 suc 𝑝) ↦ ((𝑓‘(𝑥 ↾ 𝑝))((OrdIso(𝑟, 𝑢) ∘ (𝑚‘dom OrdIso(𝑟, 𝑢))) ∘ ◡(𝑠 ∈ dom OrdIso(𝑟, 𝑢), 𝑧 ∈ dom OrdIso(𝑟, 𝑢) ↦ 〈(OrdIso(𝑟, 𝑢)‘𝑠), (OrdIso(𝑟, 𝑢)‘𝑧)〉))(𝑥‘𝑝)))), {〈∅, (OrdIso(𝑟, 𝑢)‘∅)〉})‘dom 𝑦)‘𝑦)〉) |
39 | | eqid 2622 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ω, 𝑦 ∈ 𝑢 ↦ 〈(OrdIso(𝑟, 𝑢)‘𝑥), 𝑦〉) = (𝑥 ∈ ω, 𝑦 ∈ 𝑢 ↦ 〈(OrdIso(𝑟, 𝑢)‘𝑥), 𝑦〉) |
40 | | eqid 2622 |
. . . . . . . . . . . . . . 15
⊢
((((OrdIso(𝑟, 𝑢) ∘ (𝑚‘dom OrdIso(𝑟, 𝑢))) ∘ ◡(𝑠 ∈ dom OrdIso(𝑟, 𝑢), 𝑧 ∈ dom OrdIso(𝑟, 𝑢) ↦ 〈(OrdIso(𝑟, 𝑢)‘𝑠), (OrdIso(𝑟, 𝑢)‘𝑧)〉)) ∘ (𝑥 ∈ ω, 𝑦 ∈ 𝑢 ↦ 〈(OrdIso(𝑟, 𝑢)‘𝑥), 𝑦〉)) ∘ (𝑦 ∈ ∪
𝑛 ∈ ω (𝑢 ↑𝑚
𝑛) ↦ 〈dom 𝑦,
((seq𝜔((𝑝 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝑢 ↑𝑚 suc 𝑝) ↦ ((𝑓‘(𝑥 ↾ 𝑝))((OrdIso(𝑟, 𝑢) ∘ (𝑚‘dom OrdIso(𝑟, 𝑢))) ∘ ◡(𝑠 ∈ dom OrdIso(𝑟, 𝑢), 𝑧 ∈ dom OrdIso(𝑟, 𝑢) ↦ 〈(OrdIso(𝑟, 𝑢)‘𝑠), (OrdIso(𝑟, 𝑢)‘𝑧)〉))(𝑥‘𝑝)))), {〈∅, (OrdIso(𝑟, 𝑢)‘∅)〉})‘dom 𝑦)‘𝑦)〉)) = ((((OrdIso(𝑟, 𝑢) ∘ (𝑚‘dom OrdIso(𝑟, 𝑢))) ∘ ◡(𝑠 ∈ dom OrdIso(𝑟, 𝑢), 𝑧 ∈ dom OrdIso(𝑟, 𝑢) ↦ 〈(OrdIso(𝑟, 𝑢)‘𝑠), (OrdIso(𝑟, 𝑢)‘𝑧)〉)) ∘ (𝑥 ∈ ω, 𝑦 ∈ 𝑢 ↦ 〈(OrdIso(𝑟, 𝑢)‘𝑥), 𝑦〉)) ∘ (𝑦 ∈ ∪
𝑛 ∈ ω (𝑢 ↑𝑚
𝑛) ↦ 〈dom 𝑦,
((seq𝜔((𝑝 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝑢 ↑𝑚 suc 𝑝) ↦ ((𝑓‘(𝑥 ↾ 𝑝))((OrdIso(𝑟, 𝑢) ∘ (𝑚‘dom OrdIso(𝑟, 𝑢))) ∘ ◡(𝑠 ∈ dom OrdIso(𝑟, 𝑢), 𝑧 ∈ dom OrdIso(𝑟, 𝑢) ↦ 〈(OrdIso(𝑟, 𝑢)‘𝑠), (OrdIso(𝑟, 𝑢)‘𝑧)〉))(𝑥‘𝑝)))), {〈∅, (OrdIso(𝑟, 𝑢)‘∅)〉})‘dom 𝑦)‘𝑦)〉)) |
41 | 13, 14, 15, 16, 30, 31, 32, 33, 34, 38, 39, 40 | pwfseqlem5 9485 |
. . . . . . . . . . . . . 14
⊢ ¬
(((ℎ:ω–1-1-onto→𝑡 ∧ 𝑡 ⊆ 𝐴) ∧ ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) ∧ 𝑔:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑𝑚
𝑛)) |
42 | 41 | imnani 439 |
. . . . . . . . . . . . 13
⊢ (((ℎ:ω–1-1-onto→𝑡 ∧ 𝑡 ⊆ 𝐴) ∧ ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) → ¬ 𝑔:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑𝑚
𝑛)) |
43 | 42 | nexdv 1864 |
. . . . . . . . . . . 12
⊢ (((ℎ:ω–1-1-onto→𝑡 ∧ 𝑡 ⊆ 𝐴) ∧ ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) → ¬ ∃𝑔 𝑔:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑𝑚
𝑛)) |
44 | | brdomi 7966 |
. . . . . . . . . . . 12
⊢
(𝒫 𝐴 ≼
∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛) → ∃𝑔 𝑔:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑𝑚
𝑛)) |
45 | 43, 44 | nsyl 135 |
. . . . . . . . . . 11
⊢ (((ℎ:ω–1-1-onto→𝑡 ∧ 𝑡 ⊆ 𝐴) ∧ ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) → ¬ 𝒫 𝐴 ≼ ∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛)) |
46 | 45 | ex 450 |
. . . . . . . . . 10
⊢ ((ℎ:ω–1-1-onto→𝑡 ∧ 𝑡 ⊆ 𝐴) → (∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏) → ¬ 𝒫 𝐴 ≼ ∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛))) |
47 | 46 | exlimdv 1861 |
. . . . . . . . 9
⊢ ((ℎ:ω–1-1-onto→𝑡 ∧ 𝑡 ⊆ 𝐴) → (∃𝑚∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏) → ¬ 𝒫 𝐴 ≼ ∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛))) |
48 | 7, 47 | mpi 20 |
. . . . . . . 8
⊢ ((ℎ:ω–1-1-onto→𝑡 ∧ 𝑡 ⊆ 𝐴) → ¬ 𝒫 𝐴 ≼ ∪
𝑛 ∈ ω (𝐴 ↑𝑚
𝑛)) |
49 | 48 | ex 450 |
. . . . . . 7
⊢ (ℎ:ω–1-1-onto→𝑡 → (𝑡 ⊆ 𝐴 → ¬ 𝒫 𝐴 ≼ ∪
𝑛 ∈ ω (𝐴 ↑𝑚
𝑛))) |
50 | 49 | exlimiv 1858 |
. . . . . 6
⊢
(∃ℎ ℎ:ω–1-1-onto→𝑡 → (𝑡 ⊆ 𝐴 → ¬ 𝒫 𝐴 ≼ ∪
𝑛 ∈ ω (𝐴 ↑𝑚
𝑛))) |
51 | 4, 50 | sylbi 207 |
. . . . 5
⊢ (ω
≈ 𝑡 → (𝑡 ⊆ 𝐴 → ¬ 𝒫 𝐴 ≼ ∪
𝑛 ∈ ω (𝐴 ↑𝑚
𝑛))) |
52 | 51 | imp 445 |
. . . 4
⊢ ((ω
≈ 𝑡 ∧ 𝑡 ⊆ 𝐴) → ¬ 𝒫 𝐴 ≼ ∪
𝑛 ∈ ω (𝐴 ↑𝑚
𝑛)) |
53 | 52 | exlimiv 1858 |
. . 3
⊢
(∃𝑡(ω
≈ 𝑡 ∧ 𝑡 ⊆ 𝐴) → ¬ 𝒫 𝐴 ≼ ∪
𝑛 ∈ ω (𝐴 ↑𝑚
𝑛)) |
54 | 3, 53 | syl6bi 243 |
. 2
⊢ (𝐴 ∈ V → (ω
≼ 𝐴 → ¬
𝒫 𝐴 ≼
∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛))) |
55 | 2, 54 | mpcom 38 |
1
⊢ (ω
≼ 𝐴 → ¬
𝒫 𝐴 ≼
∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛)) |