Theorem resstopn

Description: The topology of a restricted structure. (Contributed by Mario Carneiro, 26-Aug-2015)

	Ref	Expression
Hypotheses	resstopn.1	⊢ 𝐻 = ( 𝐾 ↾s 𝐴 )
	resstopn.2	⊢ 𝐽 = ( TopOpen ‘ 𝐾 )
Assertion	resstopn	⊢ ( 𝐽 ↾t 𝐴 ) = ( TopOpen ‘ 𝐻 )

Proof

Step	Hyp	Ref	Expression
1		resstopn.1	⊢ 𝐻 = ( 𝐾 ↾s 𝐴 )
2		resstopn.2	⊢ 𝐽 = ( TopOpen ‘ 𝐾 )
3		fvex	⊢ ( TopSet ‘ 𝐾 ) ∈ V
4		fvex	⊢ ( Base ‘ 𝐾 ) ∈ V
5		restco	⊢ ( ( ( TopSet ‘ 𝐾 ) ∈ V ∧ ( Base ‘ 𝐾 ) ∈ V ∧ 𝐴 ∈ V ) → ( ( ( TopSet ‘ 𝐾 ) ↾t ( Base ‘ 𝐾 ) ) ↾t 𝐴 ) = ( ( TopSet ‘ 𝐾 ) ↾t ( ( Base ‘ 𝐾 ) ∩ 𝐴 ) ) )
6	3 4 5	mp3an12	⊢ ( 𝐴 ∈ V → ( ( ( TopSet ‘ 𝐾 ) ↾t ( Base ‘ 𝐾 ) ) ↾t 𝐴 ) = ( ( TopSet ‘ 𝐾 ) ↾t ( ( Base ‘ 𝐾 ) ∩ 𝐴 ) ) )
7		eqid	⊢ ( TopSet ‘ 𝐾 ) = ( TopSet ‘ 𝐾 )
8	1 7	resstset	⊢ ( 𝐴 ∈ V → ( TopSet ‘ 𝐾 ) = ( TopSet ‘ 𝐻 ) )
9		incom	⊢ ( ( Base ‘ 𝐾 ) ∩ 𝐴 ) = ( 𝐴 ∩ ( Base ‘ 𝐾 ) )
10		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
11	1 10	ressbas	⊢ ( 𝐴 ∈ V → ( 𝐴 ∩ ( Base ‘ 𝐾 ) ) = ( Base ‘ 𝐻 ) )
12	9 11	syl5eq	⊢ ( 𝐴 ∈ V → ( ( Base ‘ 𝐾 ) ∩ 𝐴 ) = ( Base ‘ 𝐻 ) )
13	8 12	oveq12d	⊢ ( 𝐴 ∈ V → ( ( TopSet ‘ 𝐾 ) ↾t ( ( Base ‘ 𝐾 ) ∩ 𝐴 ) ) = ( ( TopSet ‘ 𝐻 ) ↾t ( Base ‘ 𝐻 ) ) )
14	6 13	eqtrd	⊢ ( 𝐴 ∈ V → ( ( ( TopSet ‘ 𝐾 ) ↾t ( Base ‘ 𝐾 ) ) ↾t 𝐴 ) = ( ( TopSet ‘ 𝐻 ) ↾t ( Base ‘ 𝐻 ) ) )
15	10 7	topnval	⊢ ( ( TopSet ‘ 𝐾 ) ↾t ( Base ‘ 𝐾 ) ) = ( TopOpen ‘ 𝐾 )
16	15 2	eqtr4i	⊢ ( ( TopSet ‘ 𝐾 ) ↾t ( Base ‘ 𝐾 ) ) = 𝐽
17	16	oveq1i	⊢ ( ( ( TopSet ‘ 𝐾 ) ↾t ( Base ‘ 𝐾 ) ) ↾t 𝐴 ) = ( 𝐽 ↾t 𝐴 )
18		eqid	⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
19		eqid	⊢ ( TopSet ‘ 𝐻 ) = ( TopSet ‘ 𝐻 )
20	18 19	topnval	⊢ ( ( TopSet ‘ 𝐻 ) ↾t ( Base ‘ 𝐻 ) ) = ( TopOpen ‘ 𝐻 )
21	14 17 20	3eqtr3g	⊢ ( 𝐴 ∈ V → ( 𝐽 ↾t 𝐴 ) = ( TopOpen ‘ 𝐻 ) )
22		simpr	⊢ ( ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) → 𝐴 ∈ V )
23		restfn	⊢ ↾t Fn ( V × V )
24	23	fndmi	⊢ dom ↾t = ( V × V )
25	24	ndmov	⊢ ( ¬ ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) → ( 𝐽 ↾t 𝐴 ) = ∅ )
26	22 25	nsyl5	⊢ ( ¬ 𝐴 ∈ V → ( 𝐽 ↾t 𝐴 ) = ∅ )
27		reldmress	⊢ Rel dom ↾s
28	27	ovprc2	⊢ ( ¬ 𝐴 ∈ V → ( 𝐾 ↾s 𝐴 ) = ∅ )
29	1 28	syl5eq	⊢ ( ¬ 𝐴 ∈ V → 𝐻 = ∅ )
30	29	fveq2d	⊢ ( ¬ 𝐴 ∈ V → ( TopSet ‘ 𝐻 ) = ( TopSet ‘ ∅ ) )
31		df-tset	⊢ TopSet = Slot 9
32	31	str0	⊢ ∅ = ( TopSet ‘ ∅ )
33	30 32	eqtr4di	⊢ ( ¬ 𝐴 ∈ V → ( TopSet ‘ 𝐻 ) = ∅ )
34	33	oveq1d	⊢ ( ¬ 𝐴 ∈ V → ( ( TopSet ‘ 𝐻 ) ↾t ( Base ‘ 𝐻 ) ) = ( ∅ ↾t ( Base ‘ 𝐻 ) ) )
35		0rest	⊢ ( ∅ ↾t ( Base ‘ 𝐻 ) ) = ∅
36	34 20 35	3eqtr3g	⊢ ( ¬ 𝐴 ∈ V → ( TopOpen ‘ 𝐻 ) = ∅ )
37	26 36	eqtr4d	⊢ ( ¬ 𝐴 ∈ V → ( 𝐽 ↾t 𝐴 ) = ( TopOpen ‘ 𝐻 ) )
38	21 37	pm2.61i	⊢ ( 𝐽 ↾t 𝐴 ) = ( TopOpen ‘ 𝐻 )