MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pwfseqlem3 Structured version   Visualization version   GIF version

Theorem pwfseqlem3 10657
Description: Lemma for pwfseq 10661. Using the construction 𝐷 from pwfseqlem1 10655, produce a function 𝐹 that maps any well-ordered infinite set to an element outside the set. (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 𝐺 ∧ Β¬ 𝑀 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘€)))})
pwfseqlem4.f 𝐹 = (π‘₯ ∈ V, π‘Ÿ ∈ V ↦ if(π‘₯ ∈ Fin, (π»β€˜(cardβ€˜π‘₯)), (π·β€˜βˆ© {𝑧 ∈ Ο‰ ∣ Β¬ (π·β€˜π‘§) ∈ π‘₯})))
Assertion
Ref Expression
pwfseqlem3 ((πœ‘ ∧ πœ“) β†’ (π‘₯πΉπ‘Ÿ) ∈ (𝐴 βˆ– π‘₯))
Distinct variable groups:   𝑛,π‘Ÿ,𝑀,π‘₯,𝑧   𝐷,𝑛,𝑧   𝑀,𝐺   𝑀,𝐾   𝐻,π‘Ÿ,π‘₯,𝑧   πœ‘,𝑛,π‘Ÿ,π‘₯,𝑧   πœ“,𝑛,𝑧   𝐴,𝑛,π‘Ÿ,π‘₯,𝑧
Allowed substitution hints:   πœ‘(𝑀)   πœ“(π‘₯,𝑀,π‘Ÿ)   𝐴(𝑀)   𝐷(π‘₯,𝑀,π‘Ÿ)   𝐹(π‘₯,𝑧,𝑀,𝑛,π‘Ÿ)   𝐺(π‘₯,𝑧,𝑛,π‘Ÿ)   𝐻(𝑀,𝑛)   𝐾(π‘₯,𝑧,𝑛,π‘Ÿ)   𝑋(π‘₯,𝑧,𝑀,𝑛,π‘Ÿ)

