Mathbox for Jim Kingdon < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >   Mathboxes  >  pw1nct GIF version

Theorem pw1nct 13369
 Description: A condition which ensures that the powerset of a singleton is not countable. The antecedent here can be referred to as the uniformity principle. Based on Mastodon posts by Andrej Bauer and Rahul Chhabra. (Contributed by Jim Kingdon, 29-May-2024.)
Assertion
Ref Expression
pw1nct (∀𝑟(𝑟 ⊆ (𝒫 1o × ω) → (∀𝑝 ∈ 𝒫 1o𝑛 ∈ ω 𝑝𝑟𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚)) → ¬ ∃𝑓 𝑓:ω–onto→(𝒫 1o ⊔ 1o))
Distinct variable groups:   𝑓,𝑚,𝑛,𝑝,𝑟   𝑓,𝑞,𝑚,𝑟

Proof of Theorem pw1nct
Dummy variable 𝑤 is distinct from all other variables.
StepHypRef Expression
1 nfv 1509 . . . . . . . 8 𝑚 𝑟 ⊆ (𝒫 1o × ω)
2 nfv 1509 . . . . . . . . 9 𝑚𝑝 ∈ 𝒫 1o𝑛 ∈ ω 𝑝𝑟𝑛
3 nfre1 2479 . . . . . . . . 9 𝑚𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚
42, 3nfim 1552 . . . . . . . 8 𝑚(∀𝑝 ∈ 𝒫 1o𝑛 ∈ ω 𝑝𝑟𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚)
51, 4nfim 1552 . . . . . . 7 𝑚(𝑟 ⊆ (𝒫 1o × ω) → (∀𝑝 ∈ 𝒫 1o𝑛 ∈ ω 𝑝𝑟𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚))
65nfal 1556 . . . . . 6 𝑚𝑟(𝑟 ⊆ (𝒫 1o × ω) → (∀𝑝 ∈ 𝒫 1o𝑛 ∈ ω 𝑝𝑟𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚))
7 nfv 1509 . . . . . 6 𝑚 𝑓:ω–onto→𝒫 1o
86, 7nfan 1545 . . . . 5 𝑚(∀𝑟(𝑟 ⊆ (𝒫 1o × ω) → (∀𝑝 ∈ 𝒫 1o𝑛 ∈ ω 𝑝𝑟𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚)) ∧ 𝑓:ω–onto→𝒫 1o)
9 breq1 3939 . . . . . . . . 9 (𝑞 = ∅ → (𝑞𝑓𝑚 ↔ ∅𝑓𝑚))
10 simpr 109 . . . . . . . . 9 ((((∀𝑟(𝑟 ⊆ (𝒫 1o × ω) → (∀𝑝 ∈ 𝒫 1o𝑛 ∈ ω 𝑝𝑟𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚)) ∧ 𝑓:ω–onto→𝒫 1o) ∧ 𝑚 ∈ ω) ∧ ∀𝑞 ∈ 𝒫 1o𝑞𝑓𝑚) → ∀𝑞 ∈ 𝒫 1o𝑞𝑓𝑚)
11 0elpw 4095 . . . . . . . . . 10 ∅ ∈ 𝒫 1o
1211a1i 9 . . . . . . . . 9 ((((∀𝑟(𝑟 ⊆ (𝒫 1o × ω) → (∀𝑝 ∈ 𝒫 1o𝑛 ∈ ω 𝑝𝑟𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚)) ∧ 𝑓:ω–onto→𝒫 1o) ∧ 𝑚 ∈ ω) ∧ ∀𝑞 ∈ 𝒫 1o𝑞𝑓𝑚) → ∅ ∈ 𝒫 1o)
139, 10, 12rspcdva 2797 . . . . . . . 8 ((((∀𝑟(𝑟 ⊆ (𝒫 1o × ω) → (∀𝑝 ∈ 𝒫 1o𝑛 ∈ ω 𝑝𝑟𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚)) ∧ 𝑓:ω–onto→𝒫 1o) ∧ 𝑚 ∈ ω) ∧ ∀𝑞 ∈ 𝒫 1o𝑞𝑓𝑚) → ∅𝑓𝑚)
14 0ex 4062 . . . . . . . . 9 ∅ ∈ V
15 vex 2692 . . . . . . . . 9 𝑚 ∈ V
1614, 15brcnv 4729 . . . . . . . 8 (∅𝑓𝑚𝑚𝑓∅)
1713, 16sylib 121 . . . . . . 7 ((((∀𝑟(𝑟 ⊆ (𝒫 1o × ω) → (∀𝑝 ∈ 𝒫 1o𝑛 ∈ ω 𝑝𝑟𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚)) ∧ 𝑓:ω–onto→𝒫 1o) ∧ 𝑚 ∈ ω) ∧ ∀𝑞 ∈ 𝒫 1o𝑞𝑓𝑚) → 𝑚𝑓∅)
18 fofn 5354 . . . . . . . . 9 (𝑓:ω–onto→𝒫 1o𝑓 Fn ω)
1918ad3antlr 485 . . . . . . . 8 ((((∀𝑟(𝑟 ⊆ (𝒫 1o × ω) → (∀𝑝 ∈ 𝒫 1o𝑛 ∈ ω 𝑝𝑟𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚)) ∧ 𝑓:ω–onto→𝒫 1o) ∧ 𝑚 ∈ ω) ∧ ∀𝑞 ∈ 𝒫 1o𝑞𝑓𝑚) → 𝑓 Fn ω)
20 simplr 520 . . . . . . . 8 ((((∀𝑟(𝑟 ⊆ (𝒫 1o × ω) → (∀𝑝 ∈ 𝒫 1o𝑛 ∈ ω 𝑝𝑟𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚)) ∧ 𝑓:ω–onto→𝒫 1o) ∧ 𝑚 ∈ ω) ∧ ∀𝑞 ∈ 𝒫 1o𝑞𝑓𝑚) → 𝑚 ∈ ω)
21 fnbrfvb 5469 . . . . . . . 8 ((𝑓 Fn ω ∧ 𝑚 ∈ ω) → ((𝑓𝑚) = ∅ ↔ 𝑚𝑓∅))
2219, 20, 21syl2anc 409 . . . . . . 7 ((((∀𝑟(𝑟 ⊆ (𝒫 1o × ω) → (∀𝑝 ∈ 𝒫 1o𝑛 ∈ ω 𝑝𝑟𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚)) ∧ 𝑓:ω–onto→𝒫 1o) ∧ 𝑚 ∈ ω) ∧ ∀𝑞 ∈ 𝒫 1o𝑞𝑓𝑚) → ((𝑓𝑚) = ∅ ↔ 𝑚𝑓∅))
2317, 22mpbird 166 . . . . . 6 ((((∀𝑟(𝑟 ⊆ (𝒫 1o × ω) → (∀𝑝 ∈ 𝒫 1o𝑛 ∈ ω 𝑝𝑟𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚)) ∧ 𝑓:ω–onto→𝒫 1o) ∧ 𝑚 ∈ ω) ∧ ∀𝑞 ∈ 𝒫 1o𝑞𝑓𝑚) → (𝑓𝑚) = ∅)
24 breq1 3939 . . . . . . . . . 10 (𝑞 = 1o → (𝑞𝑓𝑚 ↔ 1o𝑓𝑚))
25 1oex 6328 . . . . . . . . . . . 12 1o ∈ V
2625pwid 3529 . . . . . . . . . . 11 1o ∈ 𝒫 1o
2726a1i 9 . . . . . . . . . 10 ((((∀𝑟(𝑟 ⊆ (𝒫 1o × ω) → (∀𝑝 ∈ 𝒫 1o𝑛 ∈ ω 𝑝𝑟𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚)) ∧ 𝑓:ω–onto→𝒫 1o) ∧ 𝑚 ∈ ω) ∧ ∀𝑞 ∈ 𝒫 1o𝑞𝑓𝑚) → 1o ∈ 𝒫 1o)
2824, 10, 27rspcdva 2797 . . . . . . . . 9 ((((∀𝑟(𝑟 ⊆ (𝒫 1o × ω) → (∀𝑝 ∈ 𝒫 1o𝑛 ∈ ω 𝑝𝑟𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚)) ∧ 𝑓:ω–onto→𝒫 1o) ∧ 𝑚 ∈ ω) ∧ ∀𝑞 ∈ 𝒫 1o𝑞𝑓𝑚) → 1o𝑓𝑚)
2925, 15brcnv 4729 . . . . . . . . 9 (1o𝑓𝑚𝑚𝑓1o)
3028, 29sylib 121 . . . . . . . 8 ((((∀𝑟(𝑟 ⊆ (𝒫 1o × ω) → (∀𝑝 ∈ 𝒫 1o𝑛 ∈ ω 𝑝𝑟𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚)) ∧ 𝑓:ω–onto→𝒫 1o) ∧ 𝑚 ∈ ω) ∧ ∀𝑞 ∈ 𝒫 1o𝑞𝑓𝑚) → 𝑚𝑓1o)
31 fnbrfvb 5469 . . . . . . . . 9 ((𝑓 Fn ω ∧ 𝑚 ∈ ω) → ((𝑓𝑚) = 1o𝑚𝑓1o))
3219, 20, 31syl2anc 409 . . . . . . . 8 ((((∀𝑟(𝑟 ⊆ (𝒫 1o × ω) → (∀𝑝 ∈ 𝒫 1o𝑛 ∈ ω 𝑝𝑟𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚)) ∧ 𝑓:ω–onto→𝒫 1o) ∧ 𝑚 ∈ ω) ∧ ∀𝑞 ∈ 𝒫 1o𝑞𝑓𝑚) → ((𝑓𝑚) = 1o𝑚𝑓1o))
3330, 32mpbird 166 . . . . . . 7 ((((∀𝑟(𝑟 ⊆ (𝒫 1o × ω) → (∀𝑝 ∈ 𝒫 1o𝑛 ∈ ω 𝑝𝑟𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚)) ∧ 𝑓:ω–onto→𝒫 1o) ∧ 𝑚 ∈ ω) ∧ ∀𝑞 ∈ 𝒫 1o𝑞𝑓𝑚) → (𝑓𝑚) = 1o)
34 1n0 6336 . . . . . . . 8 1o ≠ ∅
3534neii 2311 . . . . . . 7 ¬ 1o = ∅
36 eqeq1 2147 . . . . . . . . 9 ((𝑓𝑚) = 1o → ((𝑓𝑚) = ∅ ↔ 1o = ∅))
3736biimpd 143 . . . . . . . 8 ((𝑓𝑚) = 1o → ((𝑓𝑚) = ∅ → 1o = ∅))
3837con3dimp 625 . . . . . . 7 (((𝑓𝑚) = 1o ∧ ¬ 1o = ∅) → ¬ (𝑓𝑚) = ∅)
3933, 35, 38sylancl 410 . . . . . 6 ((((∀𝑟(𝑟 ⊆ (𝒫 1o × ω) → (∀𝑝 ∈ 𝒫 1o𝑛 ∈ ω 𝑝𝑟𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚)) ∧ 𝑓:ω–onto→𝒫 1o) ∧ 𝑚 ∈ ω) ∧ ∀𝑞 ∈ 𝒫 1o𝑞𝑓𝑚) → ¬ (𝑓𝑚) = ∅)
4023, 39pm2.21fal 1352 . . . . 5 ((((∀𝑟(𝑟 ⊆ (𝒫 1o × ω) → (∀𝑝 ∈ 𝒫 1o𝑛 ∈ ω 𝑝𝑟𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚)) ∧ 𝑓:ω–onto→𝒫 1o) ∧ 𝑚 ∈ ω) ∧ ∀𝑞 ∈ 𝒫 1o𝑞𝑓𝑚) → ⊥)
41 fof 5352 . . . . . . . 8 (𝑓:ω–onto→𝒫 1o𝑓:ω⟶𝒫 1o)
42 fssxp 5297 . . . . . . . . . 10 (𝑓:ω⟶𝒫 1o𝑓 ⊆ (ω × 𝒫 1o))
43 cnvss 4719 . . . . . . . . . 10 (𝑓 ⊆ (ω × 𝒫 1o) → 𝑓(ω × 𝒫 1o))
4442, 43syl 14 . . . . . . . . 9 (𝑓:ω⟶𝒫 1o𝑓(ω × 𝒫 1o))
45 cnvxp 4964 . . . . . . . . 9 (ω × 𝒫 1o) = (𝒫 1o × ω)
4644, 45sseqtrdi 3149 . . . . . . . 8 (𝑓:ω⟶𝒫 1o𝑓 ⊆ (𝒫 1o × ω))
4741, 46syl 14 . . . . . . 7 (𝑓:ω–onto→𝒫 1o𝑓 ⊆ (𝒫 1o × ω))
4847adantl 275 . . . . . 6 ((∀𝑟(𝑟 ⊆ (𝒫 1o × ω) → (∀𝑝 ∈ 𝒫 1o𝑛 ∈ ω 𝑝𝑟𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚)) ∧ 𝑓:ω–onto→𝒫 1o) → 𝑓 ⊆ (𝒫 1o × ω))
49 foelrn 5661 . . . . . . . . 9 ((𝑓:ω–onto→𝒫 1o𝑝 ∈ 𝒫 1o) → ∃𝑛 ∈ ω 𝑝 = (𝑓𝑛))
5018ad2antrr 480 . . . . . . . . . . 11 (((𝑓:ω–onto→𝒫 1o𝑝 ∈ 𝒫 1o) ∧ 𝑛 ∈ ω) → 𝑓 Fn ω)
51 simpr 109 . . . . . . . . . . 11 (((𝑓:ω–onto→𝒫 1o𝑝 ∈ 𝒫 1o) ∧ 𝑛 ∈ ω) → 𝑛 ∈ ω)
52 eqcom 2142 . . . . . . . . . . . 12 ((𝑓𝑛) = 𝑝𝑝 = (𝑓𝑛))
53 fnbrfvb 5469 . . . . . . . . . . . . 13 ((𝑓 Fn ω ∧ 𝑛 ∈ ω) → ((𝑓𝑛) = 𝑝𝑛𝑓𝑝))
54 brcnvg 4727 . . . . . . . . . . . . . . 15 ((𝑝 ∈ V ∧ 𝑛 ∈ V) → (𝑝𝑓𝑛𝑛𝑓𝑝))
5554elvd 2694 . . . . . . . . . . . . . 14 (𝑝 ∈ V → (𝑝𝑓𝑛𝑛𝑓𝑝))
5655elv 2693 . . . . . . . . . . . . 13 (𝑝𝑓𝑛𝑛𝑓𝑝)
5753, 56syl6bbr 197 . . . . . . . . . . . 12 ((𝑓 Fn ω ∧ 𝑛 ∈ ω) → ((𝑓𝑛) = 𝑝𝑝𝑓𝑛))
5852, 57bitr3id 193 . . . . . . . . . . 11 ((𝑓 Fn ω ∧ 𝑛 ∈ ω) → (𝑝 = (𝑓𝑛) ↔ 𝑝𝑓𝑛))
5950, 51, 58syl2anc 409 . . . . . . . . . 10 (((𝑓:ω–onto→𝒫 1o𝑝 ∈ 𝒫 1o) ∧ 𝑛 ∈ ω) → (𝑝 = (𝑓𝑛) ↔ 𝑝𝑓𝑛))
6059rexbidva 2435 . . . . . . . . 9 ((𝑓:ω–onto→𝒫 1o𝑝 ∈ 𝒫 1o) → (∃𝑛 ∈ ω 𝑝 = (𝑓𝑛) ↔ ∃𝑛 ∈ ω 𝑝𝑓𝑛))
6149, 60mpbid 146 . . . . . . . 8 ((𝑓:ω–onto→𝒫 1o𝑝 ∈ 𝒫 1o) → ∃𝑛 ∈ ω 𝑝𝑓𝑛)
6261ralrimiva 2508 . . . . . . 7 (𝑓:ω–onto→𝒫 1o → ∀𝑝 ∈ 𝒫 1o𝑛 ∈ ω 𝑝𝑓𝑛)
6362adantl 275 . . . . . 6 ((∀𝑟(𝑟 ⊆ (𝒫 1o × ω) → (∀𝑝 ∈ 𝒫 1o𝑛 ∈ ω 𝑝𝑟𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚)) ∧ 𝑓:ω–onto→𝒫 1o) → ∀𝑝 ∈ 𝒫 1o𝑛 ∈ ω 𝑝𝑓𝑛)
64 cnvexg 5083 . . . . . . . 8 (𝑓 ∈ V → 𝑓 ∈ V)
6564elv 2693 . . . . . . 7 𝑓 ∈ V
66 simpl 108 . . . . . . 7 ((∀𝑟(𝑟 ⊆ (𝒫 1o × ω) → (∀𝑝 ∈ 𝒫 1o𝑛 ∈ ω 𝑝𝑟𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚)) ∧ 𝑓:ω–onto→𝒫 1o) → ∀𝑟(𝑟 ⊆ (𝒫 1o × ω) → (∀𝑝 ∈ 𝒫 1o𝑛 ∈ ω 𝑝𝑟𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚)))
67 sseq1 3124 . . . . . . . . 9 (𝑟 = 𝑓 → (𝑟 ⊆ (𝒫 1o × ω) ↔ 𝑓 ⊆ (𝒫 1o × ω)))
68 breq 3938 . . . . . . . . . . . 12 (𝑟 = 𝑓 → (𝑝𝑟𝑛𝑝𝑓𝑛))
6968rexbidv 2439 . . . . . . . . . . 11 (𝑟 = 𝑓 → (∃𝑛 ∈ ω 𝑝𝑟𝑛 ↔ ∃𝑛 ∈ ω 𝑝𝑓𝑛))
7069ralbidv 2438 . . . . . . . . . 10 (𝑟 = 𝑓 → (∀𝑝 ∈ 𝒫 1o𝑛 ∈ ω 𝑝𝑟𝑛 ↔ ∀𝑝 ∈ 𝒫 1o𝑛 ∈ ω 𝑝𝑓𝑛))
71 breq 3938 . . . . . . . . . . . 12 (𝑟 = 𝑓 → (𝑞𝑟𝑚𝑞𝑓𝑚))
7271ralbidv 2438 . . . . . . . . . . 11 (𝑟 = 𝑓 → (∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚 ↔ ∀𝑞 ∈ 𝒫 1o𝑞𝑓𝑚))
7372rexbidv 2439 . . . . . . . . . 10 (𝑟 = 𝑓 → (∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚 ↔ ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑓𝑚))
7470, 73imbi12d 233 . . . . . . . . 9 (𝑟 = 𝑓 → ((∀𝑝 ∈ 𝒫 1o𝑛 ∈ ω 𝑝𝑟𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚) ↔ (∀𝑝 ∈ 𝒫 1o𝑛 ∈ ω 𝑝𝑓𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑓𝑚)))
7567, 74imbi12d 233 . . . . . . . 8 (𝑟 = 𝑓 → ((𝑟 ⊆ (𝒫 1o × ω) → (∀𝑝 ∈ 𝒫 1o𝑛 ∈ ω 𝑝𝑟𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚)) ↔ (𝑓 ⊆ (𝒫 1o × ω) → (∀𝑝 ∈ 𝒫 1o𝑛 ∈ ω 𝑝𝑓𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑓𝑚))))
7675spcgv 2776 . . . . . . 7 (𝑓 ∈ V → (∀𝑟(𝑟 ⊆ (𝒫 1o × ω) → (∀𝑝 ∈ 𝒫 1o𝑛 ∈ ω 𝑝𝑟𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚)) → (𝑓 ⊆ (𝒫 1o × ω) → (∀𝑝 ∈ 𝒫 1o𝑛 ∈ ω 𝑝𝑓𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑓𝑚))))
7765, 66, 76mpsyl 65 . . . . . 6 ((∀𝑟(𝑟 ⊆ (𝒫 1o × ω) → (∀𝑝 ∈ 𝒫 1o𝑛 ∈ ω 𝑝𝑟𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚)) ∧ 𝑓:ω–onto→𝒫 1o) → (𝑓 ⊆ (𝒫 1o × ω) → (∀𝑝 ∈ 𝒫 1o𝑛 ∈ ω 𝑝𝑓𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑓𝑚)))
7848, 63, 77mp2d 47 . . . . 5 ((∀𝑟(𝑟 ⊆ (𝒫 1o × ω) → (∀𝑝 ∈ 𝒫 1o𝑛 ∈ ω 𝑝𝑟𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚)) ∧ 𝑓:ω–onto→𝒫 1o) → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑓𝑚)
798, 40, 78r19.29af 2576 . . . 4 ((∀𝑟(𝑟 ⊆ (𝒫 1o × ω) → (∀𝑝 ∈ 𝒫 1o𝑛 ∈ ω 𝑝𝑟𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚)) ∧ 𝑓:ω–onto→𝒫 1o) → ⊥)
8079inegd 1351 . . 3 (∀𝑟(𝑟 ⊆ (𝒫 1o × ω) → (∀𝑝 ∈ 𝒫 1o𝑛 ∈ ω 𝑝𝑟𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚)) → ¬ 𝑓:ω–onto→𝒫 1o)
8180nexdv 1909 . 2 (∀𝑟(𝑟 ⊆ (𝒫 1o × ω) → (∀𝑝 ∈ 𝒫 1o𝑛 ∈ ω 𝑝𝑟𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚)) → ¬ ∃𝑓 𝑓:ω–onto→𝒫 1o)
82 elex2 2705 . . 3 (∅ ∈ 𝒫 1o → ∃𝑤 𝑤 ∈ 𝒫 1o)
83 ctm 7001 . . 3 (∃𝑤 𝑤 ∈ 𝒫 1o → (∃𝑓 𝑓:ω–onto→(𝒫 1o ⊔ 1o) ↔ ∃𝑓 𝑓:ω–onto→𝒫 1o))
8411, 82, 83mp2b 8 . 2 (∃𝑓 𝑓:ω–onto→(𝒫 1o ⊔ 1o) ↔ ∃𝑓 𝑓:ω–onto→𝒫 1o)
8581, 84sylnibr 667 1 (∀𝑟(𝑟 ⊆ (𝒫 1o × ω) → (∀𝑝 ∈ 𝒫 1o𝑛 ∈ ω 𝑝𝑟𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚)) → ¬ ∃𝑓 𝑓:ω–onto→(𝒫 1o ⊔ 1o))
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104  ∀wal 1330   = wceq 1332  ⊥wfal 1337  ∃wex 1469   ∈ wcel 1481  ∀wral 2417  ∃wrex 2418  Vcvv 2689   ⊆ wss 3075  ∅c0 3367  𝒫 cpw 3514   class class class wbr 3936  ωcom 4511   × cxp 4544  ◡ccnv 4545   Fn wfn 5125  ⟶wf 5126  –onto→wfo 5128  ‘cfv 5130  1oc1o 6313   ⊔ cdju 6929 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-coll 4050  ax-sep 4053  ax-nul 4061  ax-pow 4105  ax-pr 4138  ax-un 4362  ax-iinf 4509 This theorem depends on definitions:  df-bi 116  df-dc 821  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ne 2310  df-ral 2422  df-rex 2423  df-reu 2424  df-rab 2426  df-v 2691  df-sbc 2913  df-csb 3007  df-dif 3077  df-un 3079  df-in 3081  df-ss 3088  df-nul 3368  df-if 3479  df-pw 3516  df-sn 3537  df-pr 3538  df-op 3540  df-uni 3744  df-int 3779  df-iun 3822  df-br 3937  df-opab 3997  df-mpt 3998  df-tr 4034  df-id 4222  df-iord 4295  df-on 4297  df-suc 4300  df-iom 4512  df-xp 4552  df-rel 4553  df-cnv 4554  df-co 4555  df-dm 4556  df-rn 4557  df-res 4558  df-ima 4559  df-iota 5095  df-fun 5132  df-fn 5133  df-f 5134  df-f1 5135  df-fo 5136  df-f1o 5137  df-fv 5138  df-1st 6045  df-2nd 6046  df-1o 6320  df-dju 6930  df-inl 6939  df-inr 6940  df-case 6976 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator