MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dfac14lem Structured version   Visualization version   GIF version
Theorem dfac14lem 23113
Description: Lemma for dfac14 23114. By equipping 𝑆 βˆͺ {𝑃} for some 𝑃 βˆ‰ 𝑆 with the particular point topology, we can show that 𝑃 is in the closure of 𝑆; hence the sequence 𝑃(π‘₯) is in the product of the closures, and we can utilize this instance of ptcls 23112 to extract an element of the closure of Xπ‘˜ ∈ 𝐼𝑆. (Contributed by Mario Carneiro, 2-Sep-2015.)
Hypotheses
Ref Expression
dfac14lem.i (πœ‘ β†’ 𝐼 ∈ 𝑉)
dfac14lem.s ((πœ‘ ∧ π‘₯ ∈ 𝐼) β†’ 𝑆 ∈ π‘Š)
dfac14lem.0 ((πœ‘ ∧ π‘₯ ∈ 𝐼) β†’ 𝑆 β‰  βˆ…)
dfac14lem.p 𝑃 = 𝒫 βˆͺ 𝑆
dfac14lem.r 𝑅 = {𝑦 ∈ 𝒫 (𝑆 βˆͺ {𝑃}) ∣ (𝑃 ∈ 𝑦 β†’ 𝑦 = (𝑆 βˆͺ {𝑃}))}
dfac14lem.j 𝐽 = (∏tβ€˜(π‘₯ ∈ 𝐼 ↦ 𝑅))
dfac14lem.c (πœ‘ β†’ ((clsβ€˜π½)β€˜Xπ‘₯ ∈ 𝐼 𝑆) = Xπ‘₯ ∈ 𝐼 ((clsβ€˜π‘…)β€˜π‘†))
Assertion
Ref Expression
dfac14lem (πœ‘ β†’ Xπ‘₯ ∈ 𝐼 𝑆 β‰  βˆ…)
Distinct variable groups:   π‘₯,𝐼   𝑦,𝑃   πœ‘,π‘₯   𝑦,𝑆
Allowed substitution hints:   πœ‘(𝑦)   𝑃(π‘₯)   𝑅(π‘₯,𝑦)   𝑆(π‘₯)   𝐼(𝑦)   𝐽(π‘₯,𝑦)   𝑉(π‘₯,𝑦)   π‘Š(π‘₯,𝑦)
Proof of Theorem dfac14lem
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 eleq2w 2818 . . . . . . . . . . 11 (𝑦 = 𝑧 β†’ (𝑃 ∈ 𝑦 ↔ 𝑃 ∈ 𝑧))
2 eqeq1 2737 . . . . . . . . . . 11 (𝑦 = 𝑧 β†’ (𝑦 = (𝑆 βˆͺ {𝑃}) ↔ 𝑧 = (𝑆 βˆͺ {𝑃})))
31, 2imbi12d 345 . . . . . . . . . 10 (𝑦 = 𝑧 β†’ ((𝑃 ∈ 𝑦 β†’ 𝑦 = (𝑆 βˆͺ {𝑃})) ↔ (𝑃 ∈ 𝑧 β†’ 𝑧 = (𝑆 βˆͺ {𝑃}))))
4 dfac14lem.r . . . . . . . . . 10 𝑅 = {𝑦 ∈ 𝒫 (𝑆 βˆͺ {𝑃}) ∣ (𝑃 ∈ 𝑦 β†’ 𝑦 = (𝑆 βˆͺ {𝑃}))}
53, 4elrab2 3686 . . . . . . . . 9 (𝑧 ∈ 𝑅 ↔ (𝑧 ∈ 𝒫 (𝑆 βˆͺ {𝑃}) ∧ (𝑃 ∈ 𝑧 β†’ 𝑧 = (𝑆 βˆͺ {𝑃}))))
6 dfac14lem.0 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘₯ ∈ 𝐼) β†’ 𝑆 β‰  βˆ…)
76adantr 482 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘₯ ∈ 𝐼) ∧ 𝑧 ∈ 𝒫 (𝑆 βˆͺ {𝑃})) β†’ 𝑆 β‰  βˆ…)
8 ineq1 4205 . . . . . . . . . . . . . 14 (𝑧 = (𝑆 βˆͺ {𝑃}) β†’ (𝑧 ∩ 𝑆) = ((𝑆 βˆͺ {𝑃}) ∩ 𝑆))
9 ssun1 4172 . . . . . . . . . . . . . . 15 𝑆 βŠ† (𝑆 βˆͺ {𝑃})
10 sseqin2 4215 . . . . . . . . . . . . . . 15 (𝑆 βŠ† (𝑆 βˆͺ {𝑃}) ↔ ((𝑆 βˆͺ {𝑃}) ∩ 𝑆) = 𝑆)
119, 10mpbi 229 . . . . . . . . . . . . . 14 ((𝑆 βˆͺ {𝑃}) ∩ 𝑆) = 𝑆
128, 11eqtrdi 2789 . . . . . . . . . . . . 13 (𝑧 = (𝑆 βˆͺ {𝑃}) β†’ (𝑧 ∩ 𝑆) = 𝑆)
1312neeq1d 3001 . . . . . . . . . . . 12 (𝑧 = (𝑆 βˆͺ {𝑃}) β†’ ((𝑧 ∩ 𝑆) β‰  βˆ… ↔ 𝑆 β‰  βˆ…))
147, 13syl5ibrcom 246 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ 𝐼) ∧ 𝑧 ∈ 𝒫 (𝑆 βˆͺ {𝑃})) β†’ (𝑧 = (𝑆 βˆͺ {𝑃}) β†’ (𝑧 ∩ 𝑆) β‰  βˆ…))
1514imim2d 57 . . . . . . . . . 10 (((πœ‘ ∧ π‘₯ ∈ 𝐼) ∧ 𝑧 ∈ 𝒫 (𝑆 βˆͺ {𝑃})) β†’ ((𝑃 ∈ 𝑧 β†’ 𝑧 = (𝑆 βˆͺ {𝑃})) β†’ (𝑃 ∈ 𝑧 β†’ (𝑧 ∩ 𝑆) β‰  βˆ…)))
1615expimpd 455 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ 𝐼) β†’ ((𝑧 ∈ 𝒫 (𝑆 βˆͺ {𝑃}) ∧ (𝑃 ∈ 𝑧 β†’ 𝑧 = (𝑆 βˆͺ {𝑃}))) β†’ (𝑃 ∈ 𝑧 β†’ (𝑧 ∩ 𝑆) β‰  βˆ…)))
175, 16biimtrid 241 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ 𝐼) β†’ (𝑧 ∈ 𝑅 β†’ (𝑃 ∈ 𝑧 β†’ (𝑧 ∩ 𝑆) β‰  βˆ…)))
1817ralrimiv 3146 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ 𝐼) β†’ βˆ€π‘§ ∈ 𝑅 (𝑃 ∈ 𝑧 β†’ (𝑧 ∩ 𝑆) β‰  βˆ…))
19 dfac14lem.s . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ 𝐼) β†’ 𝑆 ∈ π‘Š)
20 snex 5431 . . . . . . . . . . . 12 {𝑃} ∈ V
21 unexg 7733 . . . . . . . . . . . 12 ((𝑆 ∈ π‘Š ∧ {𝑃} ∈ V) β†’ (𝑆 βˆͺ {𝑃}) ∈ V)
2219, 20, 21sylancl 587 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ 𝐼) β†’ (𝑆 βˆͺ {𝑃}) ∈ V)
23 ssun2 4173 . . . . . . . . . . . 12 {𝑃} βŠ† (𝑆 βˆͺ {𝑃})
24 dfac14lem.p . . . . . . . . . . . . . 14 𝑃 = 𝒫 βˆͺ 𝑆
25 uniexg 7727 . . . . . . . . . . . . . . 15 (𝑆 ∈ π‘Š β†’ βˆͺ 𝑆 ∈ V)
26 pwexg 5376 . . . . . . . . . . . . . . 15 (βˆͺ 𝑆 ∈ V β†’ 𝒫 βˆͺ 𝑆 ∈ V)
2719, 25, 263syl 18 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘₯ ∈ 𝐼) β†’ 𝒫 βˆͺ 𝑆 ∈ V)
2824, 27eqeltrid 2838 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘₯ ∈ 𝐼) β†’ 𝑃 ∈ V)
29 snidg 4662 . . . . . . . . . . . . 13 (𝑃 ∈ V β†’ 𝑃 ∈ {𝑃})
3028, 29syl 17 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ 𝐼) β†’ 𝑃 ∈ {𝑃})
3123, 30sselid 3980 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ 𝐼) β†’ 𝑃 ∈ (𝑆 βˆͺ {𝑃}))
32 epttop 22504 . . . . . . . . . . 11 (((𝑆 βˆͺ {𝑃}) ∈ V ∧ 𝑃 ∈ (𝑆 βˆͺ {𝑃})) β†’ {𝑦 ∈ 𝒫 (𝑆 βˆͺ {𝑃}) ∣ (𝑃 ∈ 𝑦 β†’ 𝑦 = (𝑆 βˆͺ {𝑃}))} ∈ (TopOnβ€˜(𝑆 βˆͺ {𝑃})))
3322, 31, 32syl2anc 585 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ 𝐼) β†’ {𝑦 ∈ 𝒫 (𝑆 βˆͺ {𝑃}) ∣ (𝑃 ∈ 𝑦 β†’ 𝑦 = (𝑆 βˆͺ {𝑃}))} ∈ (TopOnβ€˜(𝑆 βˆͺ {𝑃})))
344, 33eqeltrid 2838 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ 𝐼) β†’ 𝑅 ∈ (TopOnβ€˜(𝑆 βˆͺ {𝑃})))
35 topontop 22407 . . . . . . . . 9 (𝑅 ∈ (TopOnβ€˜(𝑆 βˆͺ {𝑃})) β†’ 𝑅 ∈ Top)
3634, 35syl 17 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ 𝐼) β†’ 𝑅 ∈ Top)
37 toponuni 22408 . . . . . . . . . 10 (𝑅 ∈ (TopOnβ€˜(𝑆 βˆͺ {𝑃})) β†’ (𝑆 βˆͺ {𝑃}) = βˆͺ 𝑅)
3834, 37syl 17 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ 𝐼) β†’ (𝑆 βˆͺ {𝑃}) = βˆͺ 𝑅)
399, 38sseqtrid 4034 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ 𝐼) β†’ 𝑆 βŠ† βˆͺ 𝑅)
4031, 38eleqtrd 2836 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ 𝐼) β†’ 𝑃 ∈ βˆͺ 𝑅)
41 eqid 2733 . . . . . . . . 9 βˆͺ 𝑅 = βˆͺ 𝑅
4241elcls 22569 . . . . . . . 8 ((𝑅 ∈ Top ∧ 𝑆 βŠ† βˆͺ 𝑅 ∧ 𝑃 ∈ βˆͺ 𝑅) β†’ (𝑃 ∈ ((clsβ€˜π‘…)β€˜π‘†) ↔ βˆ€π‘§ ∈ 𝑅 (𝑃 ∈ 𝑧 β†’ (𝑧 ∩ 𝑆) β‰  βˆ…)))
4336, 39, 40, 42syl3anc 1372 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ 𝐼) β†’ (𝑃 ∈ ((clsβ€˜π‘…)β€˜π‘†) ↔ βˆ€π‘§ ∈ 𝑅 (𝑃 ∈ 𝑧 β†’ (𝑧 ∩ 𝑆) β‰  βˆ…)))
4418, 43mpbird 257 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ 𝐼) β†’ 𝑃 ∈ ((clsβ€˜π‘…)β€˜π‘†))
4544ralrimiva 3147 . . . . 5 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝐼 𝑃 ∈ ((clsβ€˜π‘…)β€˜π‘†))
46 dfac14lem.i . . . . . 6 (πœ‘ β†’ 𝐼 ∈ 𝑉)
47 mptelixpg 8926 . . . . . 6 (𝐼 ∈ 𝑉 β†’ ((π‘₯ ∈ 𝐼 ↦ 𝑃) ∈ Xπ‘₯ ∈ 𝐼 ((clsβ€˜π‘…)β€˜π‘†) ↔ βˆ€π‘₯ ∈ 𝐼 𝑃 ∈ ((clsβ€˜π‘…)β€˜π‘†)))
4846, 47syl 17 . . . . 5 (πœ‘ β†’ ((π‘₯ ∈ 𝐼 ↦ 𝑃) ∈ Xπ‘₯ ∈ 𝐼 ((clsβ€˜π‘…)β€˜π‘†) ↔ βˆ€π‘₯ ∈ 𝐼 𝑃 ∈ ((clsβ€˜π‘…)β€˜π‘†)))
4945, 48mpbird 257 . . . 4 (πœ‘ β†’ (π‘₯ ∈ 𝐼 ↦ 𝑃) ∈ Xπ‘₯ ∈ 𝐼 ((clsβ€˜π‘…)β€˜π‘†))
5049ne0d 4335 . . 3 (πœ‘ β†’ Xπ‘₯ ∈ 𝐼 ((clsβ€˜π‘…)β€˜π‘†) β‰  βˆ…)
51 dfac14lem.c . . 3 (πœ‘ β†’ ((clsβ€˜π½)β€˜Xπ‘₯ ∈ 𝐼 𝑆) = Xπ‘₯ ∈ 𝐼 ((clsβ€˜π‘…)β€˜π‘†))
5234ralrimiva 3147 . . . . 5 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝐼 𝑅 ∈ (TopOnβ€˜(𝑆 βˆͺ {𝑃})))
53 dfac14lem.j . . . . . 6 𝐽 = (∏tβ€˜(π‘₯ ∈ 𝐼 ↦ 𝑅))
5453pttopon 23092 . . . . 5 ((𝐼 ∈ 𝑉 ∧ βˆ€π‘₯ ∈ 𝐼 𝑅 ∈ (TopOnβ€˜(𝑆 βˆͺ {𝑃}))) β†’ 𝐽 ∈ (TopOnβ€˜Xπ‘₯ ∈ 𝐼 (𝑆 βˆͺ {𝑃})))
5546, 52, 54syl2anc 585 . . . 4 (πœ‘ β†’ 𝐽 ∈ (TopOnβ€˜Xπ‘₯ ∈ 𝐼 (𝑆 βˆͺ {𝑃})))
56 topontop 22407 . . . 4 (𝐽 ∈ (TopOnβ€˜Xπ‘₯ ∈ 𝐼 (𝑆 βˆͺ {𝑃})) β†’ 𝐽 ∈ Top)
57 cls0 22576 . . . 4 (𝐽 ∈ Top β†’ ((clsβ€˜π½)β€˜βˆ…) = βˆ…)
5855, 56, 573syl 18 . . 3 (πœ‘ β†’ ((clsβ€˜π½)β€˜βˆ…) = βˆ…)
5950, 51, 583netr4d 3019 . 2 (πœ‘ β†’ ((clsβ€˜π½)β€˜Xπ‘₯ ∈ 𝐼 𝑆) β‰  ((clsβ€˜π½)β€˜βˆ…))
60 fveq2 6889 . . 3 (Xπ‘₯ ∈ 𝐼 𝑆 = βˆ… β†’ ((clsβ€˜π½)β€˜Xπ‘₯ ∈ 𝐼 𝑆) = ((clsβ€˜π½)β€˜βˆ…))
6160necon3i 2974 . 2 (((clsβ€˜π½)β€˜Xπ‘₯ ∈ 𝐼 𝑆) β‰  ((clsβ€˜π½)β€˜βˆ…) β†’ Xπ‘₯ ∈ 𝐼 𝑆 β‰  βˆ…)
6259, 61syl 17 1 (πœ‘ β†’ Xπ‘₯ ∈ 𝐼 𝑆 β‰  βˆ…)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107   β‰  wne 2941  βˆ€wral 3062  {crab 3433  Vcvv 3475   βˆͺ cun 3946   ∩ cin 3947   βŠ† wss 3948  βˆ…c0 4322  π’« cpw 4602  {csn 4628  βˆͺ cuni 4908   ↦ cmpt 5231  β€˜cfv 6541  Xcixp 8888  βˆtcpt 17381  Topctop 22387  TopOnctopon 22404  clsccl 22514
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  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-iin 5000  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-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-om 7853  df-1o 8463  df-er 8700  df-ixp 8889  df-en 8937  df-fin 8940  df-fi 9403  df-topgen 17386  df-pt 17387  df-top 22388  df-topon 22405  df-bases 22441  df-cld 22515  df-ntr 22516  df-cls 22517
This theorem is referenced by:  dfac14  23114
  Copyright terms: Public domain W3C validator