Theorem cnrest 23612

Description: Continuity of a restriction from a subspace. (Contributed by Jeff Hankins, 11-Jul-2009.) (Revised by Mario Carneiro, 21-Aug-2015.)

Hypothesis

Ref	Expression
cnrest.1	⊢ 𝑋 = ∪ 𝐽

Assertion

Ref	Expression
cnrest	⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐴 ⊆ 𝑋) → (𝐹 ↾ 𝐴) ∈ ((𝐽 ↾t 𝐴) Cn 𝐾))

Proof of Theorem cnrest

Dummy variable 𝑜 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		cnrest.1	. . . . 5 ⊢ 𝑋 = ∪ 𝐽
2		eqid 2760	. . . . 5 ⊢ ∪ 𝐾 = ∪ 𝐾
3	1, 2	cnf 23573	. . . 4 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹:𝑋⟶∪ 𝐾)
4	3	adantr 486	. . 3 ⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐴 ⊆ 𝑋) → 𝐹:𝑋⟶∪ 𝐾)
5		simpr 490	. . 3 ⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐴 ⊆ 𝑋) → 𝐴 ⊆ 𝑋)
6	4, 5	fssresd 6754	. 2 ⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐴 ⊆ 𝑋) → (𝐹 ↾ 𝐴):𝐴⟶∪ 𝐾)
7		cnvresima 6234	. . . 4 ⊢ (◡(𝐹 ↾ 𝐴) “ 𝑜) = ((◡𝐹 “ 𝑜) ∩ 𝐴)
8		cntop1 23567	. . . . . . 7 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐽 ∈ Top)
9	8	adantr 486	. . . . . 6 ⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐴 ⊆ 𝑋) → 𝐽 ∈ Top)
10	9	adantr 486	. . . . 5 ⊢ (((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑜 ∈ 𝐾) → 𝐽 ∈ Top)
11	1	topopn 23233	. . . . . . . 8 ⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽)
12		ssexg 5281	. . . . . . . . 9 ⊢ ((𝐴 ⊆ 𝑋 ∧ 𝑋 ∈ 𝐽) → 𝐴 ∈ V)
13	12	ancoms 464	. . . . . . . 8 ⊢ ((𝑋 ∈ 𝐽 ∧ 𝐴 ⊆ 𝑋) → 𝐴 ∈ V)
14	11, 13	sylan 592	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → 𝐴 ∈ V)
15	8, 14	sylan 592	. . . . . 6 ⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐴 ⊆ 𝑋) → 𝐴 ∈ V)
16	15	adantr 486	. . . . 5 ⊢ (((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑜 ∈ 𝐾) → 𝐴 ∈ V)
17		cnima 23592	. . . . . 6 ⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑜 ∈ 𝐾) → (◡𝐹 “ 𝑜) ∈ 𝐽)
18	17	adantlr 728	. . . . 5 ⊢ (((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑜 ∈ 𝐾) → (◡𝐹 “ 𝑜) ∈ 𝐽)
19		elrestr 17608	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ V ∧ (◡𝐹 “ 𝑜) ∈ 𝐽) → ((◡𝐹 “ 𝑜) ∩ 𝐴) ∈ (𝐽 ↾t 𝐴))
20	10, 16, 18, 19	syl3anc 1398	. . . 4 ⊢ (((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑜 ∈ 𝐾) → ((◡𝐹 “ 𝑜) ∩ 𝐴) ∈ (𝐽 ↾t 𝐴))
21	7, 20	eqeltrid 2864	. . 3 ⊢ (((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑜 ∈ 𝐾) → (◡(𝐹 ↾ 𝐴) “ 𝑜) ∈ (𝐽 ↾t 𝐴))
22	21	ralrimiva 3154	. 2 ⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐴 ⊆ 𝑋) → ∀𝑜 ∈ 𝐾 (◡(𝐹 ↾ 𝐴) “ 𝑜) ∈ (𝐽 ↾t 𝐴))
23	1	toptopon 23244	. . . . 5 ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋))
24	8, 23	sylib 221	. . . 4 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐽 ∈ (TopOn‘𝑋))
25		resttopon 23488	. . . 4 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝐽 ↾t 𝐴) ∈ (TopOn‘𝐴))
26	24, 25	sylan 592	. . 3 ⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐴 ⊆ 𝑋) → (𝐽 ↾t 𝐴) ∈ (TopOn‘𝐴))
27		cntop2 23568	. . . . 5 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐾 ∈ Top)
28	27	adantr 486	. . . 4 ⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐴 ⊆ 𝑋) → 𝐾 ∈ Top)
29	2	toptopon 23244	. . . 4 ⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘∪ 𝐾))
30	28, 29	sylib 221	. . 3 ⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐴 ⊆ 𝑋) → 𝐾 ∈ (TopOn‘∪ 𝐾))
31		iscn 23562	. . 3 ⊢ (((𝐽 ↾t 𝐴) ∈ (TopOn‘𝐴) ∧ 𝐾 ∈ (TopOn‘∪ 𝐾)) → ((𝐹 ↾ 𝐴) ∈ ((𝐽 ↾t 𝐴) Cn 𝐾) ↔ ((𝐹 ↾ 𝐴):𝐴⟶∪ 𝐾 ∧ ∀𝑜 ∈ 𝐾 (◡(𝐹 ↾ 𝐴) “ 𝑜) ∈ (𝐽 ↾t 𝐴))))
32	26, 30, 31	syl2anc 596	. 2 ⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐴 ⊆ 𝑋) → ((𝐹 ↾ 𝐴) ∈ ((𝐽 ↾t 𝐴) Cn 𝐾) ↔ ((𝐹 ↾ 𝐴):𝐴⟶∪ 𝐾 ∧ ∀𝑜 ∈ 𝐾 (◡(𝐹 ↾ 𝐴) “ 𝑜) ∈ (𝐽 ↾t 𝐴))))
33	6, 22, 32	mpbir2and 726	1 ⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐴 ⊆ 𝑋) → (𝐹 ↾ 𝐴) ∈ ((𝐽 ↾t 𝐴) Cn 𝐾))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1569   ∈ wcel 2144  ∀wral 3076  Vcvv 3450   ⊆ wss 3896   ∩ cin 4088  ∪ cuni 4866  ^◡ccnv 5650   ↾ cres 5653   “ cima 5654  ⟶wf 6539  ‘cfv 6543  (class class class)co 7424   ↾_t crest 17600  Topctop 23220  TopOnctopon 23237   Cn ccn 23551

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-rep 5231  ax-sep 5248  ax-nul 5259  ax-pow 5327  ax-pr 5391  ax-un 7755

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3848  df-ss 3897  df-pss 4013  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-int 4907  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6497  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7427  df-oprab 7428  df-mpo 7429  df-om 7882  df-1st 8005  df-2nd 8006  df-map 8857  df-en 8982  df-fin 8985  df-fi 9410  df-rest 17602  df-topgen 17623  df-top 23221  df-topon 23238  df-bases 23273  df-cn 23554

This theorem is used by:  resthauslem  23690  imacmp  23724  connima  23752  kgencn2  23885  kgencn3  23886  xkopjcn  23984  cnmpt1res  24004  cnmpt2res  24005  qtoprest  24045  hmeores  24099  ftalem3  27411  rmulccn  34610  raddcn  34611  xrge0mulc1cn  34623  rrhre  34703  cvmliftmolem1  36164  cvmlift2lem9a  36186  cvmlift2lem9  36194  ivthALT  37247  broucube  38709  areacirclem2  38764  cnres2  38834  resuppsinopn  43551  stoweidlem28  47174  dirkercncflem2  47250