Theorem subtop 7646

Description: A subspace topology is a topology. Definition of subspace topology in [Munkres] p. 89. Y is normally a subset of the base set of J. (Contributed by FL, 15-Apr-2007.)

Assertion

Ref	Expression
subtop	|- (J e. Top -> {x | E.y e. J x = (y i^i Y)} e. Top)

Distinct variable group:   J,Y,x,y

Proof of Theorem subtop

Step	Hyp	Ref	Expression
1		funopabeq 3549	. . . . . . . . . . . . 13 |- Fun {<.y, x>. | x = (y i^i Y)}
2		ssimaexg 3769	. . . . . . . . . . . . 13 |- ((J e. Top /\ Fun {<.y, x>. | x = (y i^i Y)} /\ a (_ ({<.y, x>. | x = (y i^i Y)}"J)) -> E.z(z (_ J /\ a = ({<.y, x>. | x = (y i^i Y)}"z)))
3	1, 2	mp3an2 904	. . . . . . . . . . . 12 |- ((J e. Top /\ a (_ ({<.y, x>. | x = (y i^i Y)}"J)) -> E.z(z (_ J /\ a = ({<.y, x>. | x = (y i^i Y)}"z)))
4	3	ex 373	. . . . . . . . . . 11 |- (J e. Top -> (a (_ ({<.y, x>. | x = (y i^i Y)}"J) -> E.z(z (_ J /\ a = ({<.y, x>. | x = (y i^i Y)}"z))))
5		df-ima 3191	. . . . . . . . . . . . 13 |- ({<.y, x>. | x = (y i^i Y)}"J) = ran ({<.y, x>. | x = (y i^i Y)} |` J)
6		resopab 3395	. . . . . . . . . . . . . 14 |- ({<.y, x>. | x = (y i^i Y)} |` J) = {<.y, x>. | (y e. J /\ x = (y i^i Y))}
7	6	rneqi 3340	. . . . . . . . . . . . 13 |- ran ({<.y, x>. | x = (y i^i Y)} |` J) = ran {<.y, x>. | (y e. J /\ x = (y i^i Y))}
8	5, 7	eqtr 1495	. . . . . . . . . . . 12 |- ({<.y, x>. | x = (y i^i Y)}"J) = ran {<.y, x>. | (y e. J /\ x = (y i^i Y))}
9	8	sseq2i 2086	. . . . . . . . . . 11 |- (a (_ ({<.y, x>. | x = (y i^i Y)}"J) <-> a (_ ran {<.y, x>. | (y e. J /\ x = (y i^i Y))})
10		df-ima 3191	. . . . . . . . . . . . . . 15 |- ({<.y, x>. | x = (y i^i Y)}"z) = ran ({<.y, x>. | x = (y i^i Y)} |` z)
11		resopab 3395	. . . . . . . . . . . . . . . 16 |- ({<.y, x>. | x = (y i^i Y)} |` z) = {<.y, x>. | (y e. z /\ x = (y i^i Y))}
12	11	rneqi 3340	. . . . . . . . . . . . . . 15 |- ran ({<.y, x>. | x = (y i^i Y)} |` z) = ran {<.y, x>. | (y e. z /\ x = (y i^i Y))}
13		rnopab2 3354	. . . . . . . . . . . . . . 15 |- ran {<.y, x>. | (y e. z /\ x = (y i^i Y))} = {x | E.y e. z x = (y i^i Y)}
14	10, 12, 13	3eqtr 1499	. . . . . . . . . . . . . 14 |- ({<.y, x>. | x = (y i^i Y)}"z) = {x | E.y e. z x = (y i^i Y)}
15	14	eqeq2i 1485	. . . . . . . . . . . . 13 |- (a = ({<.y, x>. | x = (y i^i Y)}"z) <-> a = {x | E.y e. z x = (y i^i Y)})
16	15	anbi2i 480	. . . . . . . . . . . 12 |- ((z (_ J /\ a = ({<.y, x>. | x = (y i^i Y)}"z)) <-> (z (_ J /\ a = {x | E.y e. z x = (y i^i Y)}))
17	16	exbii 1051	. . . . . . . . . . 11 |- (E.z(z (_ J /\ a = ({<.y, x>. | x = (y i^i Y)}"z)) <-> E.z(z (_ J /\ a = {x | E.y e. z x = (y i^i Y)}))
18	4, 9, 17	3imtr3g 552	. . . . . . . . . 10 |- (J e. Top -> (a (_ ran {<.y, x>. | (y e. J /\ x = (y i^i Y))} -> E.z(z (_ J /\ a = {x | E.y e. z x = (y i^i Y)})))
19		rnopab2 3354	. . . . . . . . . . . 12 |- ran {<.y, x>. | (y e. J /\ x = (y i^i Y))} = {x | E.y e. J x = (y i^i Y)}
20	19	eqcomi 1479	. . . . . . . . . . 11 |- {x | E.y e. J x = (y i^i Y)} = ran {<.y, x>. | (y e. J /\ x = (y i^i Y))}
21	20	sseq2i 2086	. . . . . . . . . 10 |- (a (_ {x | E.y e. J x = (y i^i Y)} <-> a (_ ran {<.y, x>. | (y e. J /\ x = (y i^i Y))})
22	18, 21	syl5ib 206	. . . . . . . . 9 |- (J e. Top -> (a (_ {x | E.y e. J x = (y i^i Y)} -> E.z(z (_ J /\ a = {x | E.y e. z x = (y i^i Y)})))
23	22	imp 350	. . . . . . . 8 |- ((J e. Top /\ a (_ {x | E.y e. J x = (y i^i Y)}) -> E.z(z (_ J /\ a = {x | E.y e. z x = (y i^i Y)}))
24		unieq 2510	. . . . . . . . . . 11 |- (a = {x | E.y e. z x = (y i^i Y)} -> U.a = U.{x | E.y e. z x = (y i^i Y)})
25		dfiun2g 2586	. . . . . . . . . . . . . 14 |- (A.y e. z (y i^i Y) e. V -> U_y e. z (y i^i Y) = U.{x | E.y e. z x = (y i^i Y)})
26	25	eqcomd 1480	. . . . . . . . . . . . 13 |- (A.y e. z (y i^i Y) e. V -> U.{x | E.y e. z x = (y i^i Y)} = U_y e. z (y i^i Y))
27		inex1g 2718	. . . . . . . . . . . . 13 |- (y e. z -> (y i^i Y) e. V)
28	26, 27	mprg 1700	. . . . . . . . . . . 12 |- U.{x | E.y e. z x = (y i^i Y)} = U_y e. z (y i^i Y)
29		incom 2208	. . . . . . . . . . . . . 14 |- (y i^i Y) = (Y i^i y)
30	29	a1i 8	. . . . . . . . . . . . 13 |- (y e. z -> (y i^i Y) = (Y i^i y))
31	30	iuneq2i 2580	. . . . . . . . . . . 12 |- U_y e. z (y i^i Y) = U_y e. z (Y i^i y)
32		iunin2 2608	. . . . . . . . . . . . 13 |- U_y e. z (Y i^i y) = (Y i^i U_y e. z y)
33		uniiun 2601	. . . . . . . . . . . . . 14 |- U.z = U_y e. z y
34	33	ineq2i 2214	. . . . . . . . . . . . 13 |- (Y i^i U.z) = (Y i^i U_y e. z y)
35		incom 2208	. . . . . . . . . . . . 13 |- (Y i^i U.z) = (U.z i^i Y)
36	32, 34, 35	3eqtr2 1501	. . . . . . . . . . . 12 |- U_y e. z (Y i^i y) = (U.z i^i Y)
37	28, 31, 36	3eqtr 1499	. . . . . . . . . . 11 |- U.{x | E.y e. z x = (y i^i Y)} = (U.z i^i Y)
38	24, 37	syl6eq 1523	. . . . . . . . . 10 |- (a = {x | E.y e. z x = (y i^i Y)} -> U.a = (U.z i^i Y))
39	38	anim2i 335	. . . . . . . . 9 |- ((z (_ J /\ a = {x | E.y e. z x = (y i^i Y)}) -> (z (_ J /\ U.a = (U.z i^i Y)))
40	39	19.22i 1040	. . . . . . . 8 |- (E.z(z (_ J /\ a = {x | E.y e. z x = (y i^i Y)}) -> E.z(z (_ J /\ U.a = (U.z i^i Y)))
41	23, 40	syl 10	. . . . . . 7 |- ((J e. Top /\ a (_ {x | E.y e. J x = (y i^i Y)}) -> E.z(z (_ J /\ U.a = (U.z i^i Y)))
42		snex 2750	. . . . . . . . . . . 12 |- {y} e. V
43		sseq1 2082	. . . . . . . . . . . . 13 |- (z = {y} -> (z (_ J <-> {y} (_ J))
44		unieq 2510	. . . . . . . . . . . . . . . 16 |- (z = {y} -> U.z = U.{y})
45		visset 1813	. . . . . . . . . . . . . . . . 17 |- y e. V
46	45	unisn 2517	. . . . . . . . . . . . . . . 16 |- U.{y} = y
47	44, 46	syl6eq 1523	. . . . . . . . . . . . . . 15 |- (z = {y} -> U.z = y)
48	47	ineq1d 2216	. . . . . . . . . . . . . 14 |- (z = {y} -> (U.z i^i Y) = (y i^i Y))
49	48	eqeq2d 1486	. . . . . . . . . . . . 13 |- (z = {y} -> (U.a = (U.z i^i Y) <-> U.a = (y i^i Y)))
50	43, 49	anbi12d 628	. . . . . . . . . . . 12 |- (z = {y} -> ((z (_ J /\ U.a = (U.z i^i Y)) <-> ({y} (_ J /\ U.a = (y i^i Y))))
51	42, 50	cla4ev 1869	. . . . . . . . . . 11 |- (({y} (_ J /\ U.a = (y i^i Y)) -> E.z(z (_ J /\ U.a = (U.z i^i Y)))
52		snssi 2466	. . . . . . . . . . 11 |- (y e. J -> {y} (_ J)
53	51, 52	sylan 448	. . . . . . . . . 10 |- ((y e. J /\ U.a = (y i^i Y)) -> E.z(z (_ J /\ U.a = (U.z i^i Y)))
54	53	r19.23aiva 1744	. . . . . . . . 9 |- (E.y e. J U.a = (y i^i Y) -> E.z(z (_ J /\ U.a = (U.z i^i Y)))
55		uniopnt 7598	. . . . . . . . . . . . 13 |- ((J e. Top /\ z (_ J) -> U.z e. J)
56		ineq1 2210	. . . . . . . . . . . . . . . 16 |- (y = U.z -> (y i^i Y) = (U.z i^i Y))
57	56	eqeq2d 1486	. . . . . . . . . . . . . . 15 |- (y = U.z -> (U.a = (y i^i Y) <-> U.a = (U.z i^i Y)))
58	57	rcla4ev 1877	. . . . . . . . . . . . . 14 |- ((U.z e. J /\ U.a = (U.z i^i Y)) -> E.y e. J U.a = (y i^i Y))
59	58	ex 373	. . . . . . . . . . . . 13 |- (U.z e. J -> (U.a = (U.z i^i Y) -> E.y e. J U.a = (y i^i Y)))
60	55, 59	syl 10	. . . . . . . . . . . 12 |- (