Step | Hyp | Ref
| Expression |
1 | | nfv 1505 |
. . . . . . . 8
⊢
Ⅎ𝑚 𝑟 ⊆ (𝒫
1o × ω) |
2 | | nfv 1505 |
. . . . . . . . 9
⊢
Ⅎ𝑚∀𝑝 ∈ 𝒫 1o∃𝑛 ∈ ω 𝑝𝑟𝑛 |
3 | | nfre1 2497 |
. . . . . . . . 9
⊢
Ⅎ𝑚∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫
1o𝑞𝑟𝑚 |
4 | 2, 3 | nfim 1549 |
. . . . . . . 8
⊢
Ⅎ𝑚(∀𝑝 ∈ 𝒫 1o∃𝑛 ∈ ω 𝑝𝑟𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚) |
5 | 1, 4 | nfim 1549 |
. . . . . . 7
⊢
Ⅎ𝑚(𝑟 ⊆ (𝒫
1o × ω) → (∀𝑝 ∈ 𝒫 1o∃𝑛 ∈ ω 𝑝𝑟𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚)) |
6 | 5 | nfal 1553 |
. . . . . 6
⊢
Ⅎ𝑚∀𝑟(𝑟 ⊆ (𝒫 1o ×
ω) → (∀𝑝
∈ 𝒫 1o∃𝑛 ∈ ω 𝑝𝑟𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚)) |
7 | | nfv 1505 |
. . . . . 6
⊢
Ⅎ𝑚 𝑓:ω–onto→𝒫 1o |
8 | 6, 7 | nfan 1542 |
. . . . 5
⊢
Ⅎ𝑚(∀𝑟(𝑟 ⊆ (𝒫 1o ×
ω) → (∀𝑝
∈ 𝒫 1o∃𝑛 ∈ ω 𝑝𝑟𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚)) ∧ 𝑓:ω–onto→𝒫 1o) |
9 | | breq1 3964 |
. . . . . . . . 9
⊢ (𝑞 = ∅ → (𝑞◡𝑓𝑚 ↔ ∅◡𝑓𝑚)) |
10 | | simpr 109 |
. . . . . . . . 9
⊢
((((∀𝑟(𝑟 ⊆ (𝒫
1o × ω) → (∀𝑝 ∈ 𝒫 1o∃𝑛 ∈ ω 𝑝𝑟𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚)) ∧ 𝑓:ω–onto→𝒫 1o) ∧ 𝑚 ∈ ω) ∧
∀𝑞 ∈ 𝒫
1o𝑞◡𝑓𝑚) → ∀𝑞 ∈ 𝒫 1o𝑞◡𝑓𝑚) |
11 | | 0elpw 4120 |
. . . . . . . . . 10
⊢ ∅
∈ 𝒫 1o |
12 | 11 | a1i 9 |
. . . . . . . . 9
⊢
((((∀𝑟(𝑟 ⊆ (𝒫
1o × ω) → (∀𝑝 ∈ 𝒫 1o∃𝑛 ∈ ω 𝑝𝑟𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚)) ∧ 𝑓:ω–onto→𝒫 1o) ∧ 𝑚 ∈ ω) ∧
∀𝑞 ∈ 𝒫
1o𝑞◡𝑓𝑚) → ∅ ∈ 𝒫
1o) |
13 | 9, 10, 12 | rspcdva 2818 |
. . . . . . . 8
⊢
((((∀𝑟(𝑟 ⊆ (𝒫
1o × ω) → (∀𝑝 ∈ 𝒫 1o∃𝑛 ∈ ω 𝑝𝑟𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚)) ∧ 𝑓:ω–onto→𝒫 1o) ∧ 𝑚 ∈ ω) ∧
∀𝑞 ∈ 𝒫
1o𝑞◡𝑓𝑚) → ∅◡𝑓𝑚) |
14 | | 0ex 4087 |
. . . . . . . . 9
⊢ ∅
∈ V |
15 | | vex 2712 |
. . . . . . . . 9
⊢ 𝑚 ∈ V |
16 | 14, 15 | brcnv 4762 |
. . . . . . . 8
⊢
(∅◡𝑓𝑚 ↔ 𝑚𝑓∅) |
17 | 13, 16 | sylib 121 |
. . . . . . 7
⊢
((((∀𝑟(𝑟 ⊆ (𝒫
1o × ω) → (∀𝑝 ∈ 𝒫 1o∃𝑛 ∈ ω 𝑝𝑟𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚)) ∧ 𝑓:ω–onto→𝒫 1o) ∧ 𝑚 ∈ ω) ∧
∀𝑞 ∈ 𝒫
1o𝑞◡𝑓𝑚) → 𝑚𝑓∅) |
18 | | fofn 5387 |
. . . . . . . . 9
⊢ (𝑓:ω–onto→𝒫 1o → 𝑓 Fn ω) |
19 | 18 | ad3antlr 485 |
. . . . . . . 8
⊢
((((∀𝑟(𝑟 ⊆ (𝒫
1o × ω) → (∀𝑝 ∈ 𝒫 1o∃𝑛 ∈ ω 𝑝𝑟𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚)) ∧ 𝑓:ω–onto→𝒫 1o) ∧ 𝑚 ∈ ω) ∧
∀𝑞 ∈ 𝒫
1o𝑞◡𝑓𝑚) → 𝑓 Fn ω) |
20 | | simplr 520 |
. . . . . . . 8
⊢
((((∀𝑟(𝑟 ⊆ (𝒫
1o × ω) → (∀𝑝 ∈ 𝒫 1o∃𝑛 ∈ ω 𝑝𝑟𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚)) ∧ 𝑓:ω–onto→𝒫 1o) ∧ 𝑚 ∈ ω) ∧
∀𝑞 ∈ 𝒫
1o𝑞◡𝑓𝑚) → 𝑚 ∈ ω) |
21 | | fnbrfvb 5502 |
. . . . . . . 8
⊢ ((𝑓 Fn ω ∧ 𝑚 ∈ ω) → ((𝑓‘𝑚) = ∅ ↔ 𝑚𝑓∅)) |
22 | 19, 20, 21 | syl2anc 409 |
. . . . . . 7
⊢
((((∀𝑟(𝑟 ⊆ (𝒫
1o × ω) → (∀𝑝 ∈ 𝒫 1o∃𝑛 ∈ ω 𝑝𝑟𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚)) ∧ 𝑓:ω–onto→𝒫 1o) ∧ 𝑚 ∈ ω) ∧
∀𝑞 ∈ 𝒫
1o𝑞◡𝑓𝑚) → ((𝑓‘𝑚) = ∅ ↔ 𝑚𝑓∅)) |
23 | 17, 22 | mpbird 166 |
. . . . . 6
⊢
((((∀𝑟(𝑟 ⊆ (𝒫
1o × ω) → (∀𝑝 ∈ 𝒫 1o∃𝑛 ∈ ω 𝑝𝑟𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚)) ∧ 𝑓:ω–onto→𝒫 1o) ∧ 𝑚 ∈ ω) ∧
∀𝑞 ∈ 𝒫
1o𝑞◡𝑓𝑚) → (𝑓‘𝑚) = ∅) |
24 | | breq1 3964 |
. . . . . . . . . 10
⊢ (𝑞 = 1o → (𝑞◡𝑓𝑚 ↔ 1o◡𝑓𝑚)) |
25 | | 1oex 6361 |
. . . . . . . . . . . 12
⊢
1o ∈ V |
26 | 25 | pwid 3554 |
. . . . . . . . . . 11
⊢
1o ∈ 𝒫 1o |
27 | 26 | a1i 9 |
. . . . . . . . . 10
⊢
((((∀𝑟(𝑟 ⊆ (𝒫
1o × ω) → (∀𝑝 ∈ 𝒫 1o∃𝑛 ∈ ω 𝑝𝑟𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚)) ∧ 𝑓:ω–onto→𝒫 1o) ∧ 𝑚 ∈ ω) ∧
∀𝑞 ∈ 𝒫
1o𝑞◡𝑓𝑚) → 1o ∈ 𝒫
1o) |
28 | 24, 10, 27 | rspcdva 2818 |
. . . . . . . . 9
⊢
((((∀𝑟(𝑟 ⊆ (𝒫
1o × ω) → (∀𝑝 ∈ 𝒫 1o∃𝑛 ∈ ω 𝑝𝑟𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚)) ∧ 𝑓:ω–onto→𝒫 1o) ∧ 𝑚 ∈ ω) ∧
∀𝑞 ∈ 𝒫
1o𝑞◡𝑓𝑚) → 1o◡𝑓𝑚) |
29 | 25, 15 | brcnv 4762 |
. . . . . . . . 9
⊢
(1o◡𝑓𝑚 ↔ 𝑚𝑓1o) |
30 | 28, 29 | sylib 121 |
. . . . . . . 8
⊢
((((∀𝑟(𝑟 ⊆ (𝒫
1o × ω) → (∀𝑝 ∈ 𝒫 1o∃𝑛 ∈ ω 𝑝𝑟𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚)) ∧ 𝑓:ω–onto→𝒫 1o) ∧ 𝑚 ∈ ω) ∧
∀𝑞 ∈ 𝒫
1o𝑞◡𝑓𝑚) → 𝑚𝑓1o) |
31 | | fnbrfvb 5502 |
. . . . . . . . 9
⊢ ((𝑓 Fn ω ∧ 𝑚 ∈ ω) → ((𝑓‘𝑚) = 1o ↔ 𝑚𝑓1o)) |
32 | 19, 20, 31 | syl2anc 409 |
. . . . . . . 8
⊢
((((∀𝑟(𝑟 ⊆ (𝒫
1o × ω) → (∀𝑝 ∈ 𝒫 1o∃𝑛 ∈ ω 𝑝𝑟𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚)) ∧ 𝑓:ω–onto→𝒫 1o) ∧ 𝑚 ∈ ω) ∧
∀𝑞 ∈ 𝒫
1o𝑞◡𝑓𝑚) → ((𝑓‘𝑚) = 1o ↔ 𝑚𝑓1o)) |
33 | 30, 32 | mpbird 166 |
. . . . . . 7
⊢
((((∀𝑟(𝑟 ⊆ (𝒫
1o × ω) → (∀𝑝 ∈ 𝒫 1o∃𝑛 ∈ ω 𝑝𝑟𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚)) ∧ 𝑓:ω–onto→𝒫 1o) ∧ 𝑚 ∈ ω) ∧
∀𝑞 ∈ 𝒫
1o𝑞◡𝑓𝑚) → (𝑓‘𝑚) = 1o) |
34 | | 1n0 6369 |
. . . . . . . 8
⊢
1o ≠ ∅ |
35 | 34 | neii 2326 |
. . . . . . 7
⊢ ¬
1o = ∅ |
36 | | eqeq1 2161 |
. . . . . . . . 9
⊢ ((𝑓‘𝑚) = 1o → ((𝑓‘𝑚) = ∅ ↔ 1o =
∅)) |
37 | 36 | biimpd 143 |
. . . . . . . 8
⊢ ((𝑓‘𝑚) = 1o → ((𝑓‘𝑚) = ∅ → 1o =
∅)) |
38 | 37 | con3dimp 625 |
. . . . . . 7
⊢ (((𝑓‘𝑚) = 1o ∧ ¬ 1o =
∅) → ¬ (𝑓‘𝑚) = ∅) |
39 | 33, 35, 38 | sylancl 410 |
. . . . . 6
⊢
((((∀𝑟(𝑟 ⊆ (𝒫
1o × ω) → (∀𝑝 ∈ 𝒫 1o∃𝑛 ∈ ω 𝑝𝑟𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚)) ∧ 𝑓:ω–onto→𝒫 1o) ∧ 𝑚 ∈ ω) ∧
∀𝑞 ∈ 𝒫
1o𝑞◡𝑓𝑚) → ¬ (𝑓‘𝑚) = ∅) |
40 | 23, 39 | pm2.21fal 1352 |
. . . . 5
⊢
((((∀𝑟(𝑟 ⊆ (𝒫
1o × ω) → (∀𝑝 ∈ 𝒫 1o∃𝑛 ∈ ω 𝑝𝑟𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚)) ∧ 𝑓:ω–onto→𝒫 1o) ∧ 𝑚 ∈ ω) ∧
∀𝑞 ∈ 𝒫
1o𝑞◡𝑓𝑚) → ⊥) |
41 | | fof 5385 |
. . . . . . . 8
⊢ (𝑓:ω–onto→𝒫 1o → 𝑓:ω⟶𝒫
1o) |
42 | | fssxp 5330 |
. . . . . . . . . 10
⊢ (𝑓:ω⟶𝒫
1o → 𝑓
⊆ (ω × 𝒫 1o)) |
43 | | cnvss 4752 |
. . . . . . . . . 10
⊢ (𝑓 ⊆ (ω ×
𝒫 1o) → ◡𝑓 ⊆ ◡(ω × 𝒫
1o)) |
44 | 42, 43 | syl 14 |
. . . . . . . . 9
⊢ (𝑓:ω⟶𝒫
1o → ◡𝑓 ⊆ ◡(ω × 𝒫
1o)) |
45 | | cnvxp 4997 |
. . . . . . . . 9
⊢ ◡(ω × 𝒫 1o) =
(𝒫 1o × ω) |
46 | 44, 45 | sseqtrdi 3172 |
. . . . . . . 8
⊢ (𝑓:ω⟶𝒫
1o → ◡𝑓 ⊆ (𝒫
1o × ω)) |
47 | 41, 46 | syl 14 |
. . . . . . 7
⊢ (𝑓:ω–onto→𝒫 1o → ◡𝑓 ⊆ (𝒫 1o ×
ω)) |
48 | 47 | adantl 275 |
. . . . . 6
⊢
((∀𝑟(𝑟 ⊆ (𝒫
1o × ω) → (∀𝑝 ∈ 𝒫 1o∃𝑛 ∈ ω 𝑝𝑟𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚)) ∧ 𝑓:ω–onto→𝒫 1o) → ◡𝑓 ⊆ (𝒫 1o ×
ω)) |
49 | | foelrn 5694 |
. . . . . . . . 9
⊢ ((𝑓:ω–onto→𝒫 1o ∧ 𝑝 ∈ 𝒫 1o)
→ ∃𝑛 ∈
ω 𝑝 = (𝑓‘𝑛)) |
50 | 18 | ad2antrr 480 |
. . . . . . . . . . 11
⊢ (((𝑓:ω–onto→𝒫 1o ∧ 𝑝 ∈ 𝒫 1o)
∧ 𝑛 ∈ ω)
→ 𝑓 Fn
ω) |
51 | | simpr 109 |
. . . . . . . . . . 11
⊢ (((𝑓:ω–onto→𝒫 1o ∧ 𝑝 ∈ 𝒫 1o)
∧ 𝑛 ∈ ω)
→ 𝑛 ∈
ω) |
52 | | eqcom 2156 |
. . . . . . . . . . . 12
⊢ ((𝑓‘𝑛) = 𝑝 ↔ 𝑝 = (𝑓‘𝑛)) |
53 | | fnbrfvb 5502 |
. . . . . . . . . . . . 13
⊢ ((𝑓 Fn ω ∧ 𝑛 ∈ ω) → ((𝑓‘𝑛) = 𝑝 ↔ 𝑛𝑓𝑝)) |
54 | | brcnvg 4760 |
. . . . . . . . . . . . . . 15
⊢ ((𝑝 ∈ V ∧ 𝑛 ∈ V) → (𝑝◡𝑓𝑛 ↔ 𝑛𝑓𝑝)) |
55 | 54 | elvd 2714 |
. . . . . . . . . . . . . 14
⊢ (𝑝 ∈ V → (𝑝◡𝑓𝑛 ↔ 𝑛𝑓𝑝)) |
56 | 55 | elv 2713 |
. . . . . . . . . . . . 13
⊢ (𝑝◡𝑓𝑛 ↔ 𝑛𝑓𝑝) |
57 | 53, 56 | bitr4di 197 |
. . . . . . . . . . . 12
⊢ ((𝑓 Fn ω ∧ 𝑛 ∈ ω) → ((𝑓‘𝑛) = 𝑝 ↔ 𝑝◡𝑓𝑛)) |
58 | 52, 57 | bitr3id 193 |
. . . . . . . . . . 11
⊢ ((𝑓 Fn ω ∧ 𝑛 ∈ ω) → (𝑝 = (𝑓‘𝑛) ↔ 𝑝◡𝑓𝑛)) |
59 | 50, 51, 58 | syl2anc 409 |
. . . . . . . . . 10
⊢ (((𝑓:ω–onto→𝒫 1o ∧ 𝑝 ∈ 𝒫 1o)
∧ 𝑛 ∈ ω)
→ (𝑝 = (𝑓‘𝑛) ↔ 𝑝◡𝑓𝑛)) |
60 | 59 | rexbidva 2451 |
. . . . . . . . 9
⊢ ((𝑓:ω–onto→𝒫 1o ∧ 𝑝 ∈ 𝒫 1o)
→ (∃𝑛 ∈
ω 𝑝 = (𝑓‘𝑛) ↔ ∃𝑛 ∈ ω 𝑝◡𝑓𝑛)) |
61 | 49, 60 | mpbid 146 |
. . . . . . . 8
⊢ ((𝑓:ω–onto→𝒫 1o ∧ 𝑝 ∈ 𝒫 1o)
→ ∃𝑛 ∈
ω 𝑝◡𝑓𝑛) |
62 | 61 | ralrimiva 2527 |
. . . . . . 7
⊢ (𝑓:ω–onto→𝒫 1o → ∀𝑝 ∈ 𝒫
1o∃𝑛
∈ ω 𝑝◡𝑓𝑛) |
63 | 62 | adantl 275 |
. . . . . 6
⊢
((∀𝑟(𝑟 ⊆ (𝒫
1o × ω) → (∀𝑝 ∈ 𝒫 1o∃𝑛 ∈ ω 𝑝𝑟𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚)) ∧ 𝑓:ω–onto→𝒫 1o) → ∀𝑝 ∈ 𝒫
1o∃𝑛
∈ ω 𝑝◡𝑓𝑛) |
64 | | cnvexg 5116 |
. . . . . . . 8
⊢ (𝑓 ∈ V → ◡𝑓 ∈ V) |
65 | 64 | elv 2713 |
. . . . . . 7
⊢ ◡𝑓 ∈ V |
66 | | simpl 108 |
. . . . . . 7
⊢
((∀𝑟(𝑟 ⊆ (𝒫
1o × ω) → (∀𝑝 ∈ 𝒫 1o∃𝑛 ∈ ω 𝑝𝑟𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚)) ∧ 𝑓:ω–onto→𝒫 1o) → ∀𝑟(𝑟 ⊆ (𝒫 1o ×
ω) → (∀𝑝
∈ 𝒫 1o∃𝑛 ∈ ω 𝑝𝑟𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚))) |
67 | | sseq1 3147 |
. . . . . . . . 9
⊢ (𝑟 = ◡𝑓 → (𝑟 ⊆ (𝒫 1o ×
ω) ↔ ◡𝑓 ⊆ (𝒫 1o ×
ω))) |
68 | | breq 3963 |
. . . . . . . . . . . 12
⊢ (𝑟 = ◡𝑓 → (𝑝𝑟𝑛 ↔ 𝑝◡𝑓𝑛)) |
69 | 68 | rexbidv 2455 |
. . . . . . . . . . 11
⊢ (𝑟 = ◡𝑓 → (∃𝑛 ∈ ω 𝑝𝑟𝑛 ↔ ∃𝑛 ∈ ω 𝑝◡𝑓𝑛)) |
70 | 69 | ralbidv 2454 |
. . . . . . . . . 10
⊢ (𝑟 = ◡𝑓 → (∀𝑝 ∈ 𝒫 1o∃𝑛 ∈ ω 𝑝𝑟𝑛 ↔ ∀𝑝 ∈ 𝒫 1o∃𝑛 ∈ ω 𝑝◡𝑓𝑛)) |
71 | | breq 3963 |
. . . . . . . . . . . 12
⊢ (𝑟 = ◡𝑓 → (𝑞𝑟𝑚 ↔ 𝑞◡𝑓𝑚)) |
72 | 71 | ralbidv 2454 |
. . . . . . . . . . 11
⊢ (𝑟 = ◡𝑓 → (∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚 ↔ ∀𝑞 ∈ 𝒫 1o𝑞◡𝑓𝑚)) |
73 | 72 | rexbidv 2455 |
. . . . . . . . . 10
⊢ (𝑟 = ◡𝑓 → (∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚 ↔ ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞◡𝑓𝑚)) |
74 | 70, 73 | imbi12d 233 |
. . . . . . . . 9
⊢ (𝑟 = ◡𝑓 → ((∀𝑝 ∈ 𝒫 1o∃𝑛 ∈ ω 𝑝𝑟𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚) ↔ (∀𝑝 ∈ 𝒫 1o∃𝑛 ∈ ω 𝑝◡𝑓𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞◡𝑓𝑚))) |
75 | 67, 74 | imbi12d 233 |
. . . . . . . 8
⊢ (𝑟 = ◡𝑓 → ((𝑟 ⊆ (𝒫 1o ×
ω) → (∀𝑝
∈ 𝒫 1o∃𝑛 ∈ ω 𝑝𝑟𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚)) ↔ (◡𝑓 ⊆ (𝒫 1o ×
ω) → (∀𝑝
∈ 𝒫 1o∃𝑛 ∈ ω 𝑝◡𝑓𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞◡𝑓𝑚)))) |
76 | 75 | spcgv 2796 |
. . . . . . 7
⊢ (◡𝑓 ∈ V → (∀𝑟(𝑟 ⊆ (𝒫 1o ×
ω) → (∀𝑝
∈ 𝒫 1o∃𝑛 ∈ ω 𝑝𝑟𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚)) → (◡𝑓 ⊆ (𝒫 1o ×
ω) → (∀𝑝
∈ 𝒫 1o∃𝑛 ∈ ω 𝑝◡𝑓𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞◡𝑓𝑚)))) |
77 | 65, 66, 76 | mpsyl 65 |
. . . . . 6
⊢
((∀𝑟(𝑟 ⊆ (𝒫
1o × ω) → (∀𝑝 ∈ 𝒫 1o∃𝑛 ∈ ω 𝑝𝑟𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚)) ∧ 𝑓:ω–onto→𝒫 1o) → (◡𝑓 ⊆ (𝒫 1o ×
ω) → (∀𝑝
∈ 𝒫 1o∃𝑛 ∈ ω 𝑝◡𝑓𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞◡𝑓𝑚))) |
78 | 48, 63, 77 | mp2d 47 |
. . . . 5
⊢
((∀𝑟(𝑟 ⊆ (𝒫
1o × ω) → (∀𝑝 ∈ 𝒫 1o∃𝑛 ∈ ω 𝑝𝑟𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚)) ∧ 𝑓:ω–onto→𝒫 1o) → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫
1o𝑞◡𝑓𝑚) |
79 | 8, 40, 78 | r19.29af 2595 |
. . . 4
⊢
((∀𝑟(𝑟 ⊆ (𝒫
1o × ω) → (∀𝑝 ∈ 𝒫 1o∃𝑛 ∈ ω 𝑝𝑟𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚)) ∧ 𝑓:ω–onto→𝒫 1o) →
⊥) |
80 | 79 | inegd 1351 |
. . 3
⊢
(∀𝑟(𝑟 ⊆ (𝒫
1o × ω) → (∀𝑝 ∈ 𝒫 1o∃𝑛 ∈ ω 𝑝𝑟𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚)) → ¬ 𝑓:ω–onto→𝒫 1o) |
81 | 80 | nexdv 1913 |
. 2
⊢
(∀𝑟(𝑟 ⊆ (𝒫
1o × ω) → (∀𝑝 ∈ 𝒫 1o∃𝑛 ∈ ω 𝑝𝑟𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚)) → ¬ ∃𝑓 𝑓:ω–onto→𝒫 1o) |
82 | | elex2 2725 |
. . 3
⊢ (∅
∈ 𝒫 1o → ∃𝑤 𝑤 ∈ 𝒫
1o) |
83 | | ctm 7039 |
. . 3
⊢
(∃𝑤 𝑤 ∈ 𝒫 1o
→ (∃𝑓 𝑓:ω–onto→(𝒫 1o ⊔
1o) ↔ ∃𝑓 𝑓:ω–onto→𝒫 1o)) |
84 | 11, 82, 83 | mp2b 8 |
. 2
⊢
(∃𝑓 𝑓:ω–onto→(𝒫 1o ⊔
1o) ↔ ∃𝑓 𝑓:ω–onto→𝒫 1o) |
85 | 81, 84 | sylnibr 667 |
1
⊢
(∀𝑟(𝑟 ⊆ (𝒫
1o × ω) → (∀𝑝 ∈ 𝒫 1o∃𝑛 ∈ ω 𝑝𝑟𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚)) → ¬ ∃𝑓 𝑓:ω–onto→(𝒫 1o ⊔
1o)) |