MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pwfseqlem1 Structured version   Visualization version   GIF version
Theorem pwfseqlem1 10649
Description: Lemma for pwfseq 10655. Derive a contradiction by diagonalization. (Contributed by Mario Carneiro, 31-May-2015.)
Hypotheses
Ref Expression
pwfseqlem4.g (πœ‘ β†’ 𝐺:𝒫 𝐴–1-1β†’βˆͺ 𝑛 ∈ Ο‰ (𝐴 ↑m 𝑛))
pwfseqlem4.x (πœ‘ β†’ 𝑋 βŠ† 𝐴)
pwfseqlem4.h (πœ‘ β†’ 𝐻:ω–1-1-onto→𝑋)
pwfseqlem4.ps (πœ“ ↔ ((π‘₯ βŠ† 𝐴 ∧ π‘Ÿ βŠ† (π‘₯ Γ— π‘₯) ∧ π‘Ÿ We π‘₯) ∧ Ο‰ β‰Ό π‘₯))
pwfseqlem4.k ((πœ‘ ∧ πœ“) β†’ 𝐾:βˆͺ 𝑛 ∈ Ο‰ (π‘₯ ↑m 𝑛)–1-1β†’π‘₯)
pwfseqlem4.d 𝐷 = (πΊβ€˜{𝑀 ∈ π‘₯ ∣ ((β—‘πΎβ€˜π‘€) ∈ ran 𝐺 ∧ Β¬ 𝑀 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘€)))})
Assertion
Ref Expression
pwfseqlem1 ((πœ‘ ∧ πœ“) β†’ 𝐷 ∈ (βˆͺ 𝑛 ∈ Ο‰ (𝐴 ↑m 𝑛) βˆ– βˆͺ 𝑛 ∈ Ο‰ (π‘₯ ↑m 𝑛)))
Distinct variable groups:   𝑛,π‘Ÿ,𝑀,π‘₯   𝐷,𝑛   𝑀,𝐺   𝑀,𝐾   𝐻,π‘Ÿ,π‘₯   πœ‘,𝑛,π‘Ÿ,π‘₯   πœ“,𝑛   𝐴,𝑛,π‘Ÿ,π‘₯
Allowed substitution hints:   πœ‘(𝑀)   πœ“(π‘₯,𝑀,π‘Ÿ)   𝐴(𝑀)   𝐷(π‘₯,𝑀,π‘Ÿ)   𝐺(π‘₯,𝑛,π‘Ÿ)   𝐻(𝑀,𝑛)   𝐾(π‘₯,𝑛,π‘Ÿ)   𝑋(π‘₯,𝑀,𝑛,π‘Ÿ)
Proof of Theorem pwfseqlem1
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 pwfseqlem4.d . . 3 𝐷 = (πΊβ€˜{𝑀 ∈ π‘₯ ∣ ((β—‘πΎβ€˜π‘€) ∈ ran 𝐺 ∧ Β¬ 𝑀 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘€)))})
2 pwfseqlem4.g . . . . . 6 (πœ‘ β†’ 𝐺:𝒫 𝐴–1-1β†’βˆͺ 𝑛 ∈ Ο‰ (𝐴 ↑m 𝑛))
32adantr 481 . . . . 5 ((πœ‘ ∧ πœ“) β†’ 𝐺:𝒫 𝐴–1-1β†’βˆͺ 𝑛 ∈ Ο‰ (𝐴 ↑m 𝑛))
4 f1f 6784 . . . . 5 (𝐺:𝒫 𝐴–1-1β†’βˆͺ 𝑛 ∈ Ο‰ (𝐴 ↑m 𝑛) β†’ 𝐺:𝒫 𝐴⟢βˆͺ 𝑛 ∈ Ο‰ (𝐴 ↑m 𝑛))
53, 4syl 17 . . . 4 ((πœ‘ ∧ πœ“) β†’ 𝐺:𝒫 𝐴⟢βˆͺ 𝑛 ∈ Ο‰ (𝐴 ↑m 𝑛))
6 ssrab2 4076 . . . . . 6 {𝑀 ∈ π‘₯ ∣ ((β—‘πΎβ€˜π‘€) ∈ ran 𝐺 ∧ Β¬ 𝑀 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘€)))} βŠ† π‘₯
7 pwfseqlem4.ps . . . . . . 7 (πœ“ ↔ ((π‘₯ βŠ† 𝐴 ∧ π‘Ÿ βŠ† (π‘₯ Γ— π‘₯) ∧ π‘Ÿ We π‘₯) ∧ Ο‰ β‰Ό π‘₯))
8 simprl1 1218 . . . . . . 7 ((πœ‘ ∧ ((π‘₯ βŠ† 𝐴 ∧ π‘Ÿ βŠ† (π‘₯ Γ— π‘₯) ∧ π‘Ÿ We π‘₯) ∧ Ο‰ β‰Ό π‘₯)) β†’ π‘₯ βŠ† 𝐴)
97, 8sylan2b 594 . . . . . 6 ((πœ‘ ∧ πœ“) β†’ π‘₯ βŠ† 𝐴)
106, 9sstrid 3992 . . . . 5 ((πœ‘ ∧ πœ“) β†’ {𝑀 ∈ π‘₯ ∣ ((β—‘πΎβ€˜π‘€) ∈ ran 𝐺 ∧ Β¬ 𝑀 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘€)))} βŠ† 𝐴)
11 vex 3478 . . . . . . 7 π‘₯ ∈ V
1211rabex 5331 . . . . . 6 {𝑀 ∈ π‘₯ ∣ ((β—‘πΎβ€˜π‘€) ∈ ran 𝐺 ∧ Β¬ 𝑀 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘€)))} ∈ V
1312elpw 4605 . . . . 5 ({𝑀 ∈ π‘₯ ∣ ((β—‘πΎβ€˜π‘€) ∈ ran 𝐺 ∧ Β¬ 𝑀 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘€)))} ∈ 𝒫 𝐴 ↔ {𝑀 ∈ π‘₯ ∣ ((β—‘πΎβ€˜π‘€) ∈ ran 𝐺 ∧ Β¬ 𝑀 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘€)))} βŠ† 𝐴)
1410, 13sylibr 233 . . . 4 ((πœ‘ ∧ πœ“) β†’ {𝑀 ∈ π‘₯ ∣ ((β—‘πΎβ€˜π‘€) ∈ ran 𝐺 ∧ Β¬ 𝑀 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘€)))} ∈ 𝒫 𝐴)
155, 14ffvelcdmd 7084 . . 3 ((πœ‘ ∧ πœ“) β†’ (πΊβ€˜{𝑀 ∈ π‘₯ ∣ ((β—‘πΎβ€˜π‘€) ∈ ran 𝐺 ∧ Β¬ 𝑀 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘€)))}) ∈ βˆͺ 𝑛 ∈ Ο‰ (𝐴 ↑m 𝑛))
161, 15eqeltrid 2837 . 2 ((πœ‘ ∧ πœ“) β†’ 𝐷 ∈ βˆͺ 𝑛 ∈ Ο‰ (𝐴 ↑m 𝑛))
17 pm5.19 387 . . 3 Β¬ ((πΎβ€˜π·) ∈ {𝑀 ∈ π‘₯ ∣ ((β—‘πΎβ€˜π‘€) ∈ ran 𝐺 ∧ Β¬ 𝑀 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘€)))} ↔ Β¬ (πΎβ€˜π·) ∈ {𝑀 ∈ π‘₯ ∣ ((β—‘πΎβ€˜π‘€) ∈ ran 𝐺 ∧ Β¬ 𝑀 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘€)))})
18 pwfseqlem4.k . . . . . . . . 9 ((πœ‘ ∧ πœ“) β†’ 𝐾:βˆͺ 𝑛 ∈ Ο‰ (π‘₯ ↑m 𝑛)–1-1β†’π‘₯)
1918adantr 481 . . . . . . . 8 (((πœ‘ ∧ πœ“) ∧ 𝐷 ∈ βˆͺ 𝑛 ∈ Ο‰ (π‘₯ ↑m 𝑛)) β†’ 𝐾:βˆͺ 𝑛 ∈ Ο‰ (π‘₯ ↑m 𝑛)–1-1β†’π‘₯)
20 f1f 6784 . . . . . . . 8 (𝐾:βˆͺ 𝑛 ∈ Ο‰ (π‘₯ ↑m 𝑛)–1-1β†’π‘₯ β†’ 𝐾:βˆͺ 𝑛 ∈ Ο‰ (π‘₯ ↑m 𝑛)⟢π‘₯)
2119, 20syl 17 . . . . . . 7 (((πœ‘ ∧ πœ“) ∧ 𝐷 ∈ βˆͺ 𝑛 ∈ Ο‰ (π‘₯ ↑m 𝑛)) β†’ 𝐾:βˆͺ 𝑛 ∈ Ο‰ (π‘₯ ↑m 𝑛)⟢π‘₯)
22 ffvelcdm 7080 . . . . . . 7 ((𝐾:βˆͺ 𝑛 ∈ Ο‰ (π‘₯ ↑m 𝑛)⟢π‘₯ ∧ 𝐷 ∈ βˆͺ 𝑛 ∈ Ο‰ (π‘₯ ↑m 𝑛)) β†’ (πΎβ€˜π·) ∈ π‘₯)
2321, 22sylancom 588 . . . . . 6 (((πœ‘ ∧ πœ“) ∧ 𝐷 ∈ βˆͺ 𝑛 ∈ Ο‰ (π‘₯ ↑m 𝑛)) β†’ (πΎβ€˜π·) ∈ π‘₯)
24 f1f1orn 6841 . . . . . . . . 9 (𝐾:βˆͺ 𝑛 ∈ Ο‰ (π‘₯ ↑m 𝑛)–1-1β†’π‘₯ β†’ 𝐾:βˆͺ 𝑛 ∈ Ο‰ (π‘₯ ↑m 𝑛)–1-1-ontoβ†’ran 𝐾)
2519, 24syl 17 . . . . . . . 8 (((πœ‘ ∧ πœ“) ∧ 𝐷 ∈ βˆͺ 𝑛 ∈ Ο‰ (π‘₯ ↑m 𝑛)) β†’ 𝐾:βˆͺ 𝑛 ∈ Ο‰ (π‘₯ ↑m 𝑛)–1-1-ontoβ†’ran 𝐾)
26 f1ocnvfv1 7270 . . . . . . . 8 ((𝐾:βˆͺ 𝑛 ∈ Ο‰ (π‘₯ ↑m 𝑛)–1-1-ontoβ†’ran 𝐾 ∧ 𝐷 ∈ βˆͺ 𝑛 ∈ Ο‰ (π‘₯ ↑m 𝑛)) β†’ (β—‘πΎβ€˜(πΎβ€˜π·)) = 𝐷)
2725, 26sylancom 588 . . . . . . 7 (((πœ‘ ∧ πœ“) ∧ 𝐷 ∈ βˆͺ 𝑛 ∈ Ο‰ (π‘₯ ↑m 𝑛)) β†’ (β—‘πΎβ€˜(πΎβ€˜π·)) = 𝐷)
28 f1fn 6785 . . . . . . . . . . 11 (𝐺:𝒫 𝐴–1-1β†’βˆͺ 𝑛 ∈ Ο‰ (𝐴 ↑m 𝑛) β†’ 𝐺 Fn 𝒫 𝐴)
293, 28syl 17 . . . . . . . . . 10 ((πœ‘ ∧ πœ“) β†’ 𝐺 Fn 𝒫 𝐴)
30 fnfvelrn 7079 . . . . . . . . . 10 ((𝐺 Fn 𝒫 𝐴 ∧ {𝑀 ∈ π‘₯ ∣ ((β—‘πΎβ€˜π‘€) ∈ ran 𝐺 ∧ Β¬ 𝑀 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘€)))} ∈ 𝒫 𝐴) β†’ (πΊβ€˜{𝑀 ∈ π‘₯ ∣ ((β—‘πΎβ€˜π‘€) ∈ ran 𝐺 ∧ Β¬ 𝑀 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘€)))}) ∈ ran 𝐺)
3129, 14, 30syl2anc 584 . . . . . . . . 9 ((πœ‘ ∧ πœ“) β†’ (πΊβ€˜{𝑀 ∈ π‘₯ ∣ ((β—‘πΎβ€˜π‘€) ∈ ran 𝐺 ∧ Β¬ 𝑀 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘€)))}) ∈ ran 𝐺)
321, 31eqeltrid 2837 . . . . . . . 8 ((πœ‘ ∧ πœ“) β†’ 𝐷 ∈ ran 𝐺)
3332adantr 481 . . . . . . 7 (((πœ‘ ∧ πœ“) ∧ 𝐷 ∈ βˆͺ 𝑛 ∈ Ο‰ (π‘₯ ↑m 𝑛)) β†’ 𝐷 ∈ ran 𝐺)
3427, 33eqeltrd 2833 . . . . . 6 (((πœ‘ ∧ πœ“) ∧ 𝐷 ∈ βˆͺ 𝑛 ∈ Ο‰ (π‘₯ ↑m 𝑛)) β†’ (β—‘πΎβ€˜(πΎβ€˜π·)) ∈ ran 𝐺)
35 fveq2 6888 . . . . . . . . . . 11 (𝑦 = (πΎβ€˜π·) β†’ (β—‘πΎβ€˜π‘¦) = (β—‘πΎβ€˜(πΎβ€˜π·)))
3635eleq1d 2818 . . . . . . . . . 10 (𝑦 = (πΎβ€˜π·) β†’ ((β—‘πΎβ€˜π‘¦) ∈ ran 𝐺 ↔ (β—‘πΎβ€˜(πΎβ€˜π·)) ∈ ran 𝐺))
37 id 22 . . . . . . . . . . . 12 (𝑦 = (πΎβ€˜π·) β†’ 𝑦 = (πΎβ€˜π·))
38 2fveq3 6893 . . . . . . . . . . . 12 (𝑦 = (πΎβ€˜π·) β†’ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘¦)) = (β—‘πΊβ€˜(β—‘πΎβ€˜(πΎβ€˜π·))))
3937, 38eleq12d 2827 . . . . . . . . . . 11 (𝑦 = (πΎβ€˜π·) β†’ (𝑦 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘¦)) ↔ (πΎβ€˜π·) ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜(πΎβ€˜π·)))))
4039notbid 317 . . . . . . . . . 10 (𝑦 = (πΎβ€˜π·) β†’ (Β¬ 𝑦 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘¦)) ↔ Β¬ (πΎβ€˜π·) ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜(πΎβ€˜π·)))))
4136, 40anbi12d 631 . . . . . . . . 9 (𝑦 = (πΎβ€˜π·) β†’ (((β—‘πΎβ€˜π‘¦) ∈ ran 𝐺 ∧ Β¬ 𝑦 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘¦))) ↔ ((β—‘πΎβ€˜(πΎβ€˜π·)) ∈ ran 𝐺 ∧ Β¬ (πΎβ€˜π·) ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜(πΎβ€˜π·))))))
42 fveq2 6888 . . . . . . . . . . . 12 (𝑀 = 𝑦 β†’ (β—‘πΎβ€˜π‘€) = (β—‘πΎβ€˜π‘¦))
4342eleq1d 2818 . . . . . . . . . . 11 (𝑀 = 𝑦 β†’ ((β—‘πΎβ€˜π‘€) ∈ ran 𝐺 ↔ (β—‘πΎβ€˜π‘¦) ∈ ran 𝐺))
44 id 22 . . . . . . . . . . . . 13 (𝑀 = 𝑦 β†’ 𝑀 = 𝑦)
45 2fveq3 6893 . . . . . . . . . . . . 13 (𝑀 = 𝑦 β†’ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘€)) = (β—‘πΊβ€˜(β—‘πΎβ€˜π‘¦)))
4644, 45eleq12d 2827 . . . . . . . . . . . 12 (𝑀 = 𝑦 β†’ (𝑀 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘€)) ↔ 𝑦 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘¦))))
4746notbid 317 . . . . . . . . . . 11 (𝑀 = 𝑦 β†’ (Β¬ 𝑀 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘€)) ↔ Β¬ 𝑦 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘¦))))
4843, 47anbi12d 631 . . . . . . . . . 10 (𝑀 = 𝑦 β†’ (((β—‘πΎβ€˜π‘€) ∈ ran 𝐺 ∧ Β¬ 𝑀 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘€))) ↔ ((β—‘πΎβ€˜π‘¦) ∈ ran 𝐺 ∧ Β¬ 𝑦 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘¦)))))
4948cbvrabv 3442 . . . . . . . . 9 {𝑀 ∈ π‘₯ ∣ ((β—‘πΎβ€˜π‘€) ∈ ran 𝐺 ∧ Β¬ 𝑀 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘€)))} = {𝑦 ∈ π‘₯ ∣ ((β—‘πΎβ€˜π‘¦) ∈ ran 𝐺 ∧ Β¬ 𝑦 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘¦)))}
5041, 49elrab2 3685 . . . . . . . 8 ((πΎβ€˜π·) ∈ {𝑀 ∈ π‘₯ ∣ ((β—‘πΎβ€˜π‘€) ∈ ran 𝐺 ∧ Β¬ 𝑀 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘€)))} ↔ ((πΎβ€˜π·) ∈ π‘₯ ∧ ((β—‘πΎβ€˜(πΎβ€˜π·)) ∈ ran 𝐺 ∧ Β¬ (πΎβ€˜π·) ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜(πΎβ€˜π·))))))
51 anass 469 . . . . . . . 8 ((((πΎβ€˜π·) ∈ π‘₯ ∧ (β—‘πΎβ€˜(πΎβ€˜π·)) ∈ ran 𝐺) ∧ Β¬ (πΎβ€˜π·) ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜(πΎβ€˜π·)))) ↔ ((πΎβ€˜π·) ∈ π‘₯ ∧ ((β—‘πΎβ€˜(πΎβ€˜π·)) ∈ ran 𝐺 ∧ Β¬ (πΎβ€˜π·) ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜(πΎβ€˜π·))))))
5250, 51bitr4i 277 . . . . . . 7 ((πΎβ€˜π·) ∈ {𝑀 ∈ π‘₯ ∣ ((β—‘πΎβ€˜π‘€) ∈ ran 𝐺 ∧ Β¬ 𝑀 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘€)))} ↔ (((πΎβ€˜π·) ∈ π‘₯ ∧ (β—‘πΎβ€˜(πΎβ€˜π·)) ∈ ran 𝐺) ∧ Β¬ (πΎβ€˜π·) ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜(πΎβ€˜π·)))))
5352baib 536 . . . . . 6 (((πΎβ€˜π·) ∈ π‘₯ ∧ (β—‘πΎβ€˜(πΎβ€˜π·)) ∈ ran 𝐺) β†’ ((πΎβ€˜π·) ∈ {𝑀 ∈ π‘₯ ∣ ((β—‘πΎβ€˜π‘€) ∈ ran 𝐺 ∧ Β¬ 𝑀 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘€)))} ↔ Β¬ (πΎβ€˜π·) ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜(πΎβ€˜π·)))))
5423, 34, 53syl2anc 584 . . . . 5 (((πœ‘ ∧ πœ“) ∧ 𝐷 ∈ βˆͺ 𝑛 ∈ Ο‰ (π‘₯ ↑m 𝑛)) β†’ ((πΎβ€˜π·) ∈ {𝑀 ∈ π‘₯ ∣ ((β—‘πΎβ€˜π‘€) ∈ ran 𝐺 ∧ Β¬ 𝑀 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘€)))} ↔ Β¬ (πΎβ€˜π·) ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜(πΎβ€˜π·)))))
5527, 1eqtrdi 2788 . . . . . . . . 9 (((πœ‘ ∧ πœ“) ∧ 𝐷 ∈ βˆͺ 𝑛 ∈ Ο‰ (π‘₯ ↑m 𝑛)) β†’ (β—‘πΎβ€˜(πΎβ€˜π·)) = (πΊβ€˜{𝑀 ∈ π‘₯ ∣ ((β—‘πΎβ€˜π‘€) ∈ ran 𝐺 ∧ Β¬ 𝑀 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘€)))}))
5655fveq2d 6892 . . . . . . . 8 (((πœ‘ ∧ πœ“) ∧ 𝐷 ∈ βˆͺ 𝑛 ∈ Ο‰ (π‘₯ ↑m 𝑛)) β†’ (β—‘πΊβ€˜(β—‘πΎβ€˜(πΎβ€˜π·))) = (β—‘πΊβ€˜(πΊβ€˜{𝑀 ∈ π‘₯ ∣ ((β—‘πΎβ€˜π‘€) ∈ ran 𝐺 ∧ Β¬ 𝑀 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘€)))})))
57 f1f1orn 6841 . . . . . . . . . . 11 (𝐺:𝒫 𝐴–1-1β†’βˆͺ 𝑛 ∈ Ο‰ (𝐴 ↑m 𝑛) β†’ 𝐺:𝒫 𝐴–1-1-ontoβ†’ran 𝐺)
583, 57syl 17 . . . . . . . . . 10 ((πœ‘ ∧ πœ“) β†’ 𝐺:𝒫 𝐴–1-1-ontoβ†’ran 𝐺)
59 f1ocnvfv1 7270 . . . . . . . . . 10 ((𝐺:𝒫 𝐴–1-1-ontoβ†’ran 𝐺 ∧ {𝑀 ∈ π‘₯ ∣ ((β—‘πΎβ€˜π‘€) ∈ ran 𝐺 ∧ Β¬ 𝑀 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘€)))} ∈ 𝒫 𝐴) β†’ (β—‘πΊβ€˜(πΊβ€˜{𝑀 ∈ π‘₯ ∣ ((β—‘πΎβ€˜π‘€) ∈ ran 𝐺 ∧ Β¬ 𝑀 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘€)))})) = {𝑀 ∈ π‘₯ ∣ ((β—‘πΎβ€˜π‘€) ∈ ran 𝐺 ∧ Β¬ 𝑀 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘€)))})
6058, 14, 59syl2anc 584 . . . . . . . . 9 ((πœ‘ ∧ πœ“) β†’ (β—‘πΊβ€˜(πΊβ€˜{𝑀 ∈ π‘₯ ∣ ((β—‘πΎβ€˜π‘€) ∈ ran 𝐺 ∧ Β¬ 𝑀 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘€)))})) = {𝑀 ∈ π‘₯ ∣ ((β—‘πΎβ€˜π‘€) ∈ ran 𝐺 ∧ Β¬ 𝑀 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘€)))})
6160adantr 481 . . . . . . . 8 (((πœ‘ ∧ πœ“) ∧ 𝐷 ∈ βˆͺ 𝑛 ∈ Ο‰ (π‘₯ ↑m 𝑛)) β†’ (β—‘πΊβ€˜(πΊβ€˜{𝑀 ∈ π‘₯ ∣ ((β—‘πΎβ€˜π‘€) ∈ ran 𝐺 ∧ Β¬ 𝑀 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘€)))})) = {𝑀 ∈ π‘₯ ∣ ((β—‘πΎβ€˜π‘€) ∈ ran 𝐺 ∧ Β¬ 𝑀 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘€)))})
6256, 61eqtrd 2772 . . . . . . 7 (((πœ‘ ∧ πœ“) ∧ 𝐷 ∈ βˆͺ 𝑛 ∈ Ο‰ (π‘₯ ↑m 𝑛)) β†’ (β—‘πΊβ€˜(β—‘πΎβ€˜(πΎβ€˜π·))) = {𝑀 ∈ π‘₯ ∣ ((β—‘πΎβ€˜π‘€) ∈ ran 𝐺 ∧ Β¬ 𝑀 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘€)))})
6362eleq2d 2819 . . . . . 6 (((πœ‘ ∧ πœ“) ∧ 𝐷 ∈ βˆͺ 𝑛 ∈ Ο‰ (π‘₯ ↑m 𝑛)) β†’ ((πΎβ€˜π·) ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜(πΎβ€˜π·))) ↔ (πΎβ€˜π·) ∈ {𝑀 ∈ π‘₯ ∣ ((β—‘πΎβ€˜π‘€) ∈ ran 𝐺 ∧ Β¬ 𝑀 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘€)))}))
6463notbid 317 . . . . 5 (((πœ‘ ∧ πœ“) ∧ 𝐷 ∈ βˆͺ 𝑛 ∈ Ο‰ (π‘₯ ↑m 𝑛)) β†’ (Β¬ (πΎβ€˜π·) ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜(πΎβ€˜π·))) ↔ Β¬ (πΎβ€˜π·) ∈ {𝑀 ∈ π‘₯ ∣ ((β—‘πΎβ€˜π‘€) ∈ ran 𝐺 ∧ Β¬ 𝑀 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘€)))}))
6554, 64bitrd 278 . . . 4 (((πœ‘ ∧ πœ“) ∧ 𝐷 ∈ βˆͺ 𝑛 ∈ Ο‰ (π‘₯ ↑m 𝑛)) β†’ ((πΎβ€˜π·) ∈ {𝑀 ∈ π‘₯ ∣ ((β—‘πΎβ€˜π‘€) ∈ ran 𝐺 ∧ Β¬ 𝑀 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘€)))} ↔ Β¬ (πΎβ€˜π·) ∈ {𝑀 ∈ π‘₯ ∣ ((β—‘πΎβ€˜π‘€) ∈ ran 𝐺 ∧ Β¬ 𝑀 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘€)))}))
6665ex 413 . . 3 ((πœ‘ ∧ πœ“) β†’ (𝐷 ∈ βˆͺ 𝑛 ∈ Ο‰ (π‘₯ ↑m 𝑛) β†’ ((πΎβ€˜π·) ∈ {𝑀 ∈ π‘₯ ∣ ((β—‘πΎβ€˜π‘€) ∈ ran 𝐺 ∧ Β¬ 𝑀 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘€)))} ↔ Β¬ (πΎβ€˜π·) ∈ {𝑀 ∈ π‘₯ ∣ ((β—‘πΎβ€˜π‘€) ∈ ran 𝐺 ∧ Β¬ 𝑀 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘€)))})))
6717, 66mtoi 198 . 2 ((πœ‘ ∧ πœ“) β†’ Β¬ 𝐷 ∈ βˆͺ 𝑛 ∈ Ο‰ (π‘₯ ↑m 𝑛))
6816, 67eldifd 3958 1 ((πœ‘ ∧ πœ“) β†’ 𝐷 ∈ (βˆͺ 𝑛 ∈ Ο‰ (𝐴 ↑m 𝑛) βˆ– βˆͺ 𝑛 ∈ Ο‰ (π‘₯ ↑m 𝑛)))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106  {crab 3432   βˆ– cdif 3944   βŠ† wss 3947  π’« cpw 4601  βˆͺ ciun 4996   class class class wbr 5147   We wwe 5629   Γ— cxp 5673  β—‘ccnv 5674  ran crn 5676   Fn wfn 6535  βŸΆwf 6536  β€“1-1β†’wf1 6537  β€“1-1-ontoβ†’wf1o 6539  β€˜cfv 6540  (class class class)co 7405  Ο‰com 7851   ↑m cmap 8816   β‰Ό cdom 8933
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pr 5426
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548
This theorem is referenced by:  pwfseqlem3  10651
  Copyright terms: Public domain W3C validator