Proof of Theorem pwfseqlem3
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 vex 3478 . . . 4 π‘₯ ∈ V
2 vex 3478 . . . 4 π‘Ÿ ∈ V
3 fvex 6904 . . . . 5 (π»β€˜(cardβ€˜π‘₯)) ∈ V
4 fvex 6904 . . . . 5 (π·β€˜βˆ© {𝑧 ∈ Ο‰ ∣ Β¬ (π·β€˜π‘§) ∈ π‘₯}) ∈ V
53, 4ifex 4578 . . . 4 if(π‘₯ ∈ Fin, (π»β€˜(cardβ€˜π‘₯)), (π·β€˜βˆ© {𝑧 ∈ Ο‰ ∣ Β¬ (π·β€˜π‘§) ∈ π‘₯})) ∈ V
6 pwfseqlem4.f . . . . 5 𝐹 = (π‘₯ ∈ V, π‘Ÿ ∈ V ↦ if(π‘₯ ∈ Fin, (π»β€˜(cardβ€˜π‘₯)), (π·β€˜βˆ© {𝑧 ∈ Ο‰ ∣ Β¬ (π·β€˜π‘§) ∈ π‘₯})))
76ovmpt4g 7557 . . . 4 ((π‘₯ ∈ V ∧ π‘Ÿ ∈ V ∧ if(π‘₯ ∈ Fin, (π»β€˜(cardβ€˜π‘₯)), (π·β€˜βˆ© {𝑧 ∈ Ο‰ ∣ Β¬ (π·β€˜π‘§) ∈ π‘₯})) ∈ V) β†’ (π‘₯πΉπ‘Ÿ) = if(π‘₯ ∈ Fin, (π»β€˜(cardβ€˜π‘₯)), (π·β€˜βˆ© {𝑧 ∈ Ο‰ ∣ Β¬ (π·β€˜π‘§) ∈ π‘₯})))
81, 2, 5, 7mp3an 1461 . . 3 (π‘₯πΉπ‘Ÿ) = if(π‘₯ ∈ Fin, (π»β€˜(cardβ€˜π‘₯)), (π·β€˜βˆ© {𝑧 ∈ Ο‰ ∣ Β¬ (π·β€˜π‘§) ∈ π‘₯}))
9 pwfseqlem4.ps . . . . . . . 8 (πœ“ ↔ ((π‘₯ βŠ† 𝐴 ∧ π‘Ÿ βŠ† (π‘₯ Γ— π‘₯) ∧ π‘Ÿ We π‘₯) ∧ Ο‰ β‰Ό π‘₯))
109simprbi 497 . . . . . . 7 (πœ“ β†’ Ο‰ β‰Ό π‘₯)
1110adantl 482 . . . . . 6 ((πœ‘ ∧ πœ“) β†’ Ο‰ β‰Ό π‘₯)
12 domnsym 9101 . . . . . 6 (Ο‰ β‰Ό π‘₯ β†’ Β¬ π‘₯ β‰Ί Ο‰)
1311, 12syl 17 . . . . 5 ((πœ‘ ∧ πœ“) β†’ Β¬ π‘₯ β‰Ί Ο‰)
14 isfinite 9649 . . . . 5 (π‘₯ ∈ Fin ↔ π‘₯ β‰Ί Ο‰)
1513, 14sylnibr 328 . . . 4 ((πœ‘ ∧ πœ“) β†’ Β¬ π‘₯ ∈ Fin)
1615iffalsed 4539 . . 3 ((πœ‘ ∧ πœ“) β†’ if(π‘₯ ∈ Fin, (π»β€˜(cardβ€˜π‘₯)), (π·β€˜βˆ© {𝑧 ∈ Ο‰ ∣ Β¬ (π·β€˜π‘§) ∈ π‘₯})) = (π·β€˜βˆ© {𝑧 ∈ Ο‰ ∣ Β¬ (π·β€˜π‘§) ∈ π‘₯}))
178, 16eqtrid 2784 . 2 ((πœ‘ ∧ πœ“) β†’ (π‘₯πΉπ‘Ÿ) = (π·β€˜βˆ© {𝑧 ∈ Ο‰ ∣ Β¬ (π·β€˜π‘§) ∈ π‘₯}))
18 pwfseqlem4.g . . . . . . 7 (πœ‘ β†’ 𝐺:𝒫 𝐴–1-1β†’βˆͺ 𝑛 ∈ Ο‰ (𝐴 ↑m 𝑛))
19 pwfseqlem4.x . . . . . . 7 (πœ‘ β†’ 𝑋 βŠ† 𝐴)
20 pwfseqlem4.h . . . . . . 7 (πœ‘ β†’ 𝐻:ω–1-1-onto→𝑋)
21 pwfseqlem4.k . . . . . . 7 ((πœ‘ ∧ πœ“) β†’ 𝐾:βˆͺ 𝑛 ∈ Ο‰ (π‘₯ ↑m 𝑛)–1-1β†’π‘₯)
22 pwfseqlem4.d . . . . . . 7 𝐷 = (πΊβ€˜{𝑀 ∈ π‘₯ ∣ ((β—‘πΎβ€˜π‘€) ∈ ran 𝐺 ∧ Β¬ 𝑀 ∈ (β—‘πΊβ€˜(β—‘πΎβ€˜π‘€)))})
2318, 19, 20, 9, 21, 22pwfseqlem1 10655 . . . . . 6 ((πœ‘ ∧ πœ“) β†’ 𝐷 ∈ (βˆͺ 𝑛 ∈ Ο‰ (𝐴 ↑m 𝑛) βˆ– βˆͺ 𝑛 ∈ Ο‰ (π‘₯ ↑m 𝑛)))
24 eldif 3958 . . . . . 6 (𝐷 ∈ (βˆͺ 𝑛 ∈ Ο‰ (𝐴 ↑m 𝑛) βˆ– βˆͺ 𝑛 ∈ Ο‰ (π‘₯ ↑m 𝑛)) ↔ (𝐷 ∈ βˆͺ 𝑛 ∈ Ο‰ (𝐴 ↑m 𝑛) ∧ Β¬ 𝐷 ∈ βˆͺ 𝑛 ∈ Ο‰ (π‘₯ ↑m 𝑛)))
2523, 24sylib 217 . . . . 5 ((πœ‘ ∧ πœ“) β†’ (𝐷 ∈ βˆͺ 𝑛 ∈ Ο‰ (𝐴 ↑m 𝑛) ∧ Β¬ 𝐷 ∈ βˆͺ 𝑛 ∈ Ο‰ (π‘₯ ↑m 𝑛)))
2625simpld 495 . . . 4 ((πœ‘ ∧ πœ“) β†’ 𝐷 ∈ βˆͺ 𝑛 ∈ Ο‰ (𝐴 ↑m 𝑛))
27 eliun 5001 . . . 4 (𝐷 ∈ βˆͺ 𝑛 ∈ Ο‰ (𝐴 ↑m 𝑛) ↔ βˆƒπ‘› ∈ Ο‰ 𝐷 ∈ (𝐴 ↑m 𝑛))
2826, 27sylib 217 . . 3 ((πœ‘ ∧ πœ“) β†’ βˆƒπ‘› ∈ Ο‰ 𝐷 ∈ (𝐴 ↑m 𝑛))
29 elmapi 8845 . . . . . 6 (𝐷 ∈ (𝐴 ↑m 𝑛) β†’ 𝐷:π‘›βŸΆπ΄)
3029ad2antll 727 . . . . 5 (((πœ‘ ∧ πœ“) ∧ (𝑛 ∈ Ο‰ ∧ 𝐷 ∈ (𝐴 ↑m 𝑛))) β†’ 𝐷:π‘›βŸΆπ΄)
31 ssiun2 5050 . . . . . . . . 9 (𝑛 ∈ Ο‰ β†’ (π‘₯ ↑m 𝑛) βŠ† βˆͺ 𝑛 ∈ Ο‰ (π‘₯ ↑m 𝑛))
3231ad2antrl 726 . . . . . . . 8 (((πœ‘ ∧ πœ“) ∧ (𝑛 ∈ Ο‰ ∧ 𝐷 ∈ (𝐴 ↑m 𝑛))) β†’ (π‘₯ ↑m 𝑛) βŠ† βˆͺ 𝑛 ∈ Ο‰ (π‘₯ ↑m 𝑛))
3325simprd 496 . . . . . . . . 9 ((πœ‘ ∧ πœ“) β†’ Β¬ 𝐷 ∈ βˆͺ 𝑛 ∈ Ο‰ (π‘₯ ↑m 𝑛))
3433adantr 481 . . . . . . . 8 (((πœ‘ ∧ πœ“) ∧ (𝑛 ∈ Ο‰ ∧ 𝐷 ∈ (𝐴 ↑m 𝑛))) β†’ Β¬ 𝐷 ∈ βˆͺ 𝑛 ∈ Ο‰ (π‘₯ ↑m 𝑛))
3532, 34ssneldd 3985 . . . . . . 7 (((πœ‘ ∧ πœ“) ∧ (𝑛 ∈ Ο‰ ∧ 𝐷 ∈ (𝐴 ↑m 𝑛))) β†’ Β¬ 𝐷 ∈ (π‘₯ ↑m 𝑛))
36 vex 3478 . . . . . . . . 9 𝑛 ∈ V
371, 36elmap 8867 . . . . . . . 8 (𝐷 ∈ (π‘₯ ↑m 𝑛) ↔ 𝐷:π‘›βŸΆπ‘₯)
38 ffn 6717 . . . . . . . . 9 (𝐷:π‘›βŸΆπ΄ β†’ 𝐷 Fn 𝑛)
39 ffnfv 7120 . . . . . . . . . 10 (𝐷:π‘›βŸΆπ‘₯ ↔ (𝐷 Fn 𝑛 ∧ βˆ€π‘§ ∈ 𝑛 (π·β€˜π‘§) ∈ π‘₯))
4039baib 536 . . . . . . . . 9 (𝐷 Fn 𝑛 β†’ (𝐷:π‘›βŸΆπ‘₯ ↔ βˆ€π‘§ ∈ 𝑛 (π·β€˜π‘§) ∈ π‘₯))
4130, 38, 403syl 18 . . . . . . . 8 (((πœ‘ ∧ πœ“) ∧ (𝑛 ∈ Ο‰ ∧ 𝐷 ∈ (𝐴 ↑m 𝑛))) β†’ (𝐷:π‘›βŸΆπ‘₯ ↔ βˆ€π‘§ ∈ 𝑛 (π·β€˜π‘§) ∈ π‘₯))
4237, 41bitrid 282 . . . . . . 7 (((πœ‘ ∧ πœ“) ∧ (𝑛 ∈ Ο‰ ∧ 𝐷 ∈ (𝐴 ↑m 𝑛))) β†’ (𝐷 ∈ (π‘₯ ↑m 𝑛) ↔ βˆ€π‘§ ∈ 𝑛 (π·β€˜π‘§) ∈ π‘₯))
4335, 42mtbid 323 . . . . . 6 (((πœ‘ ∧ πœ“) ∧ (𝑛 ∈ Ο‰ ∧ 𝐷 ∈ (𝐴 ↑m 𝑛))) β†’ Β¬ βˆ€π‘§ ∈ 𝑛 (π·β€˜π‘§) ∈ π‘₯)
44 nnon 7863 . . . . . . . . 9 (𝑛 ∈ Ο‰ β†’ 𝑛 ∈ On)
4544ad2antrl 726 . . . . . . . 8 (((πœ‘ ∧ πœ“) ∧ (𝑛 ∈ Ο‰ ∧ 𝐷 ∈ (𝐴 ↑m 𝑛))) β†’ 𝑛 ∈ On)
46 ssrab2 4077 . . . . . . . . . 10 {𝑧 ∈ Ο‰ ∣ Β¬ (π·β€˜π‘§) ∈ π‘₯} βŠ† Ο‰
47 omsson 7861 . . . . . . . . . 10 Ο‰ βŠ† On
4846, 47sstri 3991 . . . . . . . . 9 {𝑧 ∈ Ο‰ ∣ Β¬ (π·β€˜π‘§) ∈ π‘₯} βŠ† On
49 ordom 7867 . . . . . . . . . . . . 13 Ord Ο‰
50 simprl 769 . . . . . . . . . . . . 13 (((πœ‘ ∧ πœ“) ∧ (𝑛 ∈ Ο‰ ∧ 𝐷 ∈ (𝐴 ↑m 𝑛))) β†’ 𝑛 ∈ Ο‰)
51 ordelss 6380 . . . . . . . . . . . . 13 ((Ord Ο‰ ∧ 𝑛 ∈ Ο‰) β†’ 𝑛 βŠ† Ο‰)
5249, 50, 51sylancr 587 . . . . . . . . . . . 12 (((πœ‘ ∧ πœ“) ∧ (𝑛 ∈ Ο‰ ∧ 𝐷 ∈ (𝐴 ↑m 𝑛))) β†’ 𝑛 βŠ† Ο‰)
53 rexnal 3100 . . . . . . . . . . . . 13 (βˆƒπ‘§ ∈ 𝑛 Β¬ (π·β€˜π‘§) ∈ π‘₯ ↔ Β¬ βˆ€π‘§ ∈ 𝑛 (π·β€˜π‘§) ∈ π‘₯)
5443, 53sylibr 233 . . . . . . . . . . . 12 (((πœ‘ ∧ πœ“) ∧ (𝑛 ∈ Ο‰ ∧ 𝐷 ∈ (𝐴 ↑m 𝑛))) β†’ βˆƒπ‘§ ∈ 𝑛 Β¬ (π·β€˜π‘§) ∈ π‘₯)
55 ssrexv 4051 . . . . . . . . . . . 12 (𝑛 βŠ† Ο‰ β†’ (βˆƒπ‘§ ∈ 𝑛 Β¬ (π·β€˜π‘§) ∈ π‘₯ β†’ βˆƒπ‘§ ∈ Ο‰ Β¬ (π·β€˜π‘§) ∈ π‘₯))
5652, 54, 55sylc 65 . . . . . . . . . . 11 (((πœ‘ ∧ πœ“) ∧ (𝑛 ∈ Ο‰ ∧ 𝐷 ∈ (𝐴 ↑m 𝑛))) β†’ βˆƒπ‘§ ∈ Ο‰ Β¬ (π·β€˜π‘§) ∈ π‘₯)
57 rabn0 4385 . . . . . . . . . . 11 ({𝑧 ∈ Ο‰ ∣ Β¬ (π·β€˜π‘§) ∈ π‘₯} β‰  βˆ… ↔ βˆƒπ‘§ ∈ Ο‰ Β¬ (π·β€˜π‘§) ∈ π‘₯)
5856, 57sylibr 233 . . . . . . . . . 10 (((πœ‘ ∧ πœ“) ∧ (𝑛 ∈ Ο‰ ∧ 𝐷 ∈ (𝐴 ↑m 𝑛))) β†’ {𝑧 ∈ Ο‰ ∣ Β¬ (π·β€˜π‘§) ∈ π‘₯} β‰  βˆ…)
59 onint 7780 . . . . . . . . . 10 (({𝑧 ∈ Ο‰ ∣ Β¬ (π·β€˜π‘§) ∈ π‘₯} βŠ† On ∧ {𝑧 ∈ Ο‰ ∣ Β¬ (π·β€˜π‘§) ∈ π‘₯} β‰  βˆ…) β†’ ∩ {𝑧 ∈ Ο‰ ∣ Β¬ (π·β€˜π‘§) ∈ π‘₯} ∈ {𝑧 ∈ Ο‰ ∣ Β¬ (π·β€˜π‘§) ∈ π‘₯})
6048, 58, 59sylancr 587 . . . . . . . . 9 (((πœ‘ ∧ πœ“) ∧ (𝑛 ∈ Ο‰ ∧ 𝐷 ∈ (𝐴 ↑m 𝑛))) β†’ ∩ {𝑧 ∈ Ο‰ ∣ Β¬ (π·β€˜π‘§) ∈ π‘₯} ∈ {𝑧 ∈ Ο‰ ∣ Β¬ (π·β€˜π‘§) ∈ π‘₯})
6148, 60sselid 3980 . . . . . . . 8 (((πœ‘ ∧ πœ“) ∧ (𝑛 ∈ Ο‰ ∧ 𝐷 ∈ (𝐴 ↑m 𝑛))) β†’ ∩ {𝑧 ∈ Ο‰ ∣ Β¬ (π·β€˜π‘§) ∈ π‘₯} ∈ On)
62 ontri1 6398 . . . . . . . 8 ((𝑛 ∈ On ∧ ∩ {𝑧 ∈ Ο‰ ∣ Β¬ (π·β€˜π‘§) ∈ π‘₯} ∈ On) β†’ (𝑛 βŠ† ∩ {𝑧 ∈ Ο‰ ∣ Β¬ (π·β€˜π‘§) ∈ π‘₯} ↔ Β¬ ∩ {𝑧 ∈ Ο‰ ∣ Β¬ (π·β€˜π‘§) ∈ π‘₯} ∈ 𝑛))
6345, 61, 62syl2anc 584 . . . . . . 7 (((πœ‘ ∧ πœ“) ∧ (𝑛 ∈ Ο‰ ∧ 𝐷 ∈ (𝐴 ↑m 𝑛))) β†’ (𝑛 βŠ† ∩ {𝑧 ∈ Ο‰ ∣ Β¬ (π·β€˜π‘§) ∈ π‘₯} ↔ Β¬ ∩ {𝑧 ∈ Ο‰ ∣ Β¬ (π·β€˜π‘§) ∈ π‘₯} ∈ 𝑛))
64 ssintrab 4975 . . . . . . . 8 (𝑛 βŠ† ∩ {𝑧 ∈ Ο‰ ∣ Β¬ (π·β€˜π‘§) ∈ π‘₯} ↔ βˆ€π‘§ ∈ Ο‰ (Β¬ (π·β€˜π‘§) ∈ π‘₯ β†’ 𝑛 βŠ† 𝑧))
65 nnon 7863 . . . . . . . . . . . . . . . 16 (𝑧 ∈ Ο‰ β†’ 𝑧 ∈ On)
66 ontri1 6398 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ On ∧ 𝑧 ∈ On) β†’ (𝑛 βŠ† 𝑧 ↔ Β¬ 𝑧 ∈ 𝑛))
6744, 65, 66syl2an 596 . . . . . . . . . . . . . . 15 ((𝑛 ∈ Ο‰ ∧ 𝑧 ∈ Ο‰) β†’ (𝑛 βŠ† 𝑧 ↔ Β¬ 𝑧 ∈ 𝑛))
6867imbi2d 340 . . . . . . . . . . . . . 14 ((𝑛 ∈ Ο‰ ∧ 𝑧 ∈ Ο‰) β†’ ((Β¬ (π·β€˜π‘§) ∈ π‘₯ β†’ 𝑛 βŠ† 𝑧) ↔ (Β¬ (π·β€˜π‘§) ∈ π‘₯ β†’ Β¬ 𝑧 ∈ 𝑛)))
69 con34b 315 . . . . . . . . . . . . . 14 ((𝑧 ∈ 𝑛 β†’ (π·β€˜π‘§) ∈ π‘₯) ↔ (Β¬ (π·β€˜π‘§) ∈ π‘₯ β†’ Β¬ 𝑧 ∈ 𝑛))
7068, 69bitr4di 288 . . . . . . . . . . . . 13 ((𝑛 ∈ Ο‰ ∧ 𝑧 ∈ Ο‰) β†’ ((Β¬ (π·β€˜π‘§) ∈ π‘₯ β†’ 𝑛 βŠ† 𝑧) ↔ (𝑧 ∈ 𝑛 β†’ (π·β€˜π‘§) ∈ π‘₯)))
7170pm5.74da 802 . . . . . . . . . . . 12 (𝑛 ∈ Ο‰ β†’ ((𝑧 ∈ Ο‰ β†’ (Β¬ (π·β€˜π‘§) ∈ π‘₯ β†’ 𝑛 βŠ† 𝑧)) ↔ (𝑧 ∈ Ο‰ β†’ (𝑧 ∈ 𝑛 β†’ (π·β€˜π‘§) ∈ π‘₯))))
72 bi2.04 388 . . . . . . . . . . . 12 ((𝑧 ∈ Ο‰ β†’ (𝑧 ∈ 𝑛 β†’ (π·β€˜π‘§) ∈ π‘₯)) ↔ (𝑧 ∈ 𝑛 β†’ (𝑧 ∈ Ο‰ β†’ (π·β€˜π‘§) ∈ π‘₯)))
7371, 72bitrdi 286 . . . . . . . . . . 11 (𝑛 ∈ Ο‰ β†’ ((𝑧 ∈ Ο‰ β†’ (Β¬ (π·β€˜π‘§) ∈ π‘₯ β†’ 𝑛 βŠ† 𝑧)) ↔ (𝑧 ∈ 𝑛 β†’ (𝑧 ∈ Ο‰ β†’ (π·β€˜π‘§) ∈ π‘₯))))
74 elnn 7868 . . . . . . . . . . . . . 14 ((𝑧 ∈ 𝑛 ∧ 𝑛 ∈ Ο‰) β†’ 𝑧 ∈ Ο‰)
75 pm2.27 42 . . . . . . . . . . . . . 14 (𝑧 ∈ Ο‰ β†’ ((𝑧 ∈ Ο‰ β†’ (π·β€˜π‘§) ∈ π‘₯) β†’ (π·β€˜π‘§) ∈ π‘₯))
7674, 75syl 17 . . . . . . . . . . . . 13 ((𝑧 ∈ 𝑛 ∧ 𝑛 ∈ Ο‰) β†’ ((𝑧 ∈ Ο‰ β†’ (π·β€˜π‘§) ∈ π‘₯) β†’ (π·β€˜π‘§) ∈ π‘₯))
7776expcom 414 . . . . . . . . . . . 12 (𝑛 ∈ Ο‰ β†’ (𝑧 ∈ 𝑛 β†’ ((𝑧 ∈ Ο‰ β†’ (π·β€˜π‘§) ∈ π‘₯) β†’ (π·β€˜π‘§) ∈ π‘₯)))
7877a2d 29 . . . . . . . . . . 11 (𝑛 ∈ Ο‰ β†’ ((𝑧 ∈ 𝑛 β†’ (𝑧 ∈ Ο‰ β†’ (π·β€˜π‘§) ∈ π‘₯)) β†’ (𝑧 ∈ 𝑛 β†’ (π·β€˜π‘§) ∈ π‘₯)))
7973, 78sylbid 239 . . . . . . . . . 10 (𝑛 ∈ Ο‰ β†’ ((𝑧 ∈ Ο‰ β†’ (Β¬ (π·β€˜π‘§) ∈ π‘₯ β†’ 𝑛 βŠ† 𝑧)) β†’ (𝑧 ∈ 𝑛 β†’ (π·β€˜π‘§) ∈ π‘₯)))
8079ad2antrl 726 . . . . . . . . 9 (((πœ‘ ∧ πœ“) ∧ (𝑛 ∈ Ο‰ ∧ 𝐷 ∈ (𝐴 ↑m 𝑛))) β†’ ((𝑧 ∈ Ο‰ β†’ (Β¬ (π·β€˜π‘§) ∈ π‘₯ β†’ 𝑛 βŠ† 𝑧)) β†’ (𝑧 ∈ 𝑛 β†’ (π·β€˜π‘§) ∈ π‘₯)))
8180ralimdv2 3163 . . . . . . . 8 (((πœ‘ ∧ πœ“) ∧ (𝑛 ∈ Ο‰ ∧ 𝐷 ∈ (𝐴 ↑m 𝑛))) β†’ (βˆ€π‘§ ∈ Ο‰ (Β¬ (π·β€˜π‘§) ∈ π‘₯ β†’ 𝑛 βŠ† 𝑧) β†’ βˆ€π‘§ ∈ 𝑛 (π·β€˜π‘§) ∈ π‘₯))
8264, 81biimtrid 241 . . . . . . 7 (((πœ‘ ∧ πœ“) ∧ (𝑛 ∈ Ο‰ ∧ 𝐷 ∈ (𝐴 ↑m 𝑛))) β†’ (𝑛 βŠ† ∩ {𝑧 ∈ Ο‰ ∣ Β¬ (π·β€˜π‘§) ∈ π‘₯} β†’ βˆ€π‘§ ∈ 𝑛 (π·β€˜π‘§) ∈ π‘₯))
8363, 82sylbird 259 . . . . . 6 (((πœ‘ ∧ πœ“) ∧ (𝑛 ∈ Ο‰ ∧ 𝐷 ∈ (𝐴 ↑m 𝑛))) β†’ (Β¬ ∩ {𝑧 ∈ Ο‰ ∣ Β¬ (π·β€˜π‘§) ∈ π‘₯} ∈ 𝑛 β†’ βˆ€π‘§ ∈ 𝑛 (π·β€˜π‘§) ∈ π‘₯))
8443, 83mt3d 148 . . . . 5 (((πœ‘ ∧ πœ“) ∧ (𝑛 ∈ Ο‰ ∧ 𝐷 ∈ (𝐴 ↑m 𝑛))) β†’ ∩ {𝑧 ∈ Ο‰ ∣ Β¬ (π·β€˜π‘§) ∈ π‘₯} ∈ 𝑛)
8530, 84ffvelcdmd 7087 . . . 4 (((πœ‘ ∧ πœ“) ∧ (𝑛 ∈ Ο‰ ∧ 𝐷 ∈ (𝐴 ↑m 𝑛))) β†’ (π·β€˜βˆ© {𝑧 ∈ Ο‰ ∣ Β¬ (π·β€˜π‘§) ∈ π‘₯}) ∈ 𝐴)
86 fveq2 6891 . . . . . . . . 9 (𝑦 = ∩ {𝑧 ∈ Ο‰ ∣ Β¬ (π·β€˜π‘§) ∈ π‘₯} β†’ (π·β€˜π‘¦) = (π·β€˜βˆ© {𝑧 ∈ Ο‰ ∣ Β¬ (π·β€˜π‘§) ∈ π‘₯}))
8786eleq1d 2818 . . . . . . . 8 (𝑦 = ∩ {𝑧 ∈ Ο‰ ∣ Β¬ (π·β€˜π‘§) ∈ π‘₯} β†’ ((π·β€˜π‘¦) ∈ π‘₯ ↔ (π·β€˜βˆ© {𝑧 ∈ Ο‰ ∣ Β¬ (π·β€˜π‘§) ∈ π‘₯}) ∈ π‘₯))
8887notbid 317 . . . . . . 7 (𝑦 = ∩ {𝑧 ∈ Ο‰ ∣ Β¬ (π·β€˜π‘§) ∈ π‘₯} β†’ (Β¬ (π·β€˜π‘¦) ∈ π‘₯ ↔ Β¬ (π·β€˜βˆ© {𝑧 ∈ Ο‰ ∣ Β¬ (π·β€˜π‘§) ∈ π‘₯}) ∈ π‘₯))
89 fveq2 6891 . . . . . . . . . 10 (𝑧 = 𝑦 β†’ (π·β€˜π‘§) = (π·β€˜π‘¦))
9089eleq1d 2818 . . . . . . . . 9 (𝑧 = 𝑦 β†’ ((π·β€˜π‘§) ∈ π‘₯ ↔ (π·β€˜π‘¦) ∈ π‘₯))
9190notbid 317 . . . . . . . 8 (𝑧 = 𝑦 β†’ (Β¬ (π·β€˜π‘§) ∈ π‘₯ ↔ Β¬ (π·β€˜π‘¦) ∈ π‘₯))
9291cbvrabv 3442 . . . . . . 7 {𝑧 ∈ Ο‰ ∣ Β¬ (π·β€˜π‘§) ∈ π‘₯} = {𝑦 ∈ Ο‰ ∣ Β¬ (π·β€˜π‘¦) ∈ π‘₯}
9388, 92elrab2 3686 . . . . . 6 (∩ {𝑧 ∈ Ο‰ ∣ Β¬ (π·β€˜π‘§) ∈ π‘₯} ∈ {𝑧 ∈ Ο‰ ∣ Β¬ (π·β€˜π‘§) ∈ π‘₯} ↔ (∩ {𝑧 ∈ Ο‰ ∣ Β¬ (π·β€˜π‘§) ∈ π‘₯} ∈ Ο‰ ∧ Β¬ (π·β€˜βˆ© {𝑧 ∈ Ο‰ ∣ Β¬ (π·β€˜π‘§) ∈ π‘₯}) ∈ π‘₯))
9493simprbi 497 . . . . 5 (∩ {𝑧 ∈ Ο‰ ∣ Β¬ (π·β€˜π‘§) ∈ π‘₯} ∈ {𝑧 ∈ Ο‰ ∣ Β¬ (π·β€˜π‘§) ∈ π‘₯} β†’ Β¬ (π·β€˜βˆ© {𝑧 ∈ Ο‰ ∣ Β¬ (π·β€˜π‘§) ∈ π‘₯}) ∈ π‘₯)
9560, 94syl 17 . . . 4 (((πœ‘ ∧ πœ“) ∧ (𝑛 ∈ Ο‰ ∧ 𝐷 ∈ (𝐴 ↑m 𝑛))) β†’ Β¬ (π·β€˜βˆ© {𝑧 ∈ Ο‰ ∣ Β¬ (π·β€˜π‘§) ∈ π‘₯}) ∈ π‘₯)
9685, 95eldifd 3959 . . 3 (((πœ‘ ∧ πœ“) ∧ (𝑛 ∈ Ο‰ ∧ 𝐷 ∈ (𝐴 ↑m 𝑛))) β†’ (π·β€˜βˆ© {𝑧 ∈ Ο‰ ∣ Β¬ (π·β€˜π‘§) ∈ π‘₯}) ∈ (𝐴 βˆ– π‘₯))
9728, 96rexlimddv 3161 . 2 ((πœ‘ ∧ πœ“) β†’ (π·β€˜βˆ© {𝑧 ∈ Ο‰ ∣ Β¬ (π·β€˜π‘§) ∈ π‘₯}) ∈ (𝐴 βˆ– π‘₯))
9817, 97eqeltrd 2833 1 ((πœ‘ ∧ πœ“) β†’ (π‘₯πΉπ‘Ÿ) ∈ (𝐴 βˆ– π‘₯))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106   β‰  wne 2940  βˆ€wral 3061  βˆƒwrex 3070  {crab 3432  Vcvv 3474   βˆ– cdif 3945   βŠ† wss 3948  βˆ…c0 4322  ifcif 4528  π’« cpw 4602  βˆ© cint 4950  βˆͺ ciun 4997   class class class wbr 5148   We wwe 5630   Γ— cxp 5674  β—‘ccnv 5675  ran crn 5677  Ord word 6363  Oncon0 6364   Fn wfn 6538  βŸΆwf 6539  β€“1-1β†’wf1 6540  β€“1-1-ontoβ†’wf1o 6542  β€˜cfv 6543  (class class class)co 7411   ∈ cmpo 7413  Ο‰com 7857   ↑m cmap 8822   β‰Ό cdom 8939   β‰Ί csdm 8940  Fincfn 8941  cardccrd 9932
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 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727  ax-inf2 9638
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  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-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-1st 7977  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-er 8705  df-map 8824  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945
This theorem is referenced by:  pwfseqlem4a  10658  pwfseqlem4  10659
  Copyright terms: Public domain W3C validator