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

Theorem ptcld 21226
 Description: A closed box in the product topology. (Contributed by Stefan O'Rear, 22-Feb-2015.)
Hypotheses
Ref Expression
ptcld.a (𝜑𝐴𝑉)
ptcld.f (𝜑𝐹:𝐴⟶Top)
ptcld.c ((𝜑𝑘𝐴) → 𝐶 ∈ (Clsd‘(𝐹𝑘)))
Assertion
Ref Expression
ptcld (𝜑X𝑘𝐴 𝐶 ∈ (Clsd‘(∏t𝐹)))
Distinct variable groups:   𝜑,𝑘   𝐴,𝑘   𝑘,𝐹   𝑘,𝑉
Allowed substitution hint:   𝐶(𝑘)

Proof of Theorem ptcld
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 ptcld.c . . . . 5 ((𝜑𝑘𝐴) → 𝐶 ∈ (Clsd‘(𝐹𝑘)))
2 eqid 2610 . . . . . 6 (𝐹𝑘) = (𝐹𝑘)
32cldss 20643 . . . . 5 (𝐶 ∈ (Clsd‘(𝐹𝑘)) → 𝐶 (𝐹𝑘))
41, 3syl 17 . . . 4 ((𝜑𝑘𝐴) → 𝐶 (𝐹𝑘))
54ralrimiva 2949 . . 3 (𝜑 → ∀𝑘𝐴 𝐶 (𝐹𝑘))
6 boxriin 7836 . . 3 (∀𝑘𝐴 𝐶 (𝐹𝑘) → X𝑘𝐴 𝐶 = (X𝑘𝐴 (𝐹𝑘) ∩ 𝑥𝐴 X𝑘𝐴 if(𝑘 = 𝑥, 𝐶, (𝐹𝑘))))
75, 6syl 17 . 2 (𝜑X𝑘𝐴 𝐶 = (X𝑘𝐴 (𝐹𝑘) ∩ 𝑥𝐴 X𝑘𝐴 if(𝑘 = 𝑥, 𝐶, (𝐹𝑘))))
8 ptcld.a . . . . 5 (𝜑𝐴𝑉)
9 ptcld.f . . . . 5 (𝜑𝐹:𝐴⟶Top)
10 eqid 2610 . . . . . 6 (∏t𝐹) = (∏t𝐹)
1110ptuni 21207 . . . . 5 ((𝐴𝑉𝐹:𝐴⟶Top) → X𝑘𝐴 (𝐹𝑘) = (∏t𝐹))
128, 9, 11syl2anc 691 . . . 4 (𝜑X𝑘𝐴 (𝐹𝑘) = (∏t𝐹))
1312ineq1d 3775 . . 3 (𝜑 → (X𝑘𝐴 (𝐹𝑘) ∩ 𝑥𝐴 X𝑘𝐴 if(𝑘 = 𝑥, 𝐶, (𝐹𝑘))) = ( (∏t𝐹) ∩ 𝑥𝐴 X𝑘𝐴 if(𝑘 = 𝑥, 𝐶, (𝐹𝑘))))
14 pttop 21195 . . . . 5 ((𝐴𝑉𝐹:𝐴⟶Top) → (∏t𝐹) ∈ Top)
158, 9, 14syl2anc 691 . . . 4 (𝜑 → (∏t𝐹) ∈ Top)
16 sseq1 3589 . . . . . . . . . . 11 (𝐶 = if(𝑘 = 𝑥, 𝐶, (𝐹𝑘)) → (𝐶 (𝐹𝑘) ↔ if(𝑘 = 𝑥, 𝐶, (𝐹𝑘)) ⊆ (𝐹𝑘)))
17 sseq1 3589 . . . . . . . . . . 11 ( (𝐹𝑘) = if(𝑘 = 𝑥, 𝐶, (𝐹𝑘)) → ( (𝐹𝑘) ⊆ (𝐹𝑘) ↔ if(𝑘 = 𝑥, 𝐶, (𝐹𝑘)) ⊆ (𝐹𝑘)))
18 simpl 472 . . . . . . . . . . 11 ((𝐶 (𝐹𝑘) ∧ 𝑘 = 𝑥) → 𝐶 (𝐹𝑘))
19 ssid 3587 . . . . . . . . . . . 12 (𝐹𝑘) ⊆ (𝐹𝑘)
2019a1i 11 . . . . . . . . . . 11 ((𝐶 (𝐹𝑘) ∧ ¬ 𝑘 = 𝑥) → (𝐹𝑘) ⊆ (𝐹𝑘))
2116, 17, 18, 20ifbothda 4073 . . . . . . . . . 10 (𝐶 (𝐹𝑘) → if(𝑘 = 𝑥, 𝐶, (𝐹𝑘)) ⊆ (𝐹𝑘))
2221ralimi 2936 . . . . . . . . 9 (∀𝑘𝐴 𝐶 (𝐹𝑘) → ∀𝑘𝐴 if(𝑘 = 𝑥, 𝐶, (𝐹𝑘)) ⊆ (𝐹𝑘))
23 ss2ixp 7807 . . . . . . . . 9 (∀𝑘𝐴 if(𝑘 = 𝑥, 𝐶, (𝐹𝑘)) ⊆ (𝐹𝑘) → X𝑘𝐴 if(𝑘 = 𝑥, 𝐶, (𝐹𝑘)) ⊆ X𝑘𝐴 (𝐹𝑘))
245, 22, 233syl 18 . . . . . . . 8 (𝜑X𝑘𝐴 if(𝑘 = 𝑥, 𝐶, (𝐹𝑘)) ⊆ X𝑘𝐴 (𝐹𝑘))
2524adantr 480 . . . . . . 7 ((𝜑𝑥𝐴) → X𝑘𝐴 if(𝑘 = 𝑥, 𝐶, (𝐹𝑘)) ⊆ X𝑘𝐴 (𝐹𝑘))
2612adantr 480 . . . . . . 7 ((𝜑𝑥𝐴) → X𝑘𝐴 (𝐹𝑘) = (∏t𝐹))
2725, 26sseqtrd 3604 . . . . . 6 ((𝜑𝑥𝐴) → X𝑘𝐴 if(𝑘 = 𝑥, 𝐶, (𝐹𝑘)) ⊆ (∏t𝐹))
2812eqcomd 2616 . . . . . . . . . 10 (𝜑 (∏t𝐹) = X𝑘𝐴 (𝐹𝑘))
2928difeq1d 3689 . . . . . . . . 9 (𝜑 → ( (∏t𝐹) ∖ X𝑘𝐴 if(𝑘 = 𝑥, 𝐶, (𝐹𝑘))) = (X𝑘𝐴 (𝐹𝑘) ∖ X𝑘𝐴 if(𝑘 = 𝑥, 𝐶, (𝐹𝑘))))
3029adantr 480 . . . . . . . 8 ((𝜑𝑥𝐴) → ( (∏t𝐹) ∖ X𝑘𝐴 if(𝑘 = 𝑥, 𝐶, (𝐹𝑘))) = (X𝑘𝐴 (𝐹𝑘) ∖ X𝑘𝐴 if(𝑘 = 𝑥, 𝐶, (𝐹𝑘))))
31 simpr 476 . . . . . . . . 9 ((𝜑𝑥𝐴) → 𝑥𝐴)
325adantr 480 . . . . . . . . 9 ((𝜑𝑥𝐴) → ∀𝑘𝐴 𝐶 (𝐹𝑘))
33 boxcutc 7837 . . . . . . . . 9 ((𝑥𝐴 ∧ ∀𝑘𝐴 𝐶 (𝐹𝑘)) → (X𝑘𝐴 (𝐹𝑘) ∖ X𝑘𝐴 if(𝑘 = 𝑥, 𝐶, (𝐹𝑘))) = X𝑘𝐴 if(𝑘 = 𝑥, ( (𝐹𝑘) ∖ 𝐶), (𝐹𝑘)))
3431, 32, 33syl2anc 691 . . . . . . . 8 ((𝜑𝑥𝐴) → (X𝑘𝐴 (𝐹𝑘) ∖ X𝑘𝐴 if(𝑘 = 𝑥, 𝐶, (𝐹𝑘))) = X𝑘𝐴 if(𝑘 = 𝑥, ( (𝐹𝑘) ∖ 𝐶), (𝐹𝑘)))
35 ixpeq2 7808 . . . . . . . . . 10 (∀𝑘𝐴 if(𝑘 = 𝑥, ( (𝐹𝑘) ∖ 𝐶), (𝐹𝑘)) = if(𝑘 = 𝑥, ( (𝐹𝑥) ∖ 𝑥 / 𝑘𝐶), (𝐹𝑘)) → X𝑘𝐴 if(𝑘 = 𝑥, ( (𝐹𝑘) ∖ 𝐶), (𝐹𝑘)) = X𝑘𝐴 if(𝑘 = 𝑥, ( (𝐹𝑥) ∖ 𝑥 / 𝑘𝐶), (𝐹𝑘)))
36 fveq2 6103 . . . . . . . . . . . . . 14 (𝑘 = 𝑥 → (𝐹𝑘) = (𝐹𝑥))
3736unieqd 4382 . . . . . . . . . . . . 13 (𝑘 = 𝑥 (𝐹𝑘) = (𝐹𝑥))
38 csbeq1a 3508 . . . . . . . . . . . . 13 (𝑘 = 𝑥𝐶 = 𝑥 / 𝑘𝐶)
3937, 38difeq12d 3691 . . . . . . . . . . . 12 (𝑘 = 𝑥 → ( (𝐹𝑘) ∖ 𝐶) = ( (𝐹𝑥) ∖ 𝑥 / 𝑘𝐶))
4039adantl 481 . . . . . . . . . . 11 ((𝑘𝐴𝑘 = 𝑥) → ( (𝐹𝑘) ∖ 𝐶) = ( (𝐹𝑥) ∖ 𝑥 / 𝑘𝐶))
4140ifeq1da 4066 . . . . . . . . . 10 (𝑘𝐴 → if(𝑘 = 𝑥, ( (𝐹𝑘) ∖ 𝐶), (𝐹𝑘)) = if(𝑘 = 𝑥, ( (𝐹𝑥) ∖ 𝑥 / 𝑘𝐶), (𝐹𝑘)))
4235, 41mprg 2910 . . . . . . . . 9 X𝑘𝐴 if(𝑘 = 𝑥, ( (𝐹𝑘) ∖ 𝐶), (𝐹𝑘)) = X𝑘𝐴 if(𝑘 = 𝑥, ( (𝐹𝑥) ∖ 𝑥 / 𝑘𝐶), (𝐹𝑘))
4342a1i 11 . . . . . . . 8 ((𝜑𝑥𝐴) → X𝑘𝐴 if(𝑘 = 𝑥, ( (𝐹𝑘) ∖ 𝐶), (𝐹𝑘)) = X𝑘𝐴 if(𝑘 = 𝑥, ( (𝐹𝑥) ∖ 𝑥 / 𝑘𝐶), (𝐹𝑘)))
4430, 34, 433eqtrd 2648 . . . . . . 7 ((𝜑𝑥𝐴) → ( (∏t𝐹) ∖ X𝑘𝐴 if(𝑘 = 𝑥, 𝐶, (𝐹𝑘))) = X𝑘𝐴 if(𝑘 = 𝑥, ( (𝐹𝑥) ∖ 𝑥 / 𝑘𝐶), (𝐹𝑘)))
458adantr 480 . . . . . . . 8 ((𝜑𝑥𝐴) → 𝐴𝑉)
469adantr 480 . . . . . . . 8 ((𝜑𝑥𝐴) → 𝐹:𝐴⟶Top)
471ralrimiva 2949 . . . . . . . . . . 11 (𝜑 → ∀𝑘𝐴 𝐶 ∈ (Clsd‘(𝐹𝑘)))
48 nfv 1830 . . . . . . . . . . . 12 𝑥 𝐶 ∈ (Clsd‘(𝐹𝑘))
49 nfcsb1v 3515 . . . . . . . . . . . . 13 𝑘𝑥 / 𝑘𝐶
5049nfel1 2765 . . . . . . . . . . . 12 𝑘𝑥 / 𝑘𝐶 ∈ (Clsd‘(𝐹𝑥))
5136fveq2d 6107 . . . . . . . . . . . . 13 (𝑘 = 𝑥 → (Clsd‘(𝐹𝑘)) = (Clsd‘(𝐹𝑥)))
5238, 51eleq12d 2682 . . . . . . . . . . . 12 (𝑘 = 𝑥 → (𝐶 ∈ (Clsd‘(𝐹𝑘)) ↔ 𝑥 / 𝑘𝐶 ∈ (Clsd‘(𝐹𝑥))))
5348, 50, 52cbvral 3143 . . . . . . . . . . 11 (∀𝑘𝐴 𝐶 ∈ (Clsd‘(𝐹𝑘)) ↔ ∀𝑥𝐴 𝑥 / 𝑘𝐶 ∈ (Clsd‘(𝐹𝑥)))
5447, 53sylib 207 . . . . . . . . . 10 (𝜑 → ∀𝑥𝐴 𝑥 / 𝑘𝐶 ∈ (Clsd‘(𝐹𝑥)))
5554r19.21bi 2916 . . . . . . . . 9 ((𝜑𝑥𝐴) → 𝑥 / 𝑘𝐶 ∈ (Clsd‘(𝐹𝑥)))
56 eqid 2610 . . . . . . . . . 10 (𝐹𝑥) = (𝐹𝑥)
5756cldopn 20645 . . . . . . . . 9 (𝑥 / 𝑘𝐶 ∈ (Clsd‘(𝐹𝑥)) → ( (𝐹𝑥) ∖ 𝑥 / 𝑘𝐶) ∈ (𝐹𝑥))
5855, 57syl 17 . . . . . . . 8 ((𝜑𝑥𝐴) → ( (𝐹𝑥) ∖ 𝑥 / 𝑘𝐶) ∈ (𝐹𝑥))
5945, 46, 58ptopn2 21197 . . . . . . 7 ((𝜑𝑥𝐴) → X𝑘𝐴 if(𝑘 = 𝑥, ( (𝐹𝑥) ∖ 𝑥 / 𝑘𝐶), (𝐹𝑘)) ∈ (∏t𝐹))
6044, 59eqeltrd 2688 . . . . . 6 ((𝜑𝑥𝐴) → ( (∏t𝐹) ∖ X𝑘𝐴 if(𝑘 = 𝑥, 𝐶, (𝐹𝑘))) ∈ (∏t𝐹))
61 eqid 2610 . . . . . . . . 9 (∏t𝐹) = (∏t𝐹)
6261iscld 20641 . . . . . . . 8 ((∏t𝐹) ∈ Top → (X𝑘𝐴 if(𝑘 = 𝑥, 𝐶, (𝐹𝑘)) ∈ (Clsd‘(∏t𝐹)) ↔ (X𝑘𝐴 if(𝑘 = 𝑥, 𝐶, (𝐹𝑘)) ⊆ (∏t𝐹) ∧ ( (∏t𝐹) ∖ X𝑘𝐴 if(𝑘 = 𝑥, 𝐶, (𝐹𝑘))) ∈ (∏t𝐹))))
6315, 62syl 17 . . . . . . 7 (𝜑 → (X𝑘𝐴 if(𝑘 = 𝑥, 𝐶, (𝐹𝑘)) ∈ (Clsd‘(∏t𝐹)) ↔ (X𝑘𝐴 if(𝑘 = 𝑥, 𝐶, (𝐹𝑘)) ⊆ (∏t𝐹) ∧ ( (∏t𝐹) ∖ X𝑘𝐴 if(𝑘 = 𝑥, 𝐶, (𝐹𝑘))) ∈ (∏t𝐹))))
6463adantr 480 . . . . . 6 ((𝜑𝑥𝐴) → (X𝑘𝐴 if(𝑘 = 𝑥, 𝐶, (𝐹𝑘)) ∈ (Clsd‘(∏t𝐹)) ↔ (X𝑘𝐴 if(𝑘 = 𝑥, 𝐶, (𝐹𝑘)) ⊆ (∏t𝐹) ∧ ( (∏t𝐹) ∖ X𝑘𝐴 if(𝑘 = 𝑥, 𝐶, (𝐹𝑘))) ∈ (∏t𝐹))))
6527, 60, 64mpbir2and 959 . . . . 5 ((𝜑𝑥𝐴) → X𝑘𝐴 if(𝑘 = 𝑥, 𝐶, (𝐹𝑘)) ∈ (Clsd‘(∏t𝐹)))
6665ralrimiva 2949 . . . 4 (𝜑 → ∀𝑥𝐴 X𝑘𝐴 if(𝑘 = 𝑥, 𝐶, (𝐹𝑘)) ∈ (Clsd‘(∏t𝐹)))
6761riincld 20658 . . . 4 (((∏t𝐹) ∈ Top ∧ ∀𝑥𝐴 X𝑘𝐴 if(𝑘 = 𝑥, 𝐶, (𝐹𝑘)) ∈ (Clsd‘(∏t𝐹))) → ( (∏t𝐹) ∩ 𝑥𝐴 X𝑘𝐴 if(𝑘 = 𝑥, 𝐶, (𝐹𝑘))) ∈ (Clsd‘(∏t𝐹)))
6815, 66, 67syl2anc 691 . . 3 (𝜑 → ( (∏t𝐹) ∩ 𝑥𝐴 X𝑘𝐴 if(𝑘 = 𝑥, 𝐶, (𝐹𝑘))) ∈ (Clsd‘(∏t𝐹)))
6913, 68eqeltrd 2688 . 2 (𝜑 → (X𝑘𝐴 (𝐹𝑘) ∩ 𝑥𝐴 X𝑘𝐴 if(𝑘 = 𝑥, 𝐶, (𝐹𝑘))) ∈ (Clsd‘(∏t𝐹)))
707, 69eqeltrd 2688 1 (𝜑X𝑘𝐴 𝐶 ∈ (Clsd‘(∏t𝐹)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977  ∀wral 2896  ⦋csb 3499   ∖ cdif 3537   ∩ cin 3539   ⊆ wss 3540  ifcif 4036  ∪ cuni 4372  ∩ ciin 4456  ⟶wf 5800  ‘cfv 5804  Xcixp 7794  ∏tcpt 15922  Topctop 20517  Clsdccld 20630 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-iin 4458  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-ixp 7795  df-en 7842  df-fin 7845  df-fi 8200  df-topgen 15927  df-pt 15928  df-top 20521  df-bases 20522  df-cld 20633 This theorem is referenced by:  ptcldmpt  21227
 Copyright terms: Public domain W3C validator