Step | Hyp | Ref
| Expression |
1 | | reldom 8353 |
. . 3
⊢ Rel
≼ |
2 | 1 | brrelex2i 5487 |
. 2
⊢ (ω
≼ 𝐴 → 𝐴 ∈ V) |
3 | | domeng 8361 |
. . 3
⊢ (𝐴 ∈ V → (ω
≼ 𝐴 ↔
∃𝑡(ω ≈
𝑡 ∧ 𝑡 ⊆ 𝐴))) |
4 | | bren 8356 |
. . . . . 6
⊢ (ω
≈ 𝑡 ↔
∃ℎ ℎ:ω–1-1-onto→𝑡) |
5 | | harcl 8861 |
. . . . . . . . . 10
⊢
(har‘𝒫 𝐴) ∈ On |
6 | | infxpenc2 9283 |
. . . . . . . . . 10
⊢
((har‘𝒫 𝐴) ∈ On → ∃𝑚∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) |
7 | 5, 6 | ax-mp 5 |
. . . . . . . . 9
⊢
∃𝑚∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏) |
8 | | simpr 485 |
. . . . . . . . . . . . . . . 16
⊢ ((((ℎ:ω–1-1-onto→𝑡 ∧ 𝑡 ⊆ 𝐴) ∧ ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) ∧ 𝑔:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑𝑚
𝑛)) → 𝑔:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑𝑚
𝑛)) |
9 | | oveq2 7015 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑘 → (𝐴 ↑𝑚 𝑛) = (𝐴 ↑𝑚 𝑘)) |
10 | 9 | cbviunv 4860 |
. . . . . . . . . . . . . . . . 17
⊢ ∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛) = ∪ 𝑘 ∈ ω (𝐴 ↑𝑚 𝑘) |
11 | | f1eq3 6432 |
. . . . . . . . . . . . . . . . 17
⊢ (∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛) = ∪ 𝑘 ∈ ω (𝐴 ↑𝑚 𝑘) → (𝑔:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑𝑚
𝑛) ↔ 𝑔:𝒫 𝐴–1-1→∪ 𝑘 ∈ ω (𝐴 ↑𝑚
𝑘))) |
12 | 10, 11 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑𝑚
𝑛) ↔ 𝑔:𝒫 𝐴–1-1→∪ 𝑘 ∈ ω (𝐴 ↑𝑚
𝑘)) |
13 | 8, 12 | sylib 219 |
. . . . . . . . . . . . . . 15
⊢ ((((ℎ:ω–1-1-onto→𝑡 ∧ 𝑡 ⊆ 𝐴) ∧ ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) ∧ 𝑔:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑𝑚
𝑛)) → 𝑔:𝒫 𝐴–1-1→∪ 𝑘 ∈ ω (𝐴 ↑𝑚
𝑘)) |
14 | | simpllr 772 |
. . . . . . . . . . . . . . 15
⊢ ((((ℎ:ω–1-1-onto→𝑡 ∧ 𝑡 ⊆ 𝐴) ∧ ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) ∧ 𝑔:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑𝑚
𝑛)) → 𝑡 ⊆ 𝐴) |
15 | | simplll 771 |
. . . . . . . . . . . . . . 15
⊢ ((((ℎ:ω–1-1-onto→𝑡 ∧ 𝑡 ⊆ 𝐴) ∧ ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) ∧ 𝑔:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑𝑚
𝑛)) → ℎ:ω–1-1-onto→𝑡) |
16 | | biid 262 |
. . . . . . . . . . . . . . 15
⊢ (((𝑢 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑢 × 𝑢) ∧ 𝑟 We 𝑢) ∧ ω ≼ 𝑢) ↔ ((𝑢 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑢 × 𝑢) ∧ 𝑟 We 𝑢) ∧ ω ≼ 𝑢)) |
17 | | simplr 765 |
. . . . . . . . . . . . . . . 16
⊢ ((((ℎ:ω–1-1-onto→𝑡 ∧ 𝑡 ⊆ 𝐴) ∧ ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) ∧ 𝑔:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑𝑚
𝑛)) → ∀𝑏 ∈ (har‘𝒫
𝐴)(ω ⊆ 𝑏 → (𝑚‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) |
18 | | sseq2 3909 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 = 𝑤 → (ω ⊆ 𝑏 ↔ ω ⊆ 𝑤)) |
19 | | fveq2 6530 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑏 = 𝑤 → (𝑚‘𝑏) = (𝑚‘𝑤)) |
20 | | f1oeq1 6464 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑚‘𝑏) = (𝑚‘𝑤) → ((𝑚‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏 ↔ (𝑚‘𝑤):(𝑏 × 𝑏)–1-1-onto→𝑏)) |
21 | 19, 20 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑏 = 𝑤 → ((𝑚‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏 ↔ (𝑚‘𝑤):(𝑏 × 𝑏)–1-1-onto→𝑏)) |
22 | | xpeq12 5460 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑏 = 𝑤 ∧ 𝑏 = 𝑤) → (𝑏 × 𝑏) = (𝑤 × 𝑤)) |
23 | 22 | anidms 567 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑏 = 𝑤 → (𝑏 × 𝑏) = (𝑤 × 𝑤)) |
24 | 23 | f1oeq2d 6471 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑏 = 𝑤 → ((𝑚‘𝑤):(𝑏 × 𝑏)–1-1-onto→𝑏 ↔ (𝑚‘𝑤):(𝑤 × 𝑤)–1-1-onto→𝑏)) |
25 | | f1oeq3 6466 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑏 = 𝑤 → ((𝑚‘𝑤):(𝑤 × 𝑤)–1-1-onto→𝑏 ↔ (𝑚‘𝑤):(𝑤 × 𝑤)–1-1-onto→𝑤)) |
26 | 21, 24, 25 | 3bitrd 306 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 = 𝑤 → ((𝑚‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏 ↔ (𝑚‘𝑤):(𝑤 × 𝑤)–1-1-onto→𝑤)) |
27 | 18, 26 | imbi12d 346 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = 𝑤 → ((ω ⊆ 𝑏 → (𝑚‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏) ↔ (ω ⊆ 𝑤 → (𝑚‘𝑤):(𝑤 × 𝑤)–1-1-onto→𝑤))) |
28 | 27 | cbvralv 3400 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑏 ∈
(har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏) ↔ ∀𝑤 ∈ (har‘𝒫
𝐴)(ω ⊆ 𝑤 → (𝑚‘𝑤):(𝑤 × 𝑤)–1-1-onto→𝑤)) |
29 | 17, 28 | sylib 219 |
. . . . . . . . . . . . . . 15
⊢ ((((ℎ:ω–1-1-onto→𝑡 ∧ 𝑡 ⊆ 𝐴) ∧ ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) ∧ 𝑔:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑𝑚
𝑛)) → ∀𝑤 ∈ (har‘𝒫
𝐴)(ω ⊆ 𝑤 → (𝑚‘𝑤):(𝑤 × 𝑤)–1-1-onto→𝑤)) |
30 | | eqid 2793 |
. . . . . . . . . . . . . . 15
⊢
OrdIso(𝑟, 𝑢) = OrdIso(𝑟, 𝑢) |
31 | | eqid 2793 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 ∈ dom OrdIso(𝑟, 𝑢), 𝑧 ∈ dom OrdIso(𝑟, 𝑢) ↦ 〈(OrdIso(𝑟, 𝑢)‘𝑠), (OrdIso(𝑟, 𝑢)‘𝑧)〉) = (𝑠 ∈ dom OrdIso(𝑟, 𝑢), 𝑧 ∈ dom OrdIso(𝑟, 𝑢) ↦ 〈(OrdIso(𝑟, 𝑢)‘𝑠), (OrdIso(𝑟, 𝑢)‘𝑧)〉) |
32 | | eqid 2793 |
. . . . . . . . . . . . . . 15
⊢
((OrdIso(𝑟, 𝑢) ∘ (𝑚‘dom OrdIso(𝑟, 𝑢))) ∘ ◡(𝑠 ∈ dom OrdIso(𝑟, 𝑢), 𝑧 ∈ dom OrdIso(𝑟, 𝑢) ↦ 〈(OrdIso(𝑟, 𝑢)‘𝑠), (OrdIso(𝑟, 𝑢)‘𝑧)〉)) = ((OrdIso(𝑟, 𝑢) ∘ (𝑚‘dom OrdIso(𝑟, 𝑢))) ∘ ◡(𝑠 ∈ dom OrdIso(𝑟, 𝑢), 𝑧 ∈ dom OrdIso(𝑟, 𝑢) ↦ 〈(OrdIso(𝑟, 𝑢)‘𝑠), (OrdIso(𝑟, 𝑢)‘𝑧)〉)) |
33 | | eqid 2793 |
. . . . . . . . . . . . . . 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(𝑟, 𝑢)‘∅)〉}) |
34 | | oveq2 7015 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑘 → (𝑢 ↑𝑚 𝑛) = (𝑢 ↑𝑚 𝑘)) |
35 | 34 | cbviunv 4860 |
. . . . . . . . . . . . . . . 16
⊢ ∪ 𝑛 ∈ ω (𝑢 ↑𝑚 𝑛) = ∪ 𝑘 ∈ ω (𝑢 ↑𝑚 𝑘) |
36 | 35 | mpteq1i 5044 |
. . . . . . . . . . . . . . 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 𝑦)‘𝑦)〉) |
37 | | eqid 2793 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ω, 𝑦 ∈ 𝑢 ↦ 〈(OrdIso(𝑟, 𝑢)‘𝑥), 𝑦〉) = (𝑥 ∈ ω, 𝑦 ∈ 𝑢 ↦ 〈(OrdIso(𝑟, 𝑢)‘𝑥), 𝑦〉) |
38 | | eqid 2793 |
. . . . . . . . . . . . . . 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 𝑦)‘𝑦)〉)) |
39 | 13, 14, 15, 16, 29, 30, 31, 32, 33, 36, 37, 38 | pwfseqlem5 9920 |
. . . . . . . . . . . . . 14
⊢ ¬
(((ℎ:ω–1-1-onto→𝑡 ∧ 𝑡 ⊆ 𝐴) ∧ ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) ∧ 𝑔:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑𝑚
𝑛)) |
40 | 39 | imnani 401 |
. . . . . . . . . . . . 13
⊢ (((ℎ:ω–1-1-onto→𝑡 ∧ 𝑡 ⊆ 𝐴) ∧ ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) → ¬ 𝑔:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑𝑚
𝑛)) |
41 | 40 | nexdv 1912 |
. . . . . . . . . . . 12
⊢ (((ℎ:ω–1-1-onto→𝑡 ∧ 𝑡 ⊆ 𝐴) ∧ ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) → ¬ ∃𝑔 𝑔:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑𝑚
𝑛)) |
42 | | brdomi 8358 |
. . . . . . . . . . . 12
⊢
(𝒫 𝐴 ≼
∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛) → ∃𝑔 𝑔:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑𝑚
𝑛)) |
43 | 41, 42 | nsyl 142 |
. . . . . . . . . . 11
⊢ (((ℎ:ω–1-1-onto→𝑡 ∧ 𝑡 ⊆ 𝐴) ∧ ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) → ¬ 𝒫 𝐴 ≼ ∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛)) |
44 | 43 | ex 413 |
. . . . . . . . . 10
⊢ ((ℎ:ω–1-1-onto→𝑡 ∧ 𝑡 ⊆ 𝐴) → (∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏) → ¬ 𝒫 𝐴 ≼ ∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛))) |
45 | 44 | exlimdv 1909 |
. . . . . . . . 9
⊢ ((ℎ:ω–1-1-onto→𝑡 ∧ 𝑡 ⊆ 𝐴) → (∃𝑚∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑚‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏) → ¬ 𝒫 𝐴 ≼ ∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛))) |
46 | 7, 45 | mpi 20 |
. . . . . . . 8
⊢ ((ℎ:ω–1-1-onto→𝑡 ∧ 𝑡 ⊆ 𝐴) → ¬ 𝒫 𝐴 ≼ ∪
𝑛 ∈ ω (𝐴 ↑𝑚
𝑛)) |
47 | 46 | ex 413 |
. . . . . . 7
⊢ (ℎ:ω–1-1-onto→𝑡 → (𝑡 ⊆ 𝐴 → ¬ 𝒫 𝐴 ≼ ∪
𝑛 ∈ ω (𝐴 ↑𝑚
𝑛))) |
48 | 47 | exlimiv 1906 |
. . . . . 6
⊢
(∃ℎ ℎ:ω–1-1-onto→𝑡 → (𝑡 ⊆ 𝐴 → ¬ 𝒫 𝐴 ≼ ∪
𝑛 ∈ ω (𝐴 ↑𝑚
𝑛))) |
49 | 4, 48 | sylbi 218 |
. . . . 5
⊢ (ω
≈ 𝑡 → (𝑡 ⊆ 𝐴 → ¬ 𝒫 𝐴 ≼ ∪
𝑛 ∈ ω (𝐴 ↑𝑚
𝑛))) |
50 | 49 | imp 407 |
. . . 4
⊢ ((ω
≈ 𝑡 ∧ 𝑡 ⊆ 𝐴) → ¬ 𝒫 𝐴 ≼ ∪
𝑛 ∈ ω (𝐴 ↑𝑚
𝑛)) |
51 | 50 | exlimiv 1906 |
. . 3
⊢
(∃𝑡(ω
≈ 𝑡 ∧ 𝑡 ⊆ 𝐴) → ¬ 𝒫 𝐴 ≼ ∪
𝑛 ∈ ω (𝐴 ↑𝑚
𝑛)) |
52 | 3, 51 | syl6bi 254 |
. 2
⊢ (𝐴 ∈ V → (ω
≼ 𝐴 → ¬
𝒫 𝐴 ≼
∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛))) |
53 | 2, 52 | mpcom 38 |
1
⊢ (ω
≼ 𝐴 → ¬
𝒫 𝐴 ≼
∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛)) |