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 syl6bbr ⊢ ( ( 𝐵 ∈ 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 )