Theorem resttopon 13453

Description: A subspace topology is a topology on the base set. (Contributed by Mario Carneiro, 13-Aug-2015.)

Assertion

Ref	Expression
resttopon	|- ( ( J e. (TopOn ` X ) /\ A C_ X ) -> ( J ↾t A ) e. (TopOn ` A ) )

Proof of Theorem resttopon

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		topontop 13294	. . . 4 |- ( J e. (TopOn ` X ) -> J e. Top )
2	1	adantr 276	. . 3 |- ( ( J e. (TopOn ` X ) /\ A C_ X ) -> J e. Top )
3		id 19	. . . 4 |- ( A C_ X -> A C_ X )
4		toponmax 13305	. . . 4 |- ( J e. (TopOn ` X ) -> X e. J )
5		ssexg 4140	. . . 4 |- ( ( A C_ X /\ X e. J ) -> A e. _V )
6	3, 4, 5	syl2anr 290	. . 3 |- ( ( J e. (TopOn ` X ) /\ A C_ X ) -> A e. _V )
7		resttop 13452	. . 3 |- ( ( J e. Top /\ A e. _V ) -> ( J ↾t A ) e. Top )
8	2, 6, 7	syl2anc 411	. 2 |- ( ( J e. (TopOn ` X ) /\ A C_ X ) -> ( J ↾t A ) e. Top )
9		simpr 110	. . . . . 6 |- ( ( J e. (TopOn ` X ) /\ A C_ X ) -> A C_ X )
10		sseqin2 3354	. . . . . 6 |- ( A C_ X <-> ( X i^i A ) = A )
11	9, 10	sylib 122	. . . . 5 |- ( ( J e. (TopOn ` X ) /\ A C_ X ) -> ( X i^i A ) = A )
12		simpl 109	. . . . . 6 |- ( ( J e. (TopOn ` X ) /\ A C_ X ) -> J e. (TopOn ` X ) )
13	4	adantr 276	. . . . . 6 |- ( ( J e. (TopOn ` X ) /\ A C_ X ) -> X e. J )
14		elrestr 12682	. . . . . 6 |- ( ( J e. (TopOn ` X ) /\ A e. _V /\ X e. J ) -> ( X i^i A ) e. ( J ↾t A ) )
15	12, 6, 13, 14	syl3anc 1238	. . . . 5 |- ( ( J e. (TopOn ` X ) /\ A C_ X ) -> ( X i^i A ) e. ( J ↾t A ) )
16	11, 15	eqeltrrd 2255	. . . 4 |- ( ( J e. (TopOn ` X ) /\ A C_ X ) -> A e. ( J ↾t A ) )
17		elssuni 3836	. . . 4 |- ( A e. ( J ↾t A ) -> A C_ U. ( J ↾t A ) )
18	16, 17	syl 14	. . 3 |- ( ( J e. (TopOn ` X ) /\ A C_ X ) -> A C_ U. ( J ↾t A ) )
19		restval 12680	. . . . . 6 |- ( ( J e. (TopOn ` X ) /\ A e. _V ) -> ( J ↾t A ) = ran ( x e. J |-> ( x i^i A ) ) )
20	6, 19	syldan 282	. . . . 5 |- ( ( J e. (TopOn ` X ) /\ A C_ X ) -> ( J ↾t A ) = ran ( x e. J |-> ( x i^i A ) ) )
21		inss2 3356	. . . . . . . . 9 |- ( x i^i A ) C_ A
22		vex 2740	. . . . . . . . . . 11 |- x e. _V
23	22	inex1 4135	. . . . . . . . . 10 |- ( x i^i A ) e. _V
24	23	elpw 3581	. . . . . . . . 9 |- ( ( x i^i A ) e. ~P A <-> ( x i^i A ) C_ A )
25	21, 24	mpbir 146	. . . . . . . 8 |- ( x i^i A ) e. ~P A
26	25	a1i 9	. . . . . . 7 |- ( ( ( J e. (TopOn ` X ) /\ A C_ X ) /\ x e. J ) -> ( x i^i A ) e. ~P A )
27	26	fmpttd 5668	. . . . . 6 |- ( ( J e. (TopOn ` X ) /\ A C_ X ) -> ( x e. J |-> ( x i^i A ) ) : J --> ~P A )
28	27	frnd 5372	. . . . 5 |- ( ( J e. (TopOn ` X ) /\ A C_ X ) -> ran ( x e. J |-> ( x i^i A ) ) C_ ~P A )
29	20, 28	eqsstrd 3191	. . . 4 |- ( ( J e. (TopOn ` X ) /\ A C_ X ) -> ( J ↾t A ) C_ ~P A )
30		sspwuni 3969	. . . 4 |- ( ( J ↾t A ) C_ ~P A <-> U. ( J ↾t A ) C_ A )
31	29, 30	sylib 122	. . 3 |- ( ( J e. (TopOn ` X ) /\ A C_ X ) -> U. ( J ↾t A ) C_ A )
32	18, 31	eqssd 3172	. 2 |- ( ( J e. (TopOn ` X ) /\ A C_ X ) -> A = U. ( J ↾t A ) )
33		istopon 13293	. 2 |- ( ( J ↾t A ) e. (TopOn ` A ) <-> ( ( J ↾t A ) e. Top /\ A = U. ( J ↾t A ) ) )
34	8, 32, 33	sylanbrc 417	1 |- ( ( J e. (TopOn ` X ) /\ A C_ X ) -> ( J ↾t A ) e. (TopOn ` A ) )

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1353   e. wcel 2148   _Vcvv 2737   i^i cin 3128   C_ wss 3129   ~Pcpw 3575   U.cuni 3808   |-> cmpt 4062   ran crn 4625   ` cfv 5213  (class class class)co 5870   ↾_t crest 12674   Topctop 13277  TopOnctopon 13290

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4116  ax-sep 4119  ax-pow 4172  ax-pr 4207  ax-un 4431  ax-setind 4534

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2739  df-sbc 2963  df-csb 3058  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-pw 3577  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3809  df-iun 3887  df-br 4002  df-opab 4063  df-mpt 4064  df-id 4291  df-xp 4630  df-rel 4631  df-cnv 4632  df-co 4633  df-dm 4634  df-rn 4635  df-res 4636  df-ima 4637  df-iota 5175  df-fun 5215  df-fn 5216  df-f 5217  df-f1 5218  df-fo 5219  df-f1o 5220  df-fv 5221  df-ov 5873  df-oprab 5874  df-mpo 5875  df-1st 6136  df-2nd 6137  df-rest 12676  df-topgen 12695  df-top 13278  df-topon 13291  df-bases 13323

This theorem is referenced by:  restuni  13454  stoig  13455  cnrest  13517  cnrest2  13518  cnrest2r  13519  cnptopresti  13520  cnptoprest  13521  cnptoprest2  13522  divcnap  13837  cncfmpt2fcntop  13867  cnplimcim  13918  cnlimcim  13922  cnlimc  13923  limccnpcntop  13926  limccnp2lem  13927  limccnp2cntop  13928  dvfvalap  13932  dvbss  13936  dvfgg  13939  dvcnp2cntop  13945  dvcn  13946  dvaddxxbr  13947  dvmulxxbr  13948