Metamath Proof Explorer


Theorem ptbasin

Description: The basis for a product topology is closed under intersections. (Contributed by Mario Carneiro, 3-Feb-2015)

Ref Expression
Hypothesis ptbas.1 B = x | g g Fn A y A g y F y z Fin y A z g y = F y x = y A g y
Assertion ptbasin A V F : A Top X B Y B X Y B

Proof

Step Hyp Ref Expression
1 ptbas.1 B = x | g g Fn A y A g y F y z Fin y A z g y = F y x = y A g y
2 1 elpt X B a a Fn A y A a y F y c Fin y A c a y = F y X = y A a y
3 1 elpt Y B b b Fn A y A b y F y d Fin y A d b y = F y Y = y A b y
4 2 3 anbi12i X B Y B a a Fn A y A a y F y c Fin y A c a y = F y X = y A a y b b Fn A y A b y F y d Fin y A d b y = F y Y = y A b y
5 exdistrv a b a Fn A y A a y F y c Fin y A c a y = F y X = y A a y b Fn A y A b y F y d Fin y A d b y = F y Y = y A b y a a Fn A y A a y F y c Fin y A c a y = F y X = y A a y b b Fn A y A b y F y d Fin y A d b y = F y Y = y A b y
6 4 5 bitr4i X B Y B a b a Fn A y A a y F y c Fin y A c a y = F y X = y A a y b Fn A y A b y F y d Fin y A d b y = F y Y = y A b y
7 an4 a Fn A y A a y F y c Fin y A c a y = F y X = y A a y b Fn A y A b y F y d Fin y A d b y = F y Y = y A b y a Fn A y A a y F y c Fin y A c a y = F y b Fn A y A b y F y d Fin y A d b y = F y X = y A a y Y = y A b y
8 an6 a Fn A y A a y F y c Fin y A c a y = F y b Fn A y A b y F y d Fin y A d b y = F y a Fn A b Fn A y A a y F y y A b y F y c Fin y A c a y = F y d Fin y A d b y = F y
9 df-3an a Fn A b Fn A y A a y F y y A b y F y c Fin y A c a y = F y d Fin y A d b y = F y a Fn A b Fn A y A a y F y y A b y F y c Fin y A c a y = F y d Fin y A d b y = F y
10 8 9 bitri a Fn A y A a y F y c Fin y A c a y = F y b Fn A y A b y F y d Fin y A d b y = F y a Fn A b Fn A y A a y F y y A b y F y c Fin y A c a y = F y d Fin y A d b y = F y
11 reeanv c Fin d Fin y A c a y = F y y A d b y = F y c Fin y A c a y = F y d Fin y A d b y = F y
12 fveq2 y = k a y = a k
13 fveq2 y = k b y = b k
14 12 13 ineq12d y = k a y b y = a k b k
15 14 cbvixpv y A a y b y = k A a k b k
16 simpl1l A V F : A Top a Fn A b Fn A y A a y F y y A b y F y c Fin d Fin y A c a y = F y y A d b y = F y A V
17 unfi c Fin d Fin c d Fin
18 17 ad2antrl A V F : A Top a Fn A b Fn A y A a y F y y A b y F y c Fin d Fin y A c a y = F y y A d b y = F y c d Fin
19 simpl1r A V F : A Top a Fn A b Fn A y A a y F y y A b y F y c Fin d Fin y A c a y = F y y A d b y = F y F : A Top
20 19 ffvelrnda A V F : A Top a Fn A b Fn A y A a y F y y A b y F y c Fin d Fin y A c a y = F y y A d b y = F y k A F k Top
21 simpl3l A V F : A Top a Fn A b Fn A y A a y F y y A b y F y c Fin d Fin y A c a y = F y y A d b y = F y y A a y F y
22 fveq2 y = k F y = F k
23 12 22 eleq12d y = k a y F y a k F k
24 23 rspccva y A a y F y k A a k F k
25 21 24 sylan A V F : A Top a Fn A b Fn A y A a y F y y A b y F y c Fin d Fin y A c a y = F y y A d b y = F y k A a k F k
26 simpl3r A V F : A Top a Fn A b Fn A y A a y F y y A b y F y c Fin d Fin y A c a y = F y y A d b y = F y y A b y F y
27 13 22 eleq12d y = k b y F y b k F k
28 27 rspccva y A b y F y k A b k F k
29 26 28 sylan A V F : A Top a Fn A b Fn A y A a y F y y A b y F y c Fin d Fin y A c a y = F y y A d b y = F y k A b k F k
30 inopn F k Top a k F k b k F k a k b k F k
31 20 25 29 30 syl3anc A V F : A Top a Fn A b Fn A y A a y F y y A b y F y c Fin d Fin y A c a y = F y y A d b y = F y k A a k b k F k
32 simprrl A V F : A Top a Fn A b Fn A y A a y F y y A b y F y c Fin d Fin y A c a y = F y y A d b y = F y y A c a y = F y
33 ssun1 c c d
34 sscon c c d A c d A c
35 33 34 ax-mp A c d A c
36 35 sseli k A c d k A c
37 22 unieqd y = k F y = F k
38 12 37 eqeq12d y = k a y = F y a k = F k
39 38 rspccva y A c a y = F y k A c a k = F k
40 32 36 39 syl2an A V F : A Top a Fn A b Fn A y A a y F y y A b y F y c Fin d Fin y A c a y = F y y A d b y = F y k A c d a k = F k
41 simprrr A V F : A Top a Fn A b Fn A y A a y F y y A b y F y c Fin d Fin y A c a y = F y y A d b y = F y y A d b y = F y
42 ssun2 d c d
43 sscon d c d A c d A d
44 42 43 ax-mp A c d A d
45 44 sseli k A c d k A d
46 13 37 eqeq12d y = k b y = F y b k = F k
47 46 rspccva y A d b y = F y k A d b k = F k
48 41 45 47 syl2an A V F : A Top a Fn A b Fn A y A a y F y y A b y F y c Fin d Fin y A c a y = F y y A d b y = F y k A c d b k = F k
49 40 48 ineq12d A V F : A Top a Fn A b Fn A y A a y F y y A b y F y c Fin d Fin y A c a y = F y y A d b y = F y k A c d a k b k = F k F k
50 inidm F k F k = F k
51 49 50 eqtrdi A V F : A Top a Fn A b Fn A y A a y F y y A b y F y c Fin d Fin y A c a y = F y y A d b y = F y k A c d a k b k = F k
52 1 16 18 31 51 elptr2 A V F : A Top a Fn A b Fn A y A a y F y y A b y F y c Fin d Fin y A c a y = F y y A d b y = F y k A a k b k B
53 15 52 eqeltrid A V F : A Top a Fn A b Fn A y A a y F y y A b y F y c Fin d Fin y A c a y = F y y A d b y = F y y A a y b y B
54 53 expr A V F : A Top a Fn A b Fn A y A a y F y y A b y F y c Fin d Fin y A c a y = F y y A d b y = F y y A a y b y B
55 54 rexlimdvva A V F : A Top a Fn A b Fn A y A a y F y y A b y F y c Fin d Fin y A c a y = F y y A d b y = F y y A a y b y B
56 11 55 syl5bir A V F : A Top a Fn A b Fn A y A a y F y y A b y F y c Fin y A c a y = F y d Fin y A d b y = F y y A a y b y B
57 56 3expb A V F : A Top a Fn A b Fn A y A a y F y y A b y F y c Fin y A c a y = F y d Fin y A d b y = F y y A a y b y B
58 57 impr A V F : A Top a Fn A b Fn A y A a y F y y A b y F y c Fin y A c a y = F y d Fin y A d b y = F y y A a y b y B
59 10 58 sylan2b A V F : A Top a Fn A y A a y F y c Fin y A c a y = F y b Fn A y A b y F y d Fin y A d b y = F y y A a y b y B
60 ineq12 X = y A a y Y = y A b y X Y = y A a y y A b y
61 ixpin y A a y b y = y A a y y A b y
62 60 61 eqtr4di X = y A a y Y = y A b y X Y = y A a y b y
63 62 eleq1d X = y A a y Y = y A b y X Y B y A a y b y B
64 59 63 syl5ibrcom A V F : A Top a Fn A y A a y F y c Fin y A c a y = F y b Fn A y A b y F y d Fin y A d b y = F y X = y A a y Y = y A b y X Y B
65 64 expimpd A V F : A Top a Fn A y A a y F y c Fin y A c a y = F y b Fn A y A b y F y d Fin y A d b y = F y X = y A a y Y = y A b y X Y B
66 7 65 syl5bi A V F : A Top a Fn A y A a y F y c Fin y A c a y = F y X = y A a y b Fn A y A b y F y d Fin y A d b y = F y Y = y A b y X Y B
67 66 exlimdvv A V F : A Top a b a Fn A y A a y F y c Fin y A c a y = F y X = y A a y b Fn A y A b y F y d Fin y A d b y = F y Y = y A b y X Y B
68 6 67 syl5bi A V F : A Top X B Y B X Y B
69 68 imp A V F : A Top X B Y B X Y B