Theorem qtoptop2 19294

Description: The quotient topology is a topology. (Contributed by Mario Carneiro, 23-Mar-2015.)

Assertion

Ref	Expression
qtoptop2	|- ( ( J e. Top /\ F e. V /\ Fun F ) -> ( J qTop F ) e. Top )

Proof of Theorem qtoptop2

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2443	. . . 4 |- U. J = U. J
2	1	qtopres 19293	. . 3 |- ( F e. V -> ( J qTop F ) = ( J qTop ( F |` U. J ) ) )
3	2	3ad2ant2 1010	. 2 |- ( ( J e. Top /\ F e. V /\ Fun F ) -> ( J qTop F ) = ( J qTop ( F |` U. J ) ) )
4		simp1 988	. . . . . . . . . . . . 13 |- ( ( J e. Top /\ F e. V /\ Fun F ) -> J e. Top )
5		funres 5478	. . . . . . . . . . . . . . 15 |- ( Fun F -> Fun ( F |` U. J ) )
6	5	3ad2ant3 1011	. . . . . . . . . . . . . 14 |- ( ( J e. Top /\ F e. V /\ Fun F ) -> Fun ( F |` U. J ) )
7		funforn 5648	. . . . . . . . . . . . . 14 |- ( Fun ( F |` U. J ) <-> ( F |` U. J ) : dom ( F |` U. J ) -onto-> ran ( F |` U. J ) )
8	6, 7	sylib 196	. . . . . . . . . . . . 13 |- ( ( J e. Top /\ F e. V /\ Fun F ) -> ( F |` U. J ) : dom ( F |` U. J ) -onto-> ran ( F |` U. J ) )
9		dmres 5152	. . . . . . . . . . . . . . 15 |- dom ( F |` U. J ) = ( U. J i^i dom F )
10		inss1 3591	. . . . . . . . . . . . . . 15 |- ( U. J i^i dom F ) C_ U. J
11	9, 10	eqsstri 3407	. . . . . . . . . . . . . 14 |- dom ( F |` U. J ) C_ U. J
12	11	a1i 11	. . . . . . . . . . . . 13 |- ( ( J e. Top /\ F e. V /\ Fun F ) -> dom ( F |` U. J ) C_ U. J )
13	1	elqtop 19292	. . . . . . . . . . . . 13 |- ( ( J e. Top /\ ( F |` U. J ) : dom ( F |` U. J ) -onto-> ran ( F |` U. J ) /\ dom ( F |` U. J ) C_ U. J ) -> ( y e. ( J qTop ( F |` U. J ) ) <-> ( y C_ ran ( F |` U. J ) /\ ( `' ( F |` U. J ) " y ) e. J ) ) )
14	4, 8, 12, 13	syl3anc 1218	. . . . . . . . . . . 12 |- ( ( J e. Top /\ F e. V /\ Fun F ) -> ( y e. ( J qTop ( F |` U. J ) ) <-> ( y C_ ran ( F |` U. J ) /\ ( `' ( F |` U. J ) " y ) e. J ) ) )
15	14	simprbda 623	. . . . . . . . . . 11 |- ( ( ( J e. Top /\ F e. V /\ Fun F ) /\ y e. ( J qTop ( F |` U. J ) ) ) -> y C_ ran ( F |` U. J ) )
16		selpw 3888	. . . . . . . . . . 11 |- ( y e. ~P ran ( F |` U. J ) <-> y C_ ran ( F |` U. J ) )
17	15, 16	sylibr 212	. . . . . . . . . 10 |- ( ( ( J e. Top /\ F e. V /\ Fun F ) /\ y e. ( J qTop ( F |` U. J ) ) ) -> y e. ~P ran ( F |` U. J ) )
18	17	ex 434	. . . . . . . . 9 |- ( ( J e. Top /\ F e. V /\ Fun F ) -> ( y e. ( J qTop ( F |` U. J ) ) -> y e. ~P ran ( F |` U. J ) ) )
19	18	ssrdv 3383	. . . . . . . 8 |- ( ( J e. Top /\ F e. V /\ Fun F ) -> ( J qTop ( F |` U. J ) ) C_ ~P ran ( F |` U. J ) )
20		sstr2 3384	. . . . . . . 8 |- ( x C_ ( J qTop ( F |` U. J ) ) -> ( ( J qTop ( F |` U. J ) ) C_ ~P ran ( F |` U. J ) -> x C_ ~P ran ( F |` U. J ) ) )
21	19, 20	syl5com 30	. . . . . . 7 |- ( ( J e. Top /\ F e. V /\ Fun F ) -> ( x C_ ( J qTop ( F |` U. J ) ) -> x C_ ~P ran ( F |` U. J ) ) )
22		sspwuni 4277	. . . . . . 7 |- ( x C_ ~P ran ( F |` U. J ) <-> U. x C_ ran ( F |` U. J ) )
23	21, 22	syl6ib 226	. . . . . 6 |- ( ( J e. Top /\ F e. V /\ Fun F ) -> ( x C_ ( J qTop ( F |` U. J ) ) -> U. x C_ ran ( F |` U. J ) ) )
24		imauni 5984	. . . . . . . 8 |- ( `' ( F |` U. J ) " U. x ) = U_ y e. x ( `' ( F |` U. J ) " y )
25		simpl1 991	. . . . . . . . 9 |- ( ( ( J e. Top /\ F e. V /\ Fun F ) /\ x C_ ( J qTop ( F |` U. J ) ) ) -> J e. Top )
26	14	simplbda 624	. . . . . . . . . . 11 |- ( ( ( J e. Top /\ F e. V /\ Fun F ) /\ y e. ( J qTop ( F |` U. J ) ) ) -> ( `' ( F |` U. J ) " y ) e. J )
27	26	ralrimiva 2820	. . . . . . . . . 10 |- ( ( J e. Top /\ F e. V /\ Fun F ) -> A. y e. ( J qTop ( F |` U. J ) ) ( `' ( F |` U. J ) " y ) e. J )
28		ssralv 3437	. . . . . . . . . 10 |- ( x C_ ( J qTop ( F |` U. J ) ) -> ( A. y e. ( J qTop ( F |` U. J ) ) ( `' ( F |` U. J ) " y ) e. J -> A. y e. x ( `' ( F |` U. J ) " y ) e. J ) )
29	27, 28	mpan9 469	. . . . . . . . 9 |- ( ( ( J e. Top /\ F e. V /\ Fun F ) /\ x C_ ( J qTop ( F |` U. J ) ) ) -> A. y e. x ( `' ( F |` U. J ) " y ) e. J )
30		iunopn 18533	. . . . . . . . 9 |- ( ( J e. Top /\ A. y e. x ( `' ( F |` U. J ) " y ) e. J ) -> U_ y e. x ( `' ( F |` U. J ) " y ) e. J )
31	25, 29, 30	syl2anc 661	. . . . . . . 8 |- ( ( ( J e. Top /\ F e. V /\ Fun F ) /\ x C_ ( J qTop ( F |` U. J ) ) ) -> U_ y e. x ( `' ( F |` U. J ) " y ) e. J )
32	24, 31	syl5eqel 2527	. . . . . . 7 |- ( ( ( J e. Top /\ F e. V /\ Fun F ) /\ x C_ ( J qTop ( F |` U. J ) ) ) -> ( `' ( F |` U. J ) " U. x ) e. J )
33	32	ex 434	. . . . . 6 |- ( ( J e. Top /\ F e. V /\ Fun F ) -> ( x C_ ( J qTop ( F |` U. J ) ) -> ( `' ( F |` U. J ) " U. x ) e. J ) )
34	23, 33	jcad 533	. . . . 5 |- ( ( J e. Top /\ F e. V /\ Fun F ) -> ( x C_ ( J qTop ( F |` U. J ) ) -> ( U. x C_ ran ( F |` U. J ) /\ ( `' ( F |` U. J ) " U. x ) e. J ) ) )
35	1	elqtop 19292	. . . . . 6 |- ( ( J e. Top /\ ( F |` U. J ) : dom ( F |` U. J ) -onto-> ran ( F |` U. J ) /\ dom ( F |` U. J ) C_ U. J ) -> ( U. x e. ( J qTop ( F |` U. J ) ) <-> ( U. x C_ ran ( F |` U. J ) /\ ( `' ( F |` U. J ) " U. x ) e. J ) ) )
36	4, 8, 12, 35	syl3anc 1218	. . . . 5 |- ( ( J e. Top /\ F e. V /\ Fun F ) -> ( U. x e. ( J qTop ( F |` U. J ) ) <-> ( U. x C_ ran ( F |` U. J ) /\ ( `' ( F |` U. J ) " U. x ) e. J ) ) )
37	34, 36	sylibrd 234	. . . 4 |- ( ( J e. Top /\ F e. V /\ Fun F ) -> ( x C_ ( J qTop ( F |` U. J ) ) -> U. x e. ( J qTop ( F |` U. J ) ) ) )
38	37	alrimiv 1685	. . 3 |- ( ( J e. Top /\ F e. V /\ Fun F ) -> A. x ( x C_ ( J qTop ( F |` U. J ) ) -> U. x e. ( J qTop ( F |` U. J ) ) ) )
39		inss1 3591	. . . . . 6 |- ( x i^i y ) C_ x
40	1	elqtop 19292	. . . . . . . . . 10 |- ( ( J e. Top /\ ( F |` U. J ) : dom ( F |` U. J ) -onto-> ran ( F |` U. J ) /\ dom ( F |` U. J ) C_ U. J ) -> ( x e. ( J qTop ( F |` U. J ) ) <-> ( x C_ ran ( F |` U. J ) /\ ( `' ( F |` U. J ) " x ) e. J ) ) )
41	4, 8, 12, 40	syl3anc 1218	. . . . . . . . 9 |- ( ( J e. Top /\ F e. V /\ Fun F ) -> ( x e. ( J qTop ( F |` U. J ) ) <-> ( x C_ ran ( F |` U. J ) /\ ( `' ( F |` U. J ) " x ) e. J ) ) )
42	41	biimpa 484	. . . . . . . 8 |- ( ( ( J e. Top /\ F e. V /\ Fun F ) /\ x e. ( J qTop ( F |` U. J ) ) ) -> ( x C_ ran ( F |` U. J ) /\ ( `' ( F |` U. J ) " x ) e. J ) )
43	42	adantrr 716	. . . . . . 7 |- ( ( ( J e. Top /\ F e. V /\ Fun F ) /\ ( x e. ( J qTop ( F |` U. J ) ) /\ y e. ( J qTop ( F |` U. J ) ) ) ) -> ( x C_ ran ( F |` U. J ) /\ ( `' ( F |` U. J ) " x ) e. J ) )
44	43	simpld 459	. . . . . 6 |- ( ( ( J e. Top /\ F e. V /\ Fun F ) /\ ( x e. ( J qTop ( F |` U. J ) ) /\ y e. ( J qTop ( F |` U. J ) ) ) ) -> x C_ ran ( F |` U. J ) )
45	39, 44	syl5ss 3388	. . . . 5 |- ( ( ( J e. Top /\ F e. V /\ Fun F ) /\ ( x e. ( J qTop ( F |` U. J ) ) /\ y e. ( J qTop ( F |` U. J ) ) ) ) -> ( x i^i y ) C_ ran ( F |` U. J ) )
46	6	adantr 465	. . . . . . 7 |- ( ( ( J e. Top /\ F e. V /\ Fun F ) /\ ( x e. ( J qTop ( F |` U. J ) ) /\ y e. ( J qTop ( F |` U. J ) ) ) ) -> Fun ( F |` U. J ) )
47		inpreima 5851	. . . . . . 7 |- ( Fun ( F |` U. J ) -> ( `' ( F |` U. J ) " ( x i^i y ) ) = ( ( `' ( F |` U. J ) " x ) i^i ( `' ( F |` U. J ) " y ) ) )
48	46, 47	syl 16	. . . . . 6 |- ( ( ( J e. Top /\ F e. V /\ Fun F ) /\ ( x e. ( J qTop ( F |` U. J ) ) /\ y e. ( J qTop ( F |` U. J ) ) ) ) -> ( `' ( F |` U. J ) " ( x i^i y ) ) = ( ( `' ( F |` U. J ) " x ) i^i ( `' ( F |` U. J ) " y ) ) )
49	4	adantr 465	. . . . . . 7 |- ( ( ( J e. Top /\ F e. V /\ Fun F ) /\ ( x e. ( J qTop ( F |` U. J ) ) /\ y e. ( J qTop ( F |` U. J ) ) ) ) -> J e. Top )
50	43	simprd 463	. . . . . . 7 |- ( ( ( J e. Top /\ F e. V /\ Fun F ) /\ ( x e. ( J qTop ( F |` U. J ) ) /\ y e. ( J qTop ( F |` U. J ) ) ) ) -> ( `' ( F |` U. J ) " x ) e. J )
51	26	adantrl 715	. . . . . . 7 |- ( ( ( J e. Top /\ F e. V /\ Fun F ) /\ ( x e. ( J qTop ( F |` U. J ) ) /\ y e. ( J qTop ( F |` U. J ) ) ) ) -> ( `' ( F |` U. J ) " y ) e. J )
52		inopn 18534	. . . . . . 7 |- ( ( J e. Top /\ ( `' ( F |` U. J ) " x ) e. J /\ ( `' ( F |` U. J ) " y ) e. J ) -> ( ( `' ( F |` U. J ) " x ) i^i ( `' ( F |` U. J ) " y ) ) e. J )
53	49, 50, 51, 52	syl3anc 1218	. . . . . 6 |- ( ( ( J e. Top /\ F e. V /\ Fun F ) /\ ( x e. ( J qTop ( F |` U. J ) ) /\ y e. ( J qTop ( F |` U. J ) ) ) ) -> ( ( `' ( F |` U. J ) " x ) i^i ( `' ( F |` U. J ) " y ) ) e. J )
54	48, 53	eqeltrd 2517	. . . . 5 |- ( ( ( J e. Top /\ F e. V /\ Fun F ) /\ ( x e. ( J qTop ( F |` U. J ) ) /\ y e. ( J qTop ( F |` U. J ) ) ) ) -> ( `' ( F |` U. J ) " ( x i^i y ) ) e. J )
55	1	elqtop 19292	. . . . . . 7 |- ( ( J e. Top /\ ( F |` U. J ) : dom ( F |` U. J ) -onto-> ran ( F |` U. J ) /\ dom ( F |` U. J ) C_ U. J ) -> ( ( x i^i y ) e. ( J qTop ( F |` U. J ) ) <-> ( ( x i^i y ) C_ ran ( F |` U. J ) /\ ( `' ( F |` U. J ) " ( x i^i y ) ) e. J ) ) )
56	4, 8, 12, 55	syl3anc 1218	. . . . . 6 |- ( ( J e. Top /\ F e. V /\ Fun F ) -> ( ( x i^i y ) e. ( J qTop ( F |` U. J ) ) <-> ( ( x i^i y ) C_ ran ( F |` U. J ) /\ ( `' ( F |` U. J ) " ( x i^i y ) ) e. J ) ) )
57	56	adantr 465	. . . . 5 |- ( ( ( J e. Top /\ F e. V /\ Fun F ) /\ ( x e. ( J qTop ( F |` U. J ) ) /\ y e. ( J qTop ( F |` U. J ) ) ) ) -> ( ( x i^i y ) e. ( J qTop ( F |` U. J ) ) <-> ( ( x i^i y ) C_ ran ( F |` U. J ) /\ ( `' ( F |` U. J ) " ( x i^i y ) ) e. J ) ) )
58	45, 54, 57	mpbir2and 913	. . . 4 |- ( ( ( J e. Top /\ F e. V /\ Fun F ) /\ ( x e. ( J qTop ( F |` U. J ) ) /\ y e. ( J qTop ( F |` U. J ) ) ) ) -> ( x i^i y ) e. ( J qTop ( F |` U. J ) ) )
59	58	ralrimivva 2829	. . 3 |- ( ( J e. Top /\ F e. V /\ Fun F ) -> A. x e. ( J qTop ( F |` U. J ) ) A. y e. ( J qTop ( F |` U. J ) ) ( x i^i y ) e. ( J qTop ( F |` U. J ) ) )
60		ovex 6137	. . . 4 |- ( J qTop ( F |` U. J ) ) e. _V
61		istopg 18530	. . . 4 |- ( ( J qTop ( F |` U. J ) ) e. _V -> ( ( J qTop ( F |` U. J ) ) e. Top <-> ( A. x ( x C_ ( J qTop ( F |` U. J ) ) -> U. x e. ( J qTop ( F |` U. J ) ) ) /\ A. x e. ( J qTop ( F |` U. J ) ) A. y e. ( J qTop ( F |` U. J ) ) ( x i^i y ) e. ( J qTop ( F |` U. J ) ) ) ) )
62	60, 61	ax-mp 5	. . 3 |- ( ( J qTop ( F |` U. J ) ) e. Top <-> ( A. x ( x C_ ( J qTop ( F |` U. J ) ) -> U. x e. ( J qTop ( F |` U. J ) ) ) /\ A. x e. ( J qTop ( F |` U. J ) ) A. y e. ( J qTop ( F |` U. J ) ) ( x i^i y ) e. ( J qTop ( F |` U. J ) ) ) )
63	38, 59, 62	sylanbrc 664	. 2 |- ( ( J e. Top /\ F e. V /\ Fun F ) -> ( J qTop ( F |` U. J ) ) e. Top )
64	3, 63	eqeltrd 2517	1 |- ( ( J e. Top /\ F e. V /\ Fun F ) -> ( J qTop F ) e. Top )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   /\ w3a 965   A.wal 1367   = wceq 1369   e. wcel 1756   A.wral 2736   _Vcvv 2993   i^i cin 3348   C_ wss 3349   ~Pcpw 3881   U.cuni 4112   U_ciun 4192   `'ccnv 4860   dom cdm 4861   ran crn 4862   |` cres 4863   "cima 4864   Fun wfun 5433   -onto->wfo 5437  (class class class)co 6112   qTop cqtop 14462   Topctop 18520

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-rep 4424  ax-sep 4434  ax-nul 4442  ax-pow 4491  ax-pr 4552  ax-un 6393

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-ral 2741  df-rex 2742  df-reu 2743  df-rab 2745  df-v 2995  df-sbc 3208  df-csb 3310  df-dif 3352  df-un 3354  df-in 3356  df-ss 3363  df-nul 3659  df-if 3813  df-pw 3883  df-sn 3899  df-pr 3901  df-op 3905  df-uni 4113  df-iun 4194  df-br 4314  df-opab 4372  df-mpt 4373  df-id 4657  df-xp 4867  df-rel 4868  df-cnv 4869  df-co 4870  df-dm 4871  df-rn 4872  df-res 4873  df-ima 4874  df-iota 5402  df-fun 5441  df-fn 5442  df-f 5443  df-f1 5444  df-fo 5445  df-f1o 5446  df-fv 5447  df-ov 6115  df-oprab 6116  df-mpt2 6117  df-qtop 14466  df-top 18525

This theorem is referenced by:  qtoptop  19295