qtoptop2

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

		Ref	Expression
	Assertion	qtoptop2	$⊢ (J \in Top \land F \in V \land Fun F) \to J qTop F \in Top$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ ⋃ J = ⋃ J$
2	1	qtopres	$⊢ F \in V \to J qTop F = J qTop ({F ↾}_{⋃ J})$
3	2	3ad2ant2	$⊢ (J \in Top \land F \in V \land Fun F) \to J qTop F = J qTop ({F ↾}_{⋃ J})$
4		simp1	$⊢ (J \in Top \land F \in V \land Fun F) \to J \in Top$
5		funres	$⊢ Fun F \to Fun ({F ↾}_{⋃ J})$
6	5	3ad2ant3	$⊢ (J \in Top \land F \in V \land Fun F) \to Fun ({F ↾}_{⋃ J})$
7		funforn	$⊢ Fun ({F ↾}_{⋃ J}) \leftrightarrow ({F ↾}_{⋃ J}) : dom ({F ↾}_{⋃ J}) \underset{onto}{⟶} ran ({F ↾}_{⋃ J})$
8	6 7	sylib	$⊢ (J \in Top \land F \in V \land Fun F) \to ({F ↾}_{⋃ J}) : dom ({F ↾}_{⋃ J}) \underset{onto}{⟶} ran ({F ↾}_{⋃ J})$
9		dmres	$⊢ dom ({F ↾}_{⋃ J}) = ⋃ J \cap dom F$
10		inss1	$⊢ ⋃ J \cap dom F \subseteq ⋃ J$
11	9 10	eqsstri	$⊢ dom ({F ↾}_{⋃ J}) \subseteq ⋃ J$
12	11	a1i	$⊢ (J \in Top \land F \in V \land Fun F) \to dom ({F ↾}_{⋃ J}) \subseteq ⋃ J$
13	1	elqtop	$⊢ (J \in Top \land ({F ↾}_{⋃ J}) : dom ({F ↾}_{⋃ J}) \underset{onto}{⟶} ran ({F ↾}_{⋃ J}) \land dom ({F ↾}_{⋃ J}) \subseteq ⋃ J) \to (y \in (J qTop ({F ↾}_{⋃ J})) \leftrightarrow (y \subseteq ran ({F ↾}_{⋃ J}) \land {({F ↾}_{⋃ J})}^{-1} [y] \in J))$
14	4 8 12 13	syl3anc	$⊢ (J \in Top \land F \in V \land Fun F) \to (y \in (J qTop ({F ↾}_{⋃ J})) \leftrightarrow (y \subseteq ran ({F ↾}_{⋃ J}) \land {({F ↾}_{⋃ J})}^{-1} [y] \in J))$
15	14	simprbda	$⊢ ((J \in Top \land F \in V \land Fun F) \land y \in (J qTop ({F ↾}_{⋃ J}))) \to y \subseteq ran ({F ↾}_{⋃ J})$
16		velpw	$⊢ y \in 𝒫 ran ({F ↾}_{⋃ J}) \leftrightarrow y \subseteq ran ({F ↾}_{⋃ J})$
17	15 16	sylibr	$⊢ ((J \in Top \land F \in V \land Fun F) \land y \in (J qTop ({F ↾}_{⋃ J}))) \to y \in 𝒫 ran ({F ↾}_{⋃ J})$
18	17	ex	$⊢ (J \in Top \land F \in V \land Fun F) \to (y \in (J qTop ({F ↾}_{⋃ J})) \to y \in 𝒫 ran ({F ↾}_{⋃ J}))$
19	18	ssrdv	$⊢ (J \in Top \land F \in V \land Fun F) \to J qTop ({F ↾}_{⋃ J}) \subseteq 𝒫 ran ({F ↾}_{⋃ J})$
20		sstr2	$⊢ x \subseteq J qTop ({F ↾}_{⋃ J}) \to (J qTop ({F ↾}_{⋃ J}) \subseteq 𝒫 ran ({F ↾}_{⋃ J}) \to x \subseteq 𝒫 ran ({F ↾}_{⋃ J}))$
21	19 20	syl5com	$⊢ (J \in Top \land F \in V \land Fun F) \to (x \subseteq J qTop ({F ↾}_{⋃ J}) \to x \subseteq 𝒫 ran ({F ↾}_{⋃ J}))$
22		sspwuni	$⊢ x \subseteq 𝒫 ran ({F ↾}_{⋃ J}) \leftrightarrow ⋃ x \subseteq ran ({F ↾}_{⋃ J})$
23	21 22	syl6ib	$⊢ (J \in Top \land F \in V \land Fun F) \to (x \subseteq J qTop ({F ↾}_{⋃ J}) \to ⋃ x \subseteq ran ({F ↾}_{⋃ J}))$
24		imauni	$⊢ {({F ↾}_{⋃ J})}^{-1} [⋃ x] = ⋃_{y \in x} {({F ↾}_{⋃ J})}^{-1} [y]$
25	14	simplbda	$⊢ ((J \in Top \land F \in V \land Fun F) \land y \in (J qTop ({F ↾}_{⋃ J}))) \to {({F ↾}_{⋃ J})}^{-1} [y] \in J$
26	25	ralrimiva	$⊢ (J \in Top \land F \in V \land Fun F) \to \forall y \in (J qTop ({F ↾}_{⋃ J})) {({F ↾}_{⋃ J})}^{-1} [y] \in J$
27		ssralv	$⊢ x \subseteq J qTop ({F ↾}_{⋃ J}) \to (\forall y \in (J qTop ({F ↾}_{⋃ J})) {({F ↾}_{⋃ J})}^{-1} [y] \in J \to \forall y \in x {({F ↾}_{⋃ J})}^{-1} [y] \in J)$
28	26 27	mpan9	$⊢ ((J \in Top \land F \in V \land Fun F) \land x \subseteq J qTop ({F ↾}_{⋃ J})) \to \forall y \in x {({F ↾}_{⋃ J})}^{-1} [y] \in J$
29		iunopn	$⊢ (J \in Top \land \forall y \in x {({F ↾}_{⋃ J})}^{-1} [y] \in J) \to ⋃_{y \in x} {({F ↾}_{⋃ J})}^{-1} [y] \in J$
30	4 28 29	syl2an2r	$⊢ ((J \in Top \land F \in V \land Fun F) \land x \subseteq J qTop ({F ↾}_{⋃ J})) \to ⋃_{y \in x} {({F ↾}_{⋃ J})}^{-1} [y] \in J$
31	24 30	eqeltrid	$⊢ ((J \in Top \land F \in V \land Fun F) \land x \subseteq J qTop ({F ↾}_{⋃ J})) \to {({F ↾}_{⋃ J})}^{-1} [⋃ x] \in J$
32	31	ex	$⊢ (J \in Top \land F \in V \land Fun F) \to (x \subseteq J qTop ({F ↾}_{⋃ J}) \to {({F ↾}_{⋃ J})}^{-1} [⋃ x] \in J)$
33	23 32	jcad	$⊢ (J \in Top \land F \in V \land Fun F) \to (x \subseteq J qTop ({F ↾}_{⋃ J}) \to (⋃ x \subseteq ran ({F ↾}_{⋃ J}) \land {({F ↾}_{⋃ J})}^{-1} [⋃ x] \in J))$
34	1	elqtop	$⊢ (J \in Top \land ({F ↾}_{⋃ J}) : dom ({F ↾}_{⋃ J}) \underset{onto}{⟶} ran ({F ↾}_{⋃ J}) \land dom ({F ↾}_{⋃ J}) \subseteq ⋃ J) \to (⋃ x \in (J qTop ({F ↾}_{⋃ J})) \leftrightarrow (⋃ x \subseteq ran ({F ↾}_{⋃ J}) \land {({F ↾}_{⋃ J})}^{-1} [⋃ x] \in J))$
35	4 8 12 34	syl3anc	$⊢ (J \in Top \land F \in V \land Fun F) \to (⋃ x \in (J qTop ({F ↾}_{⋃ J})) \leftrightarrow (⋃ x \subseteq ran ({F ↾}_{⋃ J}) \land {({F ↾}_{⋃ J})}^{-1} [⋃ x] \in J))$
36	33 35	sylibrd	$⊢ (J \in Top \land F \in V \land Fun F) \to (x \subseteq J qTop ({F ↾}_{⋃ J}) \to ⋃ x \in (J qTop ({F ↾}_{⋃ J})))$
37	36	alrimiv	$⊢ (J \in Top \land F \in V \land Fun F) \to \forall x (x \subseteq J qTop ({F ↾}_{⋃ J}) \to ⋃ x \in (J qTop ({F ↾}_{⋃ J})))$
38		inss1	$⊢ x \cap y \subseteq x$
39	1	elqtop	$⊢ (J \in Top \land ({F ↾}_{⋃ J}) : dom ({F ↾}_{⋃ J}) \underset{onto}{⟶} ran ({F ↾}_{⋃ J}) \land dom ({F ↾}_{⋃ J}) \subseteq ⋃ J) \to (x \in (J qTop ({F ↾}_{⋃ J})) \leftrightarrow (x \subseteq ran ({F ↾}_{⋃ J}) \land {({F ↾}_{⋃ J})}^{-1} [x] \in J))$
40	4 8 12 39	syl3anc	$⊢ (J \in Top \land F \in V \land Fun F) \to (x \in (J qTop ({F ↾}_{⋃ J})) \leftrightarrow (x \subseteq ran ({F ↾}_{⋃ J}) \land {({F ↾}_{⋃ J})}^{-1} [x] \in J))$
41	40	biimpa	$⊢ ((J \in Top \land F \in V \land Fun F) \land x \in (J qTop ({F ↾}_{⋃ J}))) \to (x \subseteq ran ({F ↾}_{⋃ J}) \land {({F ↾}_{⋃ J})}^{-1} [x] \in J)$
42	41	adantrr	$⊢ ((J \in Top \land F \in V \land Fun F) \land (x \in (J qTop ({F ↾}_{⋃ J})) \land y \in (J qTop ({F ↾}_{⋃ J})))) \to (x \subseteq ran ({F ↾}_{⋃ J}) \land {({F ↾}_{⋃ J})}^{-1} [x] \in J)$
43	42	simpld	$⊢ ((J \in Top \land F \in V \land Fun F) \land (x \in (J qTop ({F ↾}_{⋃ J})) \land y \in (J qTop ({F ↾}_{⋃ J})))) \to x \subseteq ran ({F ↾}_{⋃ J})$
44	38 43	sstrid	$⊢ ((J \in Top \land F \in V \land Fun F) \land (x \in (J qTop ({F ↾}_{⋃ J})) \land y \in (J qTop ({F ↾}_{⋃ J})))) \to x \cap y \subseteq ran ({F ↾}_{⋃ J})$
45	6	adantr	$⊢ ((J \in Top \land F \in V \land Fun F) \land (x \in (J qTop ({F ↾}_{⋃ J})) \land y \in (J qTop ({F ↾}_{⋃ J})))) \to Fun ({F ↾}_{⋃ J})$
46		inpreima	$⊢ Fun ({F ↾}_{⋃ J}) \to {({F ↾}_{⋃ J})}^{-1} [x \cap y] = {({F ↾}_{⋃ J})}^{-1} [x] \cap {({F ↾}_{⋃ J})}^{-1} [y]$
47	45 46	syl	$⊢ ((J \in Top \land F \in V \land Fun F) \land (x \in (J qTop ({F ↾}_{⋃ J})) \land y \in (J qTop ({F ↾}_{⋃ J})))) \to {({F ↾}_{⋃ J})}^{-1} [x \cap y] = {({F ↾}_{⋃ J})}^{-1} [x] \cap {({F ↾}_{⋃ J})}^{-1} [y]$
48	4	adantr	$⊢ ((J \in Top \land F \in V \land Fun F) \land (x \in (J qTop ({F ↾}_{⋃ J})) \land y \in (J qTop ({F ↾}_{⋃ J})))) \to J \in Top$
49	42	simprd	$⊢ ((J \in Top \land F \in V \land Fun F) \land (x \in (J qTop ({F ↾}_{⋃ J})) \land y \in (J qTop ({F ↾}_{⋃ J})))) \to {({F ↾}_{⋃ J})}^{-1} [x] \in J$
50	25	adantrl	$⊢ ((J \in Top \land F \in V \land Fun F) \land (x \in (J qTop ({F ↾}_{⋃ J})) \land y \in (J qTop ({F ↾}_{⋃ J})))) \to {({F ↾}_{⋃ J})}^{-1} [y] \in J$
51		inopn	$⊢ (J \in Top \land {({F ↾}_{⋃ J})}^{-1} [x] \in J \land {({F ↾}_{⋃ J})}^{-1} [y] \in J) \to {({F ↾}_{⋃ J})}^{-1} [x] \cap {({F ↾}_{⋃ J})}^{-1} [y] \in J$
52	48 49 50 51	syl3anc	$⊢ ((J \in Top \land F \in V \land Fun F) \land (x \in (J qTop ({F ↾}_{⋃ J})) \land y \in (J qTop ({F ↾}_{⋃ J})))) \to {({F ↾}_{⋃ J})}^{-1} [x] \cap {({F ↾}_{⋃ J})}^{-1} [y] \in J$
53	47 52	eqeltrd	$⊢ ((J \in Top \land F \in V \land Fun F) \land (x \in (J qTop ({F ↾}_{⋃ J})) \land y \in (J qTop ({F ↾}_{⋃ J})))) \to {({F ↾}_{⋃ J})}^{-1} [x \cap y] \in J$
54	1	elqtop	$⊢ (J \in Top \land ({F ↾}_{⋃ J}) : dom ({F ↾}_{⋃ J}) \underset{onto}{⟶} ran ({F ↾}_{⋃ J}) \land dom ({F ↾}_{⋃ J}) \subseteq ⋃ J) \to (x \cap y \in (J qTop ({F ↾}_{⋃ J})) \leftrightarrow (x \cap y \subseteq ran ({F ↾}_{⋃ J}) \land {({F ↾}_{⋃ J})}^{-1} [x \cap y] \in J))$
55	4 8 12 54	syl3anc	$⊢ (J \in Top \land F \in V \land Fun F) \to (x \cap y \in (J qTop ({F ↾}_{⋃ J})) \leftrightarrow (x \cap y \subseteq ran ({F ↾}_{⋃ J}) \land {({F ↾}_{⋃ J})}^{-1} [x \cap y] \in J))$
56	55	adantr	$⊢ ((J \in Top \land F \in V \land Fun F) \land (x \in (J qTop ({F ↾}_{⋃ J})) \land y \in (J qTop ({F ↾}_{⋃ J})))) \to (x \cap y \in (J qTop ({F ↾}_{⋃ J})) \leftrightarrow (x \cap y \subseteq ran ({F ↾}_{⋃ J}) \land {({F ↾}_{⋃ J})}^{-1} [x \cap y] \in J))$
57	44 53 56	mpbir2and	$⊢ ((J \in Top \land F \in V \land Fun F) \land (x \in (J qTop ({F ↾}_{⋃ J})) \land y \in (J qTop ({F ↾}_{⋃ J})))) \to x \cap y \in (J qTop ({F ↾}_{⋃ J}))$
58	57	ralrimivva	$⊢ (J \in Top \land F \in V \land Fun F) \to \forall x \in (J qTop ({F ↾}_{⋃ J})) \forall y \in (J qTop ({F ↾}_{⋃ J})) x \cap y \in (J qTop ({F ↾}_{⋃ J}))$
59		ovex	$⊢ J qTop ({F ↾}_{⋃ J}) \in V$
60		istopg	$⊢ J qTop ({F ↾}_{⋃ J}) \in V \to (J qTop ({F ↾}_{⋃ J}) \in Top \leftrightarrow (\forall x (x \subseteq J qTop ({F ↾}_{⋃ J}) \to ⋃ x \in (J qTop ({F ↾}_{⋃ J}))) \land \forall x \in (J qTop ({F ↾}_{⋃ J})) \forall y \in (J qTop ({F ↾}_{⋃ J})) x \cap y \in (J qTop ({F ↾}_{⋃ J}))))$
61	59 60	ax-mp	$⊢ J qTop ({F ↾}_{⋃ J}) \in Top \leftrightarrow (\forall x (x \subseteq J qTop ({F ↾}_{⋃ J}) \to ⋃ x \in (J qTop ({F ↾}_{⋃ J}))) \land \forall x \in (J qTop ({F ↾}_{⋃ J})) \forall y \in (J qTop ({F ↾}_{⋃ J})) x \cap y \in (J qTop ({F ↾}_{⋃ J})))$
62	37 58 61	sylanbrc	$⊢ (J \in Top \land F \in V \land Fun F) \to J qTop ({F ↾}_{⋃ J}) \in Top$
63	3 62	eqeltrd	$⊢ (J \in Top \land F \in V \land Fun F) \to J qTop F \in Top$

Metamath Proof Explorer

Theorem qtoptop2

Proof