Metamath Proof Explorer


Theorem restbas

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

Ref Expression
Assertion restbas ( 𝐵 ∈ TopBases → ( 𝐵t 𝐴 ) ∈ TopBases )

Proof

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