Theorem subtop 7596

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 3541	. . . . . . . . . . . . 13 |- Fun {<.y, x>. | x = (y i^i Y)}
2		ssimaexg 3760	. . . . . . . . . . . . 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 902	. . . . . . . . . . . 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 3186	. . . . . . . . . . . . 13 |- ({<.y, x>. | x = (y i^i Y)}"J) = ran ({<.y, x>. | x = (y i^i Y)} |` J)
6		resopab 3387	. . . . . . . . . . . . . 14 |- ({<.y, x>. | x = (y i^i Y)} |` J) = {<.y, x>. | (y e. J /\ x = (y i^i Y))}
7	6	rneqi 3335	. . . . . . . . . . . . 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 1492	. . . . . . . . . . . 12 |- ({<.y, x>. | x = (y i^i Y)}"J) = ran {<.y, x>. | (y e. J /\ x = (y i^i Y))}
9	8	sseq2i 2082	. . . . . . . . . . 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 3186	. . . . . . . . . . . . . . 15 |- ({<.y, x>. | x = (y i^i Y)}"z) = ran ({<.y, x>. | x = (y i^i Y)} |` z)
11		resopab 3387	. . . . . . . . . . . . . . . 16 |- ({<.y, x>. | x = (y i^i Y)} |` z) = {<.y, x>. | (y e. z /\ x = (y i^i Y))}
12	11	rneqi 3335	. . . . . . . . . . . . . . 15 |- ran ({<.y, x>. | x = (y i^i Y)} |` z) = ran {<.y, x>. | (y e. z /\ x = (y i^i Y))}
13		rnopab2 3348	. . . . . . . . . . . . . . 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 1496	. . . . . . . . . . . . . 14 |- ({<.y, x>. | x = (y i^i Y)}"z) = {x | E.y e. z x = (y i^i Y)}
15	14	eqeq2i 1482	. . . . . . . . . . . . 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 1049	. . . . . . . . . . 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 551	. . . . . . . . . 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 3348	. . . . . . . . . . . 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 1476	. . . . . . . . . . 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 2082	. . . . . . . . . 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 2505	. . . . . . . . . . 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 2581	. . . . . . . . . . . . . 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 1477	. . . . . . . . . . . . 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 2713	. . . . . . . . . . . . 13 |- (y e. z -> (y i^i Y) e. V)
28	26, 27	mprg 1697	. . . . . . . . . . . 12 |- U.{x | E.y e. z x = (y i^i Y)} = U_y e. z (y i^i Y)
29		incom 2204	. . . . . . . . . . . . . 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 2575	. . . . . . . . . . . 12 |- U_y e. z (y i^i Y) = U_y e. z (Y i^i y)
32		iunin2 2603	. . . . . . . . . . . . 13 |- U_y e. z (Y i^i y) = (Y i^i U_y e. z y)
33		uniiun 2596	. . . . . . . . . . . . . 14 |- U.z = U_y e. z y
34	33	ineq2i 2210	. . . . . . . . . . . . 13 |- (Y i^i U.z) = (Y i^i U_y e. z y)
35		incom 2204	. . . . . . . . . . . . 13 |- (Y i^i U.z) = (U.z i^i Y)
36	32, 34, 35	3eqtr2 1498	. . . . . . . . . . . 12 |- U_y e. z (Y i^i y) = (U.z i^i Y)
37	28, 31, 36	3eqtr 1496	. . . . . . . . . . 11 |- U.{x | E.y e. z x = (y i^i Y)} = (U.z i^i Y)
38	24, 37	syl6eq 1520	. . . . . . . . . 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 1038	. . . . . . . 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 2745	. . . . . . . . . . . 12 |- {y} e. V
43		sseq1 2078	. . . . . . . . . . . . 13 |- (z = {y} -> (z (_ J <-> {y} (_ J))
44		unieq 2505	. . . . . . . . . . . . . . . 16 |- (z = {y} -> U.z = U.{y})
45		visset 1809	. . . . . . . . . . . . . . . . 17 |- y e. V
46	45	unisn 2512	. . . . . . . . . . . . . . . 16 |- U.{y} = y
47	44, 46	syl6eq 1520	. . . . . . . . . . . . . . 15 |- (z = {y} -> U.z = y)
48	47	ineq1d 2212	. . . . . . . . . . . . . 14 |- (z = {y} -> (U.z i^i Y) = (y i^i Y))
49	48	eqeq2d 1483	. . . . . . . . . . . . 13 |- (z = {y} -> (U.a = (U.z i^i Y) <-> U.a = (y i^i Y)))
50	43, 49	anbi12d 627	. . . . . . . . . . . 12 |- (z = {y} -> ((z (_ J /\ U.a = (U.z i^i Y)) <-> ({y} (_ J /\ U.a = (y i^i Y))))
51	42, 50	cla4ev 1865	. . . . . . . . . . 11 |- (({y} (_ J /\ U.a = (y i^i Y)) -> E.z(z (_ J /\ U.a = (U.z i^i Y)))
52		snssi 2462	. . . . . . . . . . 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 1741	. . . . . . . . 9 |- (E.y e. J U.a = (y i^i Y) -> E.z(z (_ J /\ U.a = (U.z i^i Y)))
55		uniopnt 7548	. . . . . . . . . . . . 13 |- ((J e. Top /\ z (_ J) -> U.z e. J)
56		ineq1 2206	. . . . . . . . . . . . . . . 16 |- (y = U.z -> (y i^i Y) = (U.z i^i Y))
57	56	eqeq2d 1483	. . . . . . . . . . . . . . 15 |- (y = U.z -> (U.a = (y i^i Y) <-> U.a = (U.z i^i Y)))
58	57	rcla4ev 1873	. . . . . . . . . . . . . 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 |- ((J