Metamath Proof Explorer


Theorem restbas

Description: A subspace topology basis is a basis. (Contributed by Mario Carneiro, 19-Mar-2015)

Ref Expression
Assertion restbas B TopBases B 𝑡 A TopBases

Proof

Step Hyp Ref Expression
1 elrest B TopBases A V a B 𝑡 A u B a = u A
2 elrest B TopBases A V b B 𝑡 A v B b = v A
3 1 2 anbi12d B TopBases A V a B 𝑡 A b B 𝑡 A u B a = u A v B b = v A
4 reeanv u B v B a = u A b = v A u B a = u A v B b = v A
5 3 4 bitr4di B TopBases A V a B 𝑡 A b B 𝑡 A u B v B a = u A b = v A
6 simplll B TopBases A V u B v B c u v A B TopBases
7 simplrl B TopBases A V u B v B c u v A u B
8 simplrr B TopBases A V u B v B c u v A v B
9 simpr B TopBases A V u B v B c u v A c u v A
10 9 elin1d B TopBases A V u B v B c u v A c u v
11 basis2 B TopBases u B v B c u v z B c z z u v
12 6 7 8 10 11 syl22anc B TopBases A V u B v B c u v A z B c z z u v
13 simplll B TopBases A V u B v B c u v A z B c z z u v B TopBases A V
14 13 simpld B TopBases A V u B v B c u v A z B c z z u v B TopBases
15 13 simprd B TopBases A V u B v B c u v A z B c z z u v A V
16 simprl B TopBases A V u B v B c u v A z B c z z u v z B
17 elrestr B TopBases A V z B z A B 𝑡 A
18 14 15 16 17 syl3anc B TopBases A V u B v B c u v A z B c z z u v z A B 𝑡 A
19 simprrl B TopBases A V u B v B c u v A z B c z z u v c z
20 simplr B TopBases A V u B v B c u v A z B c z z u v c u v A
21 20 elin2d B TopBases A V u B v B c u v A z B c z z u v c A
22 19 21 elind B TopBases A V u B v B c u v A z B c z z u v c z A
23 simprrr B TopBases A V u B v B c u v A z B c z z u v z u v
24 23 ssrind B TopBases A V u B v B c u v A z B c z z u v z A u v A
25 eleq2 w = z A c w c z A
26 sseq1 w = z A w u v A z A u v A
27 25 26 anbi12d w = z A c w w u v A c z A z A u v A
28 27 rspcev z A B 𝑡 A c z A z A u v A w B 𝑡 A c w w u v A
29 18 22 24 28 syl12anc B TopBases A V u B v B c u v A z B c z z u v w B 𝑡 A c w w u v A
30 12 29 rexlimddv B TopBases A V u B v B c u v A w B 𝑡 A c w w u v A
31 30 ralrimiva B TopBases A V u B v B c u v A w B 𝑡 A c w w u v A
32 ineq12 a = u A b = v A a b = u A v A
33 inindir u v A = u A v A
34 32 33 eqtr4di a = u A b = v A a b = u v A
35 34 sseq2d a = u A b = v A w a b w u v A
36 35 anbi2d a = u A b = v A c w w a b c w w u v A
37 36 rexbidv a = u A b = v A w B 𝑡 A c w w a b w B 𝑡 A c w w u v A
38 34 37 raleqbidv a = u A b = v A c a b w B 𝑡 A c w w a b c u v A w B 𝑡 A c w w u v A
39 31 38 syl5ibrcom B TopBases A V u B v B a = u A b = v A c a b w B 𝑡 A c w w a b
40 39 rexlimdvva B TopBases A V u B v B a = u A b = v A c a b w B 𝑡 A c w w a b
41 5 40 sylbid B TopBases A V a B 𝑡 A b B 𝑡 A c a b w B 𝑡 A c w w a b
42 41 ralrimivv B TopBases A V a B 𝑡 A b B 𝑡 A c a b w B 𝑡 A c w w a b
43 ovex B 𝑡 A V
44 isbasis2g B 𝑡 A V B 𝑡 A TopBases a B 𝑡 A b B 𝑡 A c a b w B 𝑡 A c w w a b
45 43 44 ax-mp B 𝑡 A TopBases a B 𝑡 A b B 𝑡 A c a b w B 𝑡 A c w w a b
46 42 45 sylibr B TopBases A V B 𝑡 A TopBases
47 relxp Rel V × V
48 restfn 𝑡 Fn V × V
49 fndm 𝑡 Fn V × V dom 𝑡 = V × V
50 48 49 ax-mp dom 𝑡 = V × V
51 50 releqi Rel dom 𝑡 Rel V × V
52 47 51 mpbir Rel dom 𝑡
53 52 ovprc2 ¬ A V B 𝑡 A =
54 53 adantl B TopBases ¬ A V B 𝑡 A =
55 fi0 fi =
56 fibas fi TopBases
57 55 56 eqeltrri TopBases
58 54 57 eqeltrdi B TopBases ¬ A V B 𝑡 A TopBases
59 46 58 pm2.61dan B TopBases B 𝑡 A TopBases