tgqtop

Description: An injection maps generated topologies to each other. (Contributed by Mario Carneiro, 27-Aug-2015)

		Ref	Expression
	Hypothesis	qtopcmp.1	$⊢ X = ⋃ J$
	Assertion	tgqtop	$⊢ (J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \to topGen (J) qTop F = topGen (J qTop F)$

Proof

Step	Hyp	Ref	Expression
1		qtopcmp.1	$⊢ X = ⋃ J$
2		f1ocnv	$⊢ F : X \underset{1-1 onto}{⟶} Y \to F^{-1} : Y \underset{1-1 onto}{⟶} X$
3		f1ofun	$⊢ F^{-1} : Y \underset{1-1 onto}{⟶} X \to Fun F^{-1}$
4	2 3	syl	$⊢ F : X \underset{1-1 onto}{⟶} Y \to Fun F^{-1}$
5	4	ad2antlr	$⊢ ((J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \land x \subseteq Y) \to Fun F^{-1}$
6		simpr	$⊢ ((J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \land x \subseteq Y) \to x \subseteq Y$
7		df-rn	$⊢ ran F = dom F^{-1}$
8		f1ofo	$⊢ F : X \underset{1-1 onto}{⟶} Y \to F : X \underset{onto}{⟶} Y$
9	8	ad2antlr	$⊢ ((J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \land x \subseteq Y) \to F : X \underset{onto}{⟶} Y$
10		forn	$⊢ F : X \underset{onto}{⟶} Y \to ran F = Y$
11	9 10	syl	$⊢ ((J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \land x \subseteq Y) \to ran F = Y$
12	7 11	eqtr3id	$⊢ ((J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \land x \subseteq Y) \to dom F^{-1} = Y$
13	6 12	sseqtrrd	$⊢ ((J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \land x \subseteq Y) \to x \subseteq dom F^{-1}$
14		funimass4	$⊢ (Fun F^{-1} \land x \subseteq dom F^{-1}) \to (F^{-1} [x] \subseteq ⋃ (J \cap 𝒫 F^{-1} [x]) \leftrightarrow \forall y \in x F^{-1} (y) \in ⋃ (J \cap 𝒫 F^{-1} [x]))$
15	5 13 14	syl2anc	$⊢ ((J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \land x \subseteq Y) \to (F^{-1} [x] \subseteq ⋃ (J \cap 𝒫 F^{-1} [x]) \leftrightarrow \forall y \in x F^{-1} (y) \in ⋃ (J \cap 𝒫 F^{-1} [x]))$
16		dfss3	$⊢ x \subseteq ⋃ ((J qTop F) \cap 𝒫 x) \leftrightarrow \forall y \in x y \in ⋃ ((J qTop F) \cap 𝒫 x)$
17		simprl	$⊢ ((((J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \land x \subseteq Y) \land y \in x) \land (z \in ((J qTop F) \cap 𝒫 x) \land y \in z)) \to z \in ((J qTop F) \cap 𝒫 x)$
18	17	elin1d	$⊢ ((((J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \land x \subseteq Y) \land y \in x) \land (z \in ((J qTop F) \cap 𝒫 x) \land y \in z)) \to z \in (J qTop F)$
19	1	elqtop2	$⊢ (J \in TopBases \land F : X \underset{onto}{⟶} Y) \to (z \in (J qTop F) \leftrightarrow (z \subseteq Y \land F^{-1} [z] \in J))$
20	8 19	sylan2	$⊢ (J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \to (z \in (J qTop F) \leftrightarrow (z \subseteq Y \land F^{-1} [z] \in J))$
21	20	ad3antrrr	$⊢ ((((J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \land x \subseteq Y) \land y \in x) \land (z \in ((J qTop F) \cap 𝒫 x) \land y \in z)) \to (z \in (J qTop F) \leftrightarrow (z \subseteq Y \land F^{-1} [z] \in J))$
22	18 21	mpbid	$⊢ ((((J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \land x \subseteq Y) \land y \in x) \land (z \in ((J qTop F) \cap 𝒫 x) \land y \in z)) \to (z \subseteq Y \land F^{-1} [z] \in J)$
23	22	simprd	$⊢ ((((J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \land x \subseteq Y) \land y \in x) \land (z \in ((J qTop F) \cap 𝒫 x) \land y \in z)) \to F^{-1} [z] \in J$
24	17	elin2d	$⊢ ((((J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \land x \subseteq Y) \land y \in x) \land (z \in ((J qTop F) \cap 𝒫 x) \land y \in z)) \to z \in 𝒫 x$
25	24	elpwid	$⊢ ((((J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \land x \subseteq Y) \land y \in x) \land (z \in ((J qTop F) \cap 𝒫 x) \land y \in z)) \to z \subseteq x$
26		imass2	$⊢ z \subseteq x \to F^{-1} [z] \subseteq F^{-1} [x]$
27	25 26	syl	$⊢ ((((J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \land x \subseteq Y) \land y \in x) \land (z \in ((J qTop F) \cap 𝒫 x) \land y \in z)) \to F^{-1} [z] \subseteq F^{-1} [x]$
28	23 27	elpwd	$⊢ ((((J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \land x \subseteq Y) \land y \in x) \land (z \in ((J qTop F) \cap 𝒫 x) \land y \in z)) \to F^{-1} [z] \in 𝒫 F^{-1} [x]$
29	23 28	elind	$⊢ ((((J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \land x \subseteq Y) \land y \in x) \land (z \in ((J qTop F) \cap 𝒫 x) \land y \in z)) \to F^{-1} [z] \in (J \cap 𝒫 F^{-1} [x])$
30		simp-4r	$⊢ ((((J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \land x \subseteq Y) \land y \in x) \land (z \in ((J qTop F) \cap 𝒫 x) \land y \in z)) \to F : X \underset{1-1 onto}{⟶} Y$
31	30 2	syl	$⊢ ((((J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \land x \subseteq Y) \land y \in x) \land (z \in ((J qTop F) \cap 𝒫 x) \land y \in z)) \to F^{-1} : Y \underset{1-1 onto}{⟶} X$
32		f1ofn	$⊢ F^{-1} : Y \underset{1-1 onto}{⟶} X \to F^{-1} Fn Y$
33	31 32	syl	$⊢ ((((J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \land x \subseteq Y) \land y \in x) \land (z \in ((J qTop F) \cap 𝒫 x) \land y \in z)) \to F^{-1} Fn Y$
34	6	ad2antrr	$⊢ ((((J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \land x \subseteq Y) \land y \in x) \land (z \in ((J qTop F) \cap 𝒫 x) \land y \in z)) \to x \subseteq Y$
35	25 34	sstrd	$⊢ ((((J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \land x \subseteq Y) \land y \in x) \land (z \in ((J qTop F) \cap 𝒫 x) \land y \in z)) \to z \subseteq Y$
36		simprr	$⊢ ((((J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \land x \subseteq Y) \land y \in x) \land (z \in ((J qTop F) \cap 𝒫 x) \land y \in z)) \to y \in z$
37		fnfvima	$⊢ (F^{-1} Fn Y \land z \subseteq Y \land y \in z) \to F^{-1} (y) \in F^{-1} [z]$
38	33 35 36 37	syl3anc	$⊢ ((((J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \land x \subseteq Y) \land y \in x) \land (z \in ((J qTop F) \cap 𝒫 x) \land y \in z)) \to F^{-1} (y) \in F^{-1} [z]$
39		eleq2	$⊢ w = F^{-1} [z] \to (F^{-1} (y) \in w \leftrightarrow F^{-1} (y) \in F^{-1} [z])$
40	39	rspcev	$⊢ (F^{-1} [z] \in (J \cap 𝒫 F^{-1} [x]) \land F^{-1} (y) \in F^{-1} [z]) \to \exists w \in (J \cap 𝒫 F^{-1} [x]) F^{-1} (y) \in w$
41	29 38 40	syl2anc	$⊢ ((((J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \land x \subseteq Y) \land y \in x) \land (z \in ((J qTop F) \cap 𝒫 x) \land y \in z)) \to \exists w \in (J \cap 𝒫 F^{-1} [x]) F^{-1} (y) \in w$
42	41	rexlimdvaa	$⊢ (((J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \land x \subseteq Y) \land y \in x) \to (\exists z \in ((J qTop F) \cap 𝒫 x) y \in z \to \exists w \in (J \cap 𝒫 F^{-1} [x]) F^{-1} (y) \in w)$
43		simp-4r	$⊢ ((((J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \land x \subseteq Y) \land y \in x) \land (w \in (J \cap 𝒫 F^{-1} [x]) \land F^{-1} (y) \in w)) \to F : X \underset{1-1 onto}{⟶} Y$
44		f1ofun	$⊢ F : X \underset{1-1 onto}{⟶} Y \to Fun F$
45	43 44	syl	$⊢ ((((J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \land x \subseteq Y) \land y \in x) \land (w \in (J \cap 𝒫 F^{-1} [x]) \land F^{-1} (y) \in w)) \to Fun F$
46		simprl	$⊢ ((((J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \land x \subseteq Y) \land y \in x) \land (w \in (J \cap 𝒫 F^{-1} [x]) \land F^{-1} (y) \in w)) \to w \in (J \cap 𝒫 F^{-1} [x])$
47	46	elin2d	$⊢ ((((J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \land x \subseteq Y) \land y \in x) \land (w \in (J \cap 𝒫 F^{-1} [x]) \land F^{-1} (y) \in w)) \to w \in 𝒫 F^{-1} [x]$
48	47	elpwid	$⊢ ((((J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \land x \subseteq Y) \land y \in x) \land (w \in (J \cap 𝒫 F^{-1} [x]) \land F^{-1} (y) \in w)) \to w \subseteq F^{-1} [x]$
49		funimass2	$⊢ (Fun F \land w \subseteq F^{-1} [x]) \to F [w] \subseteq x$
50	45 48 49	syl2anc	$⊢ ((((J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \land x \subseteq Y) \land y \in x) \land (w \in (J \cap 𝒫 F^{-1} [x]) \land F^{-1} (y) \in w)) \to F [w] \subseteq x$
51	6	ad2antrr	$⊢ ((((J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \land x \subseteq Y) \land y \in x) \land (w \in (J \cap 𝒫 F^{-1} [x]) \land F^{-1} (y) \in w)) \to x \subseteq Y$
52	50 51	sstrd	$⊢ ((((J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \land x \subseteq Y) \land y \in x) \land (w \in (J \cap 𝒫 F^{-1} [x]) \land F^{-1} (y) \in w)) \to F [w] \subseteq Y$
53		f1of1	$⊢ F : X \underset{1-1 onto}{⟶} Y \to F : X \underset{1-1}{⟶} Y$
54	43 53	syl	$⊢ ((((J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \land x \subseteq Y) \land y \in x) \land (w \in (J \cap 𝒫 F^{-1} [x]) \land F^{-1} (y) \in w)) \to F : X \underset{1-1}{⟶} Y$
55	46	elin1d	$⊢ ((((J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \land x \subseteq Y) \land y \in x) \land (w \in (J \cap 𝒫 F^{-1} [x]) \land F^{-1} (y) \in w)) \to w \in J$
56		elssuni	$⊢ w \in J \to w \subseteq ⋃ J$
57	56 1	sseqtrrdi	$⊢ w \in J \to w \subseteq X$
58	55 57	syl	$⊢ ((((J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \land x \subseteq Y) \land y \in x) \land (w \in (J \cap 𝒫 F^{-1} [x]) \land F^{-1} (y) \in w)) \to w \subseteq X$
59		f1imacnv	$⊢ (F : X \underset{1-1}{⟶} Y \land w \subseteq X) \to F^{-1} [F [w]] = w$
60	54 58 59	syl2anc	$⊢ ((((J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \land x \subseteq Y) \land y \in x) \land (w \in (J \cap 𝒫 F^{-1} [x]) \land F^{-1} (y) \in w)) \to F^{-1} [F [w]] = w$
61	60 55	eqeltrd	$⊢ ((((J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \land x \subseteq Y) \land y \in x) \land (w \in (J \cap 𝒫 F^{-1} [x]) \land F^{-1} (y) \in w)) \to F^{-1} [F [w]] \in J$
62	1	elqtop2	$⊢ (J \in TopBases \land F : X \underset{onto}{⟶} Y) \to (F [w] \in (J qTop F) \leftrightarrow (F [w] \subseteq Y \land F^{-1} [F [w]] \in J))$
63	8 62	sylan2	$⊢ (J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \to (F [w] \in (J qTop F) \leftrightarrow (F [w] \subseteq Y \land F^{-1} [F [w]] \in J))$
64	63	ad3antrrr	$⊢ ((((J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \land x \subseteq Y) \land y \in x) \land (w \in (J \cap 𝒫 F^{-1} [x]) \land F^{-1} (y) \in w)) \to (F [w] \in (J qTop F) \leftrightarrow (F [w] \subseteq Y \land F^{-1} [F [w]] \in J))$
65	52 61 64	mpbir2and	$⊢ ((((J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \land x \subseteq Y) \land y \in x) \land (w \in (J \cap 𝒫 F^{-1} [x]) \land F^{-1} (y) \in w)) \to F [w] \in (J qTop F)$
66		vex	$⊢ x \in V$
67	66	elpw2	$⊢ F [w] \in 𝒫 x \leftrightarrow F [w] \subseteq x$
68	50 67	sylibr	$⊢ ((((J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \land x \subseteq Y) \land y \in x) \land (w \in (J \cap 𝒫 F^{-1} [x]) \land F^{-1} (y) \in w)) \to F [w] \in 𝒫 x$
69	65 68	elind	$⊢ ((((J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \land x \subseteq Y) \land y \in x) \land (w \in (J \cap 𝒫 F^{-1} [x]) \land F^{-1} (y) \in w)) \to F [w] \in ((J qTop F) \cap 𝒫 x)$
70	6	sselda	$⊢ (((J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \land x \subseteq Y) \land y \in x) \to y \in Y$
71	70	adantr	$⊢ ((((J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \land x \subseteq Y) \land y \in x) \land (w \in (J \cap 𝒫 F^{-1} [x]) \land F^{-1} (y) \in w)) \to y \in Y$
72		f1ocnvfv2	$⊢ (F : X \underset{1-1 onto}{⟶} Y \land y \in Y) \to F (F^{-1} (y)) = y$
73	43 71 72	syl2anc	$⊢ ((((J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \land x \subseteq Y) \land y \in x) \land (w \in (J \cap 𝒫 F^{-1} [x]) \land F^{-1} (y) \in w)) \to F (F^{-1} (y)) = y$
74		f1ofn	$⊢ F : X \underset{1-1 onto}{⟶} Y \to F Fn X$
75	74	adantl	$⊢ (J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \to F Fn X$
76	75	ad3antrrr	$⊢ ((((J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \land x \subseteq Y) \land y \in x) \land (w \in (J \cap 𝒫 F^{-1} [x]) \land F^{-1} (y) \in w)) \to F Fn X$
77		simprr	$⊢ ((((J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \land x \subseteq Y) \land y \in x) \land (w \in (J \cap 𝒫 F^{-1} [x]) \land F^{-1} (y) \in w)) \to F^{-1} (y) \in w$
78		fnfvima	$⊢ (F Fn X \land w \subseteq X \land F^{-1} (y) \in w) \to F (F^{-1} (y)) \in F [w]$
79	76 58 77 78	syl3anc	$⊢ ((((J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \land x \subseteq Y) \land y \in x) \land (w \in (J \cap 𝒫 F^{-1} [x]) \land F^{-1} (y) \in w)) \to F (F^{-1} (y)) \in F [w]$
80	73 79	eqeltrrd	$⊢ ((((J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \land x \subseteq Y) \land y \in x) \land (w \in (J \cap 𝒫 F^{-1} [x]) \land F^{-1} (y) \in w)) \to y \in F [w]$
81		eleq2	$⊢ z = F [w] \to (y \in z \leftrightarrow y \in F [w])$
82	81	rspcev	$⊢ (F [w] \in ((J qTop F) \cap 𝒫 x) \land y \in F [w]) \to \exists z \in ((J qTop F) \cap 𝒫 x) y \in z$
83	69 80 82	syl2anc	$⊢ ((((J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \land x \subseteq Y) \land y \in x) \land (w \in (J \cap 𝒫 F^{-1} [x]) \land F^{-1} (y) \in w)) \to \exists z \in ((J qTop F) \cap 𝒫 x) y \in z$
84	83	rexlimdvaa	$⊢ (((J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \land x \subseteq Y) \land y \in x) \to (\exists w \in (J \cap 𝒫 F^{-1} [x]) F^{-1} (y) \in w \to \exists z \in ((J qTop F) \cap 𝒫 x) y \in z)$
85	42 84	impbid	$⊢ (((J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \land x \subseteq Y) \land y \in x) \to (\exists z \in ((J qTop F) \cap 𝒫 x) y \in z \leftrightarrow \exists w \in (J \cap 𝒫 F^{-1} [x]) F^{-1} (y) \in w)$
86		eluni2	$⊢ y \in ⋃ ((J qTop F) \cap 𝒫 x) \leftrightarrow \exists z \in ((J qTop F) \cap 𝒫 x) y \in z$
87		eluni2	$⊢ F^{-1} (y) \in ⋃ (J \cap 𝒫 F^{-1} [x]) \leftrightarrow \exists w \in (J \cap 𝒫 F^{-1} [x]) F^{-1} (y) \in w$
88	85 86 87	3bitr4g	$⊢ (((J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \land x \subseteq Y) \land y \in x) \to (y \in ⋃ ((J qTop F) \cap 𝒫 x) \leftrightarrow F^{-1} (y) \in ⋃ (J \cap 𝒫 F^{-1} [x]))$
89	88	ralbidva	$⊢ ((J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \land x \subseteq Y) \to (\forall y \in x y \in ⋃ ((J qTop F) \cap 𝒫 x) \leftrightarrow \forall y \in x F^{-1} (y) \in ⋃ (J \cap 𝒫 F^{-1} [x]))$
90	16 89	bitrid	$⊢ ((J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \land x \subseteq Y) \to (x \subseteq ⋃ ((J qTop F) \cap 𝒫 x) \leftrightarrow \forall y \in x F^{-1} (y) \in ⋃ (J \cap 𝒫 F^{-1} [x]))$
91	15 90	bitr4d	$⊢ ((J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \land x \subseteq Y) \to (F^{-1} [x] \subseteq ⋃ (J \cap 𝒫 F^{-1} [x]) \leftrightarrow x \subseteq ⋃ ((J qTop F) \cap 𝒫 x))$
92		eltg	$⊢ J \in TopBases \to (F^{-1} [x] \in topGen (J) \leftrightarrow F^{-1} [x] \subseteq ⋃ (J \cap 𝒫 F^{-1} [x]))$
93	92	ad2antrr	$⊢ ((J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \land x \subseteq Y) \to (F^{-1} [x] \in topGen (J) \leftrightarrow F^{-1} [x] \subseteq ⋃ (J \cap 𝒫 F^{-1} [x]))$
94		ovex	$⊢ J qTop F \in V$
95		eltg	$⊢ J qTop F \in V \to (x \in topGen (J qTop F) \leftrightarrow x \subseteq ⋃ ((J qTop F) \cap 𝒫 x))$
96	94 95	mp1i	$⊢ ((J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \land x \subseteq Y) \to (x \in topGen (J qTop F) \leftrightarrow x \subseteq ⋃ ((J qTop F) \cap 𝒫 x))$
97	91 93 96	3bitr4d	$⊢ ((J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \land x \subseteq Y) \to (F^{-1} [x] \in topGen (J) \leftrightarrow x \in topGen (J qTop F))$
98	97	pm5.32da	$⊢ (J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \to ((x \subseteq Y \land F^{-1} [x] \in topGen (J)) \leftrightarrow (x \subseteq Y \land x \in topGen (J qTop F)))$
99		tgtopon	$⊢ J \in TopBases \to topGen (J) \in TopOn (⋃ J)$
100	99	adantr	$⊢ (J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \to topGen (J) \in TopOn (⋃ J)$
101	1	fveq2i	$⊢ TopOn (X) = TopOn (⋃ J)$
102	100 101	eleqtrrdi	$⊢ (J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \to topGen (J) \in TopOn (X)$
103	8	adantl	$⊢ (J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \to F : X \underset{onto}{⟶} Y$
104		elqtop3	$⊢ (topGen (J) \in TopOn (X) \land F : X \underset{onto}{⟶} Y) \to (x \in (topGen (J) qTop F) \leftrightarrow (x \subseteq Y \land F^{-1} [x] \in topGen (J)))$
105	102 103 104	syl2anc	$⊢ (J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \to (x \in (topGen (J) qTop F) \leftrightarrow (x \subseteq Y \land F^{-1} [x] \in topGen (J)))$
106		unitg	$⊢ J qTop F \in V \to ⋃ topGen (J qTop F) = ⋃ (J qTop F)$
107	94 106	ax-mp	$⊢ ⋃ topGen (J qTop F) = ⋃ (J qTop F)$
108	1	elqtop2	$⊢ (J \in TopBases \land F : X \underset{onto}{⟶} Y) \to (x \in (J qTop F) \leftrightarrow (x \subseteq Y \land F^{-1} [x] \in J))$
109	8 108	sylan2	$⊢ (J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \to (x \in (J qTop F) \leftrightarrow (x \subseteq Y \land F^{-1} [x] \in J))$
110		simpl	$⊢ (x \subseteq Y \land F^{-1} [x] \in J) \to x \subseteq Y$
111		velpw	$⊢ x \in 𝒫 Y \leftrightarrow x \subseteq Y$
112	110 111	sylibr	$⊢ (x \subseteq Y \land F^{-1} [x] \in J) \to x \in 𝒫 Y$
113	109 112	biimtrdi	$⊢ (J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \to (x \in (J qTop F) \to x \in 𝒫 Y)$
114	113	ssrdv	$⊢ (J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \to J qTop F \subseteq 𝒫 Y$
115		sspwuni	$⊢ J qTop F \subseteq 𝒫 Y \leftrightarrow ⋃ (J qTop F) \subseteq Y$
116	114 115	sylib	$⊢ (J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \to ⋃ (J qTop F) \subseteq Y$
117	107 116	eqsstrid	$⊢ (J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \to ⋃ topGen (J qTop F) \subseteq Y$
118		sspwuni	$⊢ topGen (J qTop F) \subseteq 𝒫 Y \leftrightarrow ⋃ topGen (J qTop F) \subseteq Y$
119	117 118	sylibr	$⊢ (J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \to topGen (J qTop F) \subseteq 𝒫 Y$
120	119	sseld	$⊢ (J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \to (x \in topGen (J qTop F) \to x \in 𝒫 Y)$
121	120 111	imbitrdi	$⊢ (J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \to (x \in topGen (J qTop F) \to x \subseteq Y)$
122	121	pm4.71rd	$⊢ (J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \to (x \in topGen (J qTop F) \leftrightarrow (x \subseteq Y \land x \in topGen (J qTop F)))$
123	98 105 122	3bitr4d	$⊢ (J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \to (x \in (topGen (J) qTop F) \leftrightarrow x \in topGen (J qTop F))$
124	123	eqrdv	$⊢ (J \in TopBases \land F : X \underset{1-1 onto}{⟶} Y) \to topGen (J) qTop F = topGen (J qTop F)$

Metamath Proof Explorer

Theorem tgqtop

Proof