![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ptopn2 | Structured version Visualization version GIF version |
Description: A sub-basic open set in the product topology. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
Ref | Expression |
---|---|
ptopn2.a | ⊢ (𝜑 → 𝐴 ∈ 𝑉) |
ptopn2.f | ⊢ (𝜑 → 𝐹:𝐴⟶Top) |
ptopn2.o | ⊢ (𝜑 → 𝑂 ∈ (𝐹‘𝑌)) |
Ref | Expression |
---|---|
ptopn2 | ⊢ (𝜑 → X𝑘 ∈ 𝐴 if(𝑘 = 𝑌, 𝑂, ∪ (𝐹‘𝑘)) ∈ (∏t‘𝐹)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ptopn2.a | . 2 ⊢ (𝜑 → 𝐴 ∈ 𝑉) | |
2 | ptopn2.f | . 2 ⊢ (𝜑 → 𝐹:𝐴⟶Top) | |
3 | snfi 8383 | . . 3 ⊢ {𝑌} ∈ Fin | |
4 | 3 | a1i 11 | . 2 ⊢ (𝜑 → {𝑌} ∈ Fin) |
5 | ptopn2.o | . . . . . 6 ⊢ (𝜑 → 𝑂 ∈ (𝐹‘𝑌)) | |
6 | 5 | adantr 473 | . . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑂 ∈ (𝐹‘𝑌)) |
7 | fveq2 6493 | . . . . . 6 ⊢ (𝑘 = 𝑌 → (𝐹‘𝑘) = (𝐹‘𝑌)) | |
8 | 7 | eleq2d 2845 | . . . . 5 ⊢ (𝑘 = 𝑌 → (𝑂 ∈ (𝐹‘𝑘) ↔ 𝑂 ∈ (𝐹‘𝑌))) |
9 | 6, 8 | syl5ibrcom 239 | . . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑘 = 𝑌 → 𝑂 ∈ (𝐹‘𝑘))) |
10 | 9 | imp 398 | . . 3 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑘 = 𝑌) → 𝑂 ∈ (𝐹‘𝑘)) |
11 | 2 | ffvelrnda 6670 | . . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ Top) |
12 | eqid 2772 | . . . . . 6 ⊢ ∪ (𝐹‘𝑘) = ∪ (𝐹‘𝑘) | |
13 | 12 | topopn 21208 | . . . . 5 ⊢ ((𝐹‘𝑘) ∈ Top → ∪ (𝐹‘𝑘) ∈ (𝐹‘𝑘)) |
14 | 11, 13 | syl 17 | . . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ∪ (𝐹‘𝑘) ∈ (𝐹‘𝑘)) |
15 | 14 | adantr 473 | . . 3 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ¬ 𝑘 = 𝑌) → ∪ (𝐹‘𝑘) ∈ (𝐹‘𝑘)) |
16 | 10, 15 | ifclda 4378 | . 2 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → if(𝑘 = 𝑌, 𝑂, ∪ (𝐹‘𝑘)) ∈ (𝐹‘𝑘)) |
17 | eldifn 3990 | . . . . 5 ⊢ (𝑘 ∈ (𝐴 ∖ {𝑌}) → ¬ 𝑘 ∈ {𝑌}) | |
18 | velsn 4451 | . . . . 5 ⊢ (𝑘 ∈ {𝑌} ↔ 𝑘 = 𝑌) | |
19 | 17, 18 | sylnib 320 | . . . 4 ⊢ (𝑘 ∈ (𝐴 ∖ {𝑌}) → ¬ 𝑘 = 𝑌) |
20 | 19 | iffalsed 4355 | . . 3 ⊢ (𝑘 ∈ (𝐴 ∖ {𝑌}) → if(𝑘 = 𝑌, 𝑂, ∪ (𝐹‘𝑘)) = ∪ (𝐹‘𝑘)) |
21 | 20 | adantl 474 | . 2 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ {𝑌})) → if(𝑘 = 𝑌, 𝑂, ∪ (𝐹‘𝑘)) = ∪ (𝐹‘𝑘)) |
22 | 1, 2, 4, 16, 21 | ptopn 21885 | 1 ⊢ (𝜑 → X𝑘 ∈ 𝐴 if(𝑘 = 𝑌, 𝑂, ∪ (𝐹‘𝑘)) ∈ (∏t‘𝐹)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 387 = wceq 1507 ∈ wcel 2048 ∖ cdif 3822 ifcif 4344 {csn 4435 ∪ cuni 4706 ⟶wf 6178 ‘cfv 6182 Xcixp 8251 Fincfn 8298 ∏tcpt 16558 Topctop 21195 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1964 ax-8 2050 ax-9 2057 ax-10 2077 ax-11 2091 ax-12 2104 ax-13 2299 ax-ext 2745 ax-rep 5043 ax-sep 5054 ax-nul 5061 ax-pow 5113 ax-pr 5180 ax-un 7273 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3or 1069 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2014 df-mo 2544 df-eu 2580 df-clab 2754 df-cleq 2765 df-clel 2840 df-nfc 2912 df-ne 2962 df-ral 3087 df-rex 3088 df-reu 3089 df-rab 3091 df-v 3411 df-sbc 3678 df-csb 3783 df-dif 3828 df-un 3830 df-in 3832 df-ss 3839 df-pss 3841 df-nul 4174 df-if 4345 df-pw 4418 df-sn 4436 df-pr 4438 df-tp 4440 df-op 4442 df-uni 4707 df-int 4744 df-iun 4788 df-br 4924 df-opab 4986 df-mpt 5003 df-tr 5025 df-id 5305 df-eprel 5310 df-po 5319 df-so 5320 df-fr 5359 df-we 5361 df-xp 5406 df-rel 5407 df-cnv 5408 df-co 5409 df-dm 5410 df-rn 5411 df-res 5412 df-ima 5413 df-pred 5980 df-ord 6026 df-on 6027 df-lim 6028 df-suc 6029 df-iota 6146 df-fun 6184 df-fn 6185 df-f 6186 df-f1 6187 df-fo 6188 df-f1o 6189 df-fv 6190 df-ov 6973 df-oprab 6974 df-mpo 6975 df-om 7391 df-wrecs 7743 df-recs 7805 df-rdg 7843 df-1o 7897 df-oadd 7901 df-er 8081 df-ixp 8252 df-en 8299 df-fin 8302 df-fi 8662 df-topgen 16563 df-pt 16564 df-top 21196 df-bases 21248 |
This theorem is referenced by: ptcld 21915 |
Copyright terms: Public domain | W3C validator |