Theorem qusp 10430

Description: A quotient space is a topology.

Hypotheses

Ref	Expression
qusp.1	|- X = U.J
qusp.2	|- Er R

Assertion

Ref	Expression
qusp	|- (J e. Top -> {x | (x (_ (X/.R) /\ U.x e. J)} e. Top)

Distinct variable groups:   x,X   x,J   x,R

Proof of Theorem qusp

Step	Hyp	Ref	Expression
1		simplr 413	. . . . . . . . . . 11 |- (((J e. Top /\ U.y (_ (X/.R)) /\ A.x e. y U.x e. J) -> U.y (_ (X/.R))
2		uniopnt 7540	. . . . . . . . . . . . 13 |- ((J e. Top /\ {z | E.x(z = U.x /\ x e. y)} (_ J) -> U.{z | E.x(z = U.x /\ x e. y)} e. J)
3		simpll 412	. . . . . . . . . . . . 13 |- (((J e. Top /\ U.y (_ (X/.R)) /\ A.x e. y U.x e. J) -> J e. Top)
4		df-ral 1641	. . . . . . . . . . . . . . . 16 |- (A.x e. y U.x e. J <-> A.x(x e. y -> U.x e. J))
5		hba1 1000	. . . . . . . . . . . . . . . . . 18 |- (A.x(x e. y -> U.x e. J) -> A.xA.x(x e. y -> U.x e. J))
6		ax-17 968	. . . . . . . . . . . . . . . . . 18 |- (z e. J -> A.x z e. J)
7		eleq1a 1535	. . . . . . . . . . . . . . . . . . . . . 22 |- (U.x e. J -> (z = U.x -> z e. J))
8	7	imim2i 17	. . . . . . . . . . . . . . . . . . . . 21 |- ((x e. y -> U.x e. J) -> (x e. y -> (z = U.x -> z e. J)))
9	8	com23 32	. . . . . . . . . . . . . . . . . . . 20 |- ((x e. y -> U.x e. J) -> (z = U.x -> (x e. y -> z e. J)))
10	9	imp3a 361	. . . . . . . . . . . . . . . . . . 19 |- ((x e. y -> U.x e. J) -> ((z = U.x /\ x e. y) -> z e. J))
11	10	a4s 981	. . . . . . . . . . . . . . . . . 18 |- (A.x(x e. y -> U.x e. J) -> ((z = U.x /\ x e. y) -> z e. J))
12	5, 6, 11	19.23ad 1062	. . . . . . . . . . . . . . . . 17 |- (A.x(x e. y -> U.x e. J) -> (E.x(z = U.x /\ x e. y) -> z e. J))
13	12	19.21aiv 1281	. . . . . . . . . . . . . . . 16 |- (A.x(x e. y -> U.x e. J) -> A.z(E.x(z = U.x /\ x e. y) -> z e. J))
14	4, 13	sylbi 199	. . . . . . . . . . . . . . 15 |- (A.x e. y U.x e. J -> A.z(E.x(z = U.x /\ x e. y) -> z e. J))
15	14	adantl 388	. . . . . . . . . . . . . 14 |- (((J e. Top /\ U.y (_ (X/.R)) /\ A.x e. y U.x e. J) -> A.z(E.x(z = U.x /\ x e. y) -> z e. J))
16		abss 2107	. . . . . . . . . . . . . 14 |- ({z | E.x(z = U.x /\ x e. y)} (_ J <-> A.z(E.x(z = U.x /\ x e. y) -> z e. J))
17	15, 16	sylibr 200	. . . . . . . . . . . . 13 |- (((J e. Top /\ U.y (_ (X/.R)) /\ A.x e. y U.x e. J) -> {z | E.x(z = U.x /\ x e. y)} (_ J)
18	2, 3, 17	sylanc 471	. . . . . . . . . . . 12 |- (((J e. Top /\ U.y (_ (X/.R)) /\ A.x e. y U.x e. J) -> U.{z | E.x(z = U.x /\ x e. y)} e. J)
19		uniuni 2870	. . . . . . . . . . . 12 |- U.U.y = U.{z | E.x(z = U.x /\ x e. y)}
20	18, 19	syl5eqel 1544	. . . . . . . . . . 11 |- (((J e. Top /\ U.y (_ (X/.R)) /\ A.x e. y U.x e. J) -> U.U.y e. J)
21	1, 20	jca 288	. . . . . . . . . 10 |- (((J e. Top /\ U.y (_ (X/.R)) /\ A.x e. y U.x e. J) -> (U.y (_ (X/.R) /\ U.U.y e. J))
22	21	exp31 376	. . . . . . . . 9 |- (J e. Top -> (U.y (_ (X/.R) -> (A.x e. y U.x e. J -> (U.y (_ (X/.R) /\ U.U.y e. J))))
23		unissb 2518	. . . . . . . . 9 |- (U.y (_ (X/.R) <-> A.x e. y x (_ (X/.R))
24	22, 23	syl5ibr 207	. . . . . . . 8 |- (J e. Top -> (A.x e. y x (_ (X/.R) -> (A.x e. y U.x e. J -> (U.y (_ (X/.R) /\ U.U.y e. J))))
25	24	imp3a 361	. . . . . . 7 |- (J e. Top -> ((A.x e. y x (_ (X/.R) /\ A.x e. y U.x e. J) -> (U.y (_ (X/.R) /\ U.U.y e. J)))
26		r19.26 1742	. . . . . . 7 |- (A.x e. y (x (_ (X/.R) /\ U.x e. J) <-> (A.x e. y x (_ (X/.R) /\ A.x e. y U.x e. J))
27	25, 26	syl5ib 206	. . . . . 6 |- (J e. Top -> (A.x e. y (x (_ (X/.R) /\ U.x e. J) -> (U.y (_ (X/.R) /\ U.U.y e. J)))
28		df-ral 1641	. . . . . 6 |- (A.x e. y (x (_ (X/.R) /\ U.x e. J) <-> A.x(x e. y -> (x (_ (X/.R) /\ U.x e. J)))
29	27, 28	syl5ibr 207	. . . . 5 |- (J e. Top -> (A.x(x e. y -> (x (_ (X/.R) /\ U.x e. J)) -> (U.y (_ (X/.R) /\ U.U.y e. J)))
30		ssab 2108	. . . . 5 |- (y (_ {x | (x (_ (X/.R) /\ U.x e. J)} <-> A.x(x e. y -> (x (_ (X/.R) /\ U.x e. J)))
31		visset 1804	. . . . . . 7 |- y e. V
32	31	uniex 2861	. . . . . 6 |- U.y e. V
33		sseq1 2072	. . . . . . 7 |- (x = U.y -> (x (_ (X/.R) <-> U.y (_ (X/.R)))
34		unieq 2500	. . . . . . . 8 |- (x = U.y -> U.x = U.U.y)
35	34	eleq1d 1532	. . . . . . 7 |- (x = U.y -> (U.x e. J <-> U.U.y e. J))
36	33, 35	anbi12d 626	. . . . . 6 |- (x = U.y -> ((x (_ (X/.R) /\ U.x e. J) <-> (U.y (_ (X/.R) /\ U.U.y e. J)))
37	32, 36	elab 1888	. . . . 5 |- (U.y e. {x | (x (_ (X/.R) /\ U.x e. J)} <-> (U.y (_ (X/.R) /\ U.U.y e. J))
38	29, 30, 37	3imtr4g 551	. . . 4 |- (J e. Top -> (y (_ {x | (x (_ (X/.R) /\ U.x e. J)} -> U.y e. {x | (x (_ (X/.R) /\ U.x e. J)}))
39	38	19.21aiv 1281	. . 3 |- (J e. Top -> A.y(y (_ {x | (x (_ (X/.R) /\ U.x e. J)} -> U.y e. {x | (x (_ (X/.R) /\ U.x e. J)}))
40		ssinss1 2227	. . . . . . . . . . . . . . . 16 |- (y (_ (X/.R) -> (y i^i z) (_ (X/.R))
41	40	ad2antrr 404	. . . . . . . . . . . . . . 15 |- (((y (_ (X/.R) /\ z (_ (X/.R)) /\ (U.y e. J /\ U.z e. J)) -> (y i^i z) (_ (X/.R))
42	41	adantl 388	. . . . . . . . . . . . . 14 |- ((J e. Top /\ ((y (_ (X/.R) /\ z (_ (X/.R)) /\ (U.y e. J /\ U.z e. J))) -> (y i^i z) (_ (X/.R))
43		qusp.2	. . . . . . . . . . . . . . . . 17 |- Er R
44	43	uninqs 10342	. . . . . . . . . . . . . . . 16 |- ((y (_ (X/.R) /\ z (_ (X/.R)) -> U.(y i^i z) = (U.y i^i U.z))
45	44	ad2antrl 406	. . . . . . . . . . . . . . 15 |- ((J e. Top /\ ((y (_ (X/.R) /\ z (_ (X/.R)) /\ (U.y e. J /\ U.z e. J))) -> U.(y i^i z) = (U.y i^i U.z))
46		inopnt 7542	. . . . . . . . . . . . . . . . . . 19 |- ((J e. Top /\ U.y e. J /\ U.z e. J) -> (U.y i^i U.z) e. J)
47	46	3expib 834	. . . . . . . . . . . . . . . . . 18 |- (J e. Top -> ((U.y e. J /\ U.z e. J) -> (U.y i^i U.z) e. J))
48	47	com12 11	. . . . . . . . . . . . . . . . 17 |- ((U.y e. J /\ U.z e. J) -> (J e. Top -> (U.y i^i U.z) e. J))
49	48	adantl 388	. . . . . . . . . . . . . . . 16 |- (((y (_ (X/.R) /\ z (_ (X/.R)) /\ (U.y e. J /\ U.z e. J)) -> (J e. Top -> (U.y i^i U.z) e. J))
50	49	impcom 351	. . . . . . . . . . . . . . 15 |- ((J e. Top /\ ((y (_ (X/.R) /\ z (_ (X/.R)) /\ (U.y e. J /\ U.z e. J))) -> (U.y i^i U.z) e. J)
51	45, 50	eqeltrd 1540	. . . . . . . . . . . . . 14 |- ((J e. Top /\ ((y (_ (X/.R) /\ z (_ (X/.R)) /\ (U.y e. J /\ U.z e. J))) -> U.(y i^i z) e. J)
52	42, 51	jca 288	. . . . . . . . . . . . 13 |- ((J e. Top /\ ((y (_ (X/.R) /\ z (_ (X/.R)) /\ (U.y e. J /\ U.z e. J))) -> ((y i^i z) (_ (X/.R) /\ U.(y i^i z) e. J))
53	52	ex 373	. . . . . . . . . . . 12 |- (J e. Top -> (((y (_ (X/.R) /\ z (_ (X/.R)) /\ (U.y e. J /\ U.z e. J)) -> ((y i^i z) (_ (X/.R) /\ U.(y i^i z) e. J)))
54		an4 505	. . . . . . . . . . . 12 |- (((y (_ (X/.R) /\ U.y e. J) /\ (z (_ (X/.R) /\ U.z e. J)) <-> ((y (_ (X/.R) /\ z (_ (X/.R)) /\ (U.y e. J /\ U.