Theorem resttopon 13251

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 13092	. . . 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 13103	. . . 4 |- ( J e. (TopOn ` X ) -> X e. J )
5		ssexg 4137	. . . 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 13250	. . 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 3352	. . . . . 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 12627	. . . . . 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 2253	. . . 4 |- ( ( J e. (TopOn ` X ) /\ A C_ X ) -> A e. ( J ↾t A ) )
17		elssuni 3833	. . . 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 12625	. . . . . 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 3354	. . . . . . . . 9 |- ( x i^i A ) C_ A
22		vex 2738	. . . . . . . . . . 11 |- x e. _V
23	22	inex1 4132	. . . . . . . . . 10 |- ( x i^i A ) e. _V
24	23	elpw 3578	. . . . . . . . 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 5663	. . . . . 6 |- ( ( J e. (TopOn ` X ) /\ A C_ X ) -> ( x e. J |-> ( x i^i A ) ) : J --> ~P A )
28	27	frnd 5367	. . . . 5 |- ( ( J e. (TopOn ` X ) /\ A C_ X ) -> ran ( x e. J |-> ( x i^i A ) ) C_ ~P A )
29	20, 28	eqsstrd 3189	. . . 4 |- ( ( J e. (TopOn ` X ) /\ A C_ X ) -> ( J ↾t A ) C_ ~P A )
30		sspwuni 3966	. . . 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 3170	. 2 |- ( ( J e. (TopOn ` X ) /\ A C_ X ) -> A = U. ( J ↾t A ) )
33		istopon 13091	. 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 2146   _Vcvv 2735   i^i cin 3126   C_ wss 3127   ~Pcpw 3572   U.cuni 3805   |-> cmpt 4059   ran crn 4621   ` cfv 5208  (class class class)co 5865   ↾_t crest 12619   Topctop 13075  TopOnctopon 13088

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 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-13 2148  ax-14 2149  ax-ext 2157  ax-coll 4113  ax-sep 4116  ax-pow 4169  ax-pr 4203  ax-un 4427  ax-setind 4530

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1459  df-sb 1761  df-eu 2027  df-mo 2028  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-ne 2346  df-ral 2458  df-rex 2459  df-reu 2460  df-rab 2462  df-v 2737  df-sbc 2961  df-csb 3056  df-dif 3129  df-un 3131  df-in 3133  df-ss 3140  df-pw 3574  df-sn 3595  df-pr 3596  df-op 3598  df-uni 3806  df-iun 3884  df-br 3999  df-opab 4060  df-mpt 4061  df-id 4287  df-xp 4626  df-rel 4627  df-cnv 4628  df-co 4629  df-dm 4630  df-rn 4631  df-res 4632  df-ima 4633  df-iota 5170  df-fun 5210  df-fn 5211  df-f 5212  df-f1 5213  df-fo 5214  df-f1o 5215  df-fv 5216  df-ov 5868  df-oprab 5869  df-mpo 5870  df-1st 6131  df-2nd 6132  df-rest 12621  df-topgen 12640  df-top 13076  df-topon 13089  df-bases 13121

This theorem is referenced by:  restuni  13252  stoig  13253  cnrest  13315  cnrest2  13316  cnrest2r  13317  cnptopresti  13318  cnptoprest  13319  cnptoprest2  13320  divcnap  13635  cncfmpt2fcntop  13665  cnplimcim  13716  cnlimcim  13720  cnlimc  13721  limccnpcntop  13724  limccnp2lem  13725  limccnp2cntop  13726  dvfvalap  13730  dvbss  13734  dvfgg  13737  dvcnp2cntop  13743  dvcn  13744  dvaddxxbr  13745  dvmulxxbr  13746