qtophaus

Description: If an open map's graph in the product space ( J tX J ) is closed, then its quotient topology is Hausdorff. (Contributed by Thierry Arnoux, 4-Jan-2020)

	Ref	Expression
Hypotheses	qtophaus.x	$⊢ X = ⋃ J$
	qtophaus.e	$⊢ \underset{˙}{\sim} = F^{-1} \circ F$
	qtophaus.h	$⊢ H = (x \in X, y \in X ⟼ ⟨F (x), F (y)⟩)$
	qtophaus.1	$⊢ φ \to J \in Haus$
	qtophaus.2	$⊢ φ \to F : X \underset{onto}{⟶} Y$
	qtophaus.3	$⊢ (φ \land x \in J) \to F [x] \in (J qTop F)$
	qtophaus.4	$⊢ φ \to \underset{˙}{\sim} \in Clsd (J \times_{t} J)$
Assertion	qtophaus	$⊢ φ \to J qTop F \in Haus$

Proof

Step	Hyp	Ref	Expression
1		qtophaus.x	$⊢ X = ⋃ J$
2		qtophaus.e	$⊢ \underset{˙}{\sim} = F^{-1} \circ F$
3		qtophaus.h	$⊢ H = (x \in X, y \in X ⟼ ⟨F (x), F (y)⟩)$
4		qtophaus.1	$⊢ φ \to J \in Haus$
5		qtophaus.2	$⊢ φ \to F : X \underset{onto}{⟶} Y$
6		qtophaus.3	$⊢ (φ \land x \in J) \to F [x] \in (J qTop F)$
7		qtophaus.4	$⊢ φ \to \underset{˙}{\sim} \in Clsd (J \times_{t} J)$
8		haustop	$⊢ J \in Haus \to J \in Top$
9	4 8	syl	$⊢ φ \to J \in Top$
10		fofn	$⊢ F : X \underset{onto}{⟶} Y \to F Fn X$
11	5 10	syl	$⊢ φ \to F Fn X$
12	1	qtoptop	$⊢ (J \in Top \land F Fn X) \to J qTop F \in Top$
13	9 11 12	syl2anc	$⊢ φ \to J qTop F \in Top$
14		txtop	$⊢ (J qTop F \in Top \land J qTop F \in Top) \to (J qTop F) \times_{t} (J qTop F) \in Top$
15	13 13 14	syl2anc	$⊢ φ \to (J qTop F) \times_{t} (J qTop F) \in Top$
16		idssxp	$⊢ {I ↾}_{⋃ (J qTop F)} \subseteq ⋃ (J qTop F) \times ⋃ (J qTop F)$
17		eqid	$⊢ ⋃ (J qTop F) = ⋃ (J qTop F)$
18	17 17	txuni	$⊢ (J qTop F \in Top \land J qTop F \in Top) \to ⋃ (J qTop F) \times ⋃ (J qTop F) = ⋃ ((J qTop F) \times_{t} (J qTop F))$
19	13 13 18	syl2anc	$⊢ φ \to ⋃ (J qTop F) \times ⋃ (J qTop F) = ⋃ ((J qTop F) \times_{t} (J qTop F))$
20	16 19	sseqtrid	$⊢ φ \to {I ↾}_{⋃ (J qTop F)} \subseteq ⋃ ((J qTop F) \times_{t} (J qTop F))$
21	1	qtopuni	$⊢ (J \in Top \land F : X \underset{onto}{⟶} Y) \to Y = ⋃ (J qTop F)$
22	9 5 21	syl2anc	$⊢ φ \to Y = ⋃ (J qTop F)$
23	22	sqxpeqd	$⊢ φ \to Y \times Y = ⋃ (J qTop F) \times ⋃ (J qTop F)$
24	23 19	eqtr2d	$⊢ φ \to ⋃ ((J qTop F) \times_{t} (J qTop F)) = Y \times Y$
25	22	eqcomd	$⊢ φ \to ⋃ (J qTop F) = Y$
26	25	reseq2d	$⊢ φ \to {I ↾}_{⋃ (J qTop F)} = {I ↾}_{Y}$
27	24 26	difeq12d	$⊢ φ \to ⋃ ((J qTop F) \times_{t} (J qTop F)) ∖ ({I ↾}_{⋃ (J qTop F)}) = (Y \times Y) ∖ ({I ↾}_{Y})$
28		opex	$⊢ ⟨F (x), F (y)⟩ \in V$
29	3 28	fnmpoi	$⊢ H Fn (X \times X)$
30		difss	$⊢ (X \times X) ∖ \underset{˙}{\sim} \subseteq X \times X$
31		fvelimab	$⊢ (H Fn (X \times X) \land (X \times X) ∖ \underset{˙}{\sim} \subseteq X \times X) \to (c \in H [(X \times X) ∖ \underset{˙}{\sim}] \leftrightarrow \exists z \in ((X \times X) ∖ \underset{˙}{\sim}) H (z) = c)$
32	29 30 31	mp2an	$⊢ c \in H [(X \times X) ∖ \underset{˙}{\sim}] \leftrightarrow \exists z \in ((X \times X) ∖ \underset{˙}{\sim}) H (z) = c$
33		simp-4r	$⊢ ((((((((φ \land c \in ((Y \times Y) ∖ I)) \land a \in Y) \land b \in Y) \land c = ⟨a, b⟩) \land x \in X) \land F (x) = a) \land y \in X) \land F (y) = b) \to x \in X$
34		simplr	$⊢ ((((((((φ \land c \in ((Y \times Y) ∖ I)) \land a \in Y) \land b \in Y) \land c = ⟨a, b⟩) \land x \in X) \land F (x) = a) \land y \in X) \land F (y) = b) \to y \in X$
35		opelxpi	$⊢ (x \in X \land y \in X) \to ⟨x, y⟩ \in (X \times X)$
36	33 34 35	syl2anc	$⊢ ((((((((φ \land c \in ((Y \times Y) ∖ I)) \land a \in Y) \land b \in Y) \land c = ⟨a, b⟩) \land x \in X) \land F (x) = a) \land y \in X) \land F (y) = b) \to ⟨x, y⟩ \in (X \times X)$
37		df-br	$⊢ x (X \times X) y \leftrightarrow ⟨x, y⟩ \in (X \times X)$
38	36 37	sylibr	$⊢ ((((((((φ \land c \in ((Y \times Y) ∖ I)) \land a \in Y) \land b \in Y) \land c = ⟨a, b⟩) \land x \in X) \land F (x) = a) \land y \in X) \land F (y) = b) \to x (X \times X) y$
39		simpllr	$⊢ ((((((((φ \land c \in ((Y \times Y) ∖ I)) \land a \in Y) \land b \in Y) \land c = ⟨a, b⟩) \land x \in X) \land F (x) = a) \land y \in X) \land F (y) = b) \to F (x) = a$
40		simpr	$⊢ ((((((((φ \land c \in ((Y \times Y) ∖ I)) \land a \in Y) \land b \in Y) \land c = ⟨a, b⟩) \land x \in X) \land F (x) = a) \land y \in X) \land F (y) = b) \to F (y) = b$
41	39 40	opeq12d	$⊢ ((((((((φ \land c \in ((Y \times Y) ∖ I)) \land a \in Y) \land b \in Y) \land c = ⟨a, b⟩) \land x \in X) \land F (x) = a) \land y \in X) \land F (y) = b) \to ⟨F (x), F (y)⟩ = ⟨a, b⟩$
42		simp-5r	$⊢ ((((((((φ \land c \in ((Y \times Y) ∖ I)) \land a \in Y) \land b \in Y) \land c = ⟨a, b⟩) \land x \in X) \land F (x) = a) \land y \in X) \land F (y) = b) \to c = ⟨a, b⟩$
43		simp-8r	$⊢ ((((((((φ \land c \in ((Y \times Y) ∖ I)) \land a \in Y) \land b \in Y) \land c = ⟨a, b⟩) \land x \in X) \land F (x) = a) \land y \in X) \land F (y) = b) \to c \in ((Y \times Y) ∖ I)$
44	42 43	eqeltrrd	$⊢ ((((((((φ \land c \in ((Y \times Y) ∖ I)) \land a \in Y) \land b \in Y) \land c = ⟨a, b⟩) \land x \in X) \land F (x) = a) \land y \in X) \land F (y) = b) \to ⟨a, b⟩ \in ((Y \times Y) ∖ I)$
45	41 44	eqeltrd	$⊢ ((((((((φ \land c \in ((Y \times Y) ∖ I)) \land a \in Y) \land b \in Y) \land c = ⟨a, b⟩) \land x \in X) \land F (x) = a) \land y \in X) \land F (y) = b) \to ⟨F (x), F (y)⟩ \in ((Y \times Y) ∖ I)$
46		relxp	$⊢ Rel (Y \times Y)$
47		opeldifid	$⊢ Rel (Y \times Y) \to (⟨F (x), F (y)⟩ \in ((Y \times Y) ∖ I) \leftrightarrow (⟨F (x), F (y)⟩ \in (Y \times Y) \land F (x) \neq F (y)))$
48	46 47	ax-mp	$⊢ ⟨F (x), F (y)⟩ \in ((Y \times Y) ∖ I) \leftrightarrow (⟨F (x), F (y)⟩ \in (Y \times Y) \land F (x) \neq F (y))$
49	45 48	sylib	$⊢ ((((((((φ \land c \in ((Y \times Y) ∖ I)) \land a \in Y) \land b \in Y) \land c = ⟨a, b⟩) \land x \in X) \land F (x) = a) \land y \in X) \land F (y) = b) \to (⟨F (x), F (y)⟩ \in (Y \times Y) \land F (x) \neq F (y))$
50	49	simprd	$⊢ ((((((((φ \land c \in ((Y \times Y) ∖ I)) \land a \in Y) \land b \in Y) \land c = ⟨a, b⟩) \land x \in X) \land F (x) = a) \land y \in X) \land F (y) = b) \to F (x) \neq F (y)$
51	11	ad8antr	$⊢ ((((((((φ \land c \in ((Y \times Y) ∖ I)) \land a \in Y) \land b \in Y) \land c = ⟨a, b⟩) \land x \in X) \land F (x) = a) \land y \in X) \land F (y) = b) \to F Fn X$
52	2	fcoinvbr	$⊢ (F Fn X \land x \in X \land y \in X) \to (x \underset{˙}{\sim} y \leftrightarrow F (x) = F (y))$
53	51 33 34 52	syl3anc	$⊢ ((((((((φ \land c \in ((Y \times Y) ∖ I)) \land a \in Y) \land b \in Y) \land c = ⟨a, b⟩) \land x \in X) \land F (x) = a) \land y \in X) \land F (y) = b) \to (x \underset{˙}{\sim} y \leftrightarrow F (x) = F (y))$
54	53	necon3bbid	$⊢ ((((((((φ \land c \in ((Y \times Y) ∖ I)) \land a \in Y) \land b \in Y) \land c = ⟨a, b⟩) \land x \in X) \land F (x) = a) \land y \in X) \land F (y) = b) \to (\neg x \underset{˙}{\sim} y \leftrightarrow F (x) \neq F (y))$
55	50 54	mpbird	$⊢ ((((((((φ \land c \in ((Y \times Y) ∖ I)) \land a \in Y) \land b \in Y) \land c = ⟨a, b⟩) \land x \in X) \land F (x) = a) \land y \in X) \land F (y) = b) \to \neg x \underset{˙}{\sim} y$
56		df-br	$⊢ x ((X \times X) ∖ \underset{˙}{\sim}) y \leftrightarrow ⟨x, y⟩ \in ((X \times X) ∖ \underset{˙}{\sim})$
57		brdif	$⊢ x ((X \times X) ∖ \underset{˙}{\sim}) y \leftrightarrow (x (X \times X) y \land \neg x \underset{˙}{\sim} y)$
58	56 57	bitr3i	$⊢ ⟨x, y⟩ \in ((X \times X) ∖ \underset{˙}{\sim}) \leftrightarrow (x (X \times X) y \land \neg x \underset{˙}{\sim} y)$
59	38 55 58	sylanbrc	$⊢ ((((((((φ \land c \in ((Y \times Y) ∖ I)) \land a \in Y) \land b \in Y) \land c = ⟨a, b⟩) \land x \in X) \land F (x) = a) \land y \in X) \land F (y) = b) \to ⟨x, y⟩ \in ((X \times X) ∖ \underset{˙}{\sim})$
60	3 33 34	fvproj	$⊢ ((((((((φ \land c \in ((Y \times Y) ∖ I)) \land a \in Y) \land b \in Y) \land c = ⟨a, b⟩) \land x \in X) \land F (x) = a) \land y \in X) \land F (y) = b) \to H (⟨x, y⟩) = ⟨F (x), F (y)⟩$
61	41 60 42	3eqtr4d	$⊢ ((((((((φ \land c \in ((Y \times Y) ∖ I)) \land a \in Y) \land b \in Y) \land c = ⟨a, b⟩) \land x \in X) \land F (x) = a) \land y \in X) \land F (y) = b) \to H (⟨x, y⟩) = c$
62		fveqeq2	$⊢ z = ⟨x, y⟩ \to (H (z) = c \leftrightarrow H (⟨x, y⟩) = c)$
63	62	rspcev	$⊢ (⟨x, y⟩ \in ((X \times X) ∖ \underset{˙}{\sim}) \land H (⟨x, y⟩) = c) \to \exists z \in ((X \times X) ∖ \underset{˙}{\sim}) H (z) = c$
64	59 61 63	syl2anc	$⊢ ((((((((φ \land c \in ((Y \times Y) ∖ I)) \land a \in Y) \land b \in Y) \land c = ⟨a, b⟩) \land x \in X) \land F (x) = a) \land y \in X) \land F (y) = b) \to \exists z \in ((X \times X) ∖ \underset{˙}{\sim}) H (z) = c$
65		fofun	$⊢ F : X \underset{onto}{⟶} Y \to Fun F$
66	5 65	syl	$⊢ φ \to Fun F$
67	66	ad4antr	$⊢ ((((φ \land c \in ((Y \times Y) ∖ I)) \land a \in Y) \land b \in Y) \land c = ⟨a, b⟩) \to Fun F$
68	67	ad2antrr	$⊢ ((((((φ \land c \in ((Y \times Y) ∖ I)) \land a \in Y) \land b \in Y) \land c = ⟨a, b⟩) \land x \in X) \land F (x) = a) \to Fun F$
69		simp-4r	$⊢ ((((((φ \land c \in ((Y \times Y) ∖ I)) \land a \in Y) \land b \in Y) \land c = ⟨a, b⟩) \land x \in X) \land F (x) = a) \to b \in Y$
70		foima	$⊢ F : X \underset{onto}{⟶} Y \to F [X] = Y$
71	5 70	syl	$⊢ φ \to F [X] = Y$
72	71	ad4antr	$⊢ ((((φ \land c \in ((Y \times Y) ∖ I)) \land a \in Y) \land b \in Y) \land c = ⟨a, b⟩) \to F [X] = Y$
73	72	ad2antrr	$⊢ ((((((φ \land c \in ((Y \times Y) ∖ I)) \land a \in Y) \land b \in Y) \land c = ⟨a, b⟩) \land x \in X) \land F (x) = a) \to F [X] = Y$
74	69 73	eleqtrrd	$⊢ ((((((φ \land c \in ((Y \times Y) ∖ I)) \land a \in Y) \land b \in Y) \land c = ⟨a, b⟩) \land x \in X) \land F (x) = a) \to b \in F [X]$
75		fvelima	$⊢ (Fun F \land b \in F [X]) \to \exists y \in X F (y) = b$
76	68 74 75	syl2anc	$⊢ ((((((φ \land c \in ((Y \times Y) ∖ I)) \land a \in Y) \land b \in Y) \land c = ⟨a, b⟩) \land x \in X) \land F (x) = a) \to \exists y \in X F (y) = b$
77	64 76	r19.29a	$⊢ ((((((φ \land c \in ((Y \times Y) ∖ I)) \land a \in Y) \land b \in Y) \land c = ⟨a, b⟩) \land x \in X) \land F (x) = a) \to \exists z \in ((X \times X) ∖ \underset{˙}{\sim}) H (z) = c$
78		simpllr	$⊢ ((((φ \land c \in ((Y \times Y) ∖ I)) \land a \in Y) \land b \in Y) \land c = ⟨a, b⟩) \to a \in Y$
79	78 72	eleqtrrd	$⊢ ((((φ \land c \in ((Y \times Y) ∖ I)) \land a \in Y) \land b \in Y) \land c = ⟨a, b⟩) \to a \in F [X]$
80		fvelima	$⊢ (Fun F \land a \in F [X]) \to \exists x \in X F (x) = a$
81	67 79 80	syl2anc	$⊢ ((((φ \land c \in ((Y \times Y) ∖ I)) \land a \in Y) \land b \in Y) \land c = ⟨a, b⟩) \to \exists x \in X F (x) = a$
82	77 81	r19.29a	$⊢ ((((φ \land c \in ((Y \times Y) ∖ I)) \land a \in Y) \land b \in Y) \land c = ⟨a, b⟩) \to \exists z \in ((X \times X) ∖ \underset{˙}{\sim}) H (z) = c$
83		simpr	$⊢ (φ \land c \in ((Y \times Y) ∖ I)) \to c \in ((Y \times Y) ∖ I)$
84	83	eldifad	$⊢ (φ \land c \in ((Y \times Y) ∖ I)) \to c \in (Y \times Y)$
85		elxp2	$⊢ c \in (Y \times Y) \leftrightarrow \exists a \in Y \exists b \in Y c = ⟨a, b⟩$
86	84 85	sylib	$⊢ (φ \land c \in ((Y \times Y) ∖ I)) \to \exists a \in Y \exists b \in Y c = ⟨a, b⟩$
87	82 86	r19.29vva	$⊢ (φ \land c \in ((Y \times Y) ∖ I)) \to \exists z \in ((X \times X) ∖ \underset{˙}{\sim}) H (z) = c$
88		simpr	$⊢ (((((φ \land z \in ((X \times X) ∖ \underset{˙}{\sim})) \land H (z) = c) \land x \in X) \land y \in X) \land z = ⟨x, y⟩) \to z = ⟨x, y⟩$
89	88	fveq2d	$⊢ (((((φ \land z \in ((X \times X) ∖ \underset{˙}{\sim})) \land H (z) = c) \land x \in X) \land y \in X) \land z = ⟨x, y⟩) \to H (z) = H (⟨x, y⟩)$
90		simp-4r	$⊢ (((((φ \land z \in ((X \times X) ∖ \underset{˙}{\sim})) \land H (z) = c) \land x \in X) \land y \in X) \land z = ⟨x, y⟩) \to H (z) = c$
91		simpllr	$⊢ (((((φ \land z \in ((X \times X) ∖ \underset{˙}{\sim})) \land H (z) = c) \land x \in X) \land y \in X) \land z = ⟨x, y⟩) \to x \in X$
92		simplr	$⊢ (((((φ \land z \in ((X \times X) ∖ \underset{˙}{\sim})) \land H (z) = c) \land x \in X) \land y \in X) \land z = ⟨x, y⟩) \to y \in X$
93	3 91 92	fvproj	$⊢ (((((φ \land z \in ((X \times X) ∖ \underset{˙}{\sim})) \land H (z) = c) \land x \in X) \land y \in X) \land z = ⟨x, y⟩) \to H (⟨x, y⟩) = ⟨F (x), F (y)⟩$
94	89 90 93	3eqtr3d	$⊢ (((((φ \land z \in ((X \times X) ∖ \underset{˙}{\sim})) \land H (z) = c) \land x \in X) \land y \in X) \land z = ⟨x, y⟩) \to c = ⟨F (x), F (y)⟩$
95		fof	$⊢ F : X \underset{onto}{⟶} Y \to F : X ⟶ Y$
96	5 95	syl	$⊢ φ \to F : X ⟶ Y$
97	96	ad5antr	$⊢ (((((φ \land z \in ((X \times X) ∖ \underset{˙}{\sim})) \land H (z) = c) \land x \in X) \land y \in X) \land z = ⟨x, y⟩) \to F : X ⟶ Y$
98	97 91	ffvelrnd	$⊢ (((((φ \land z \in ((X \times X) ∖ \underset{˙}{\sim})) \land H (z) = c) \land x \in X) \land y \in X) \land z = ⟨x, y⟩) \to F (x) \in Y$
99	97 92	ffvelrnd	$⊢ (((((φ \land z \in ((X \times X) ∖ \underset{˙}{\sim})) \land H (z) = c) \land x \in X) \land y \in X) \land z = ⟨x, y⟩) \to F (y) \in Y$
100		opelxp	$⊢ ⟨F (x), F (y)⟩ \in (Y \times Y) \leftrightarrow (F (x) \in Y \land F (y) \in Y)$
101	98 99 100	sylanbrc	$⊢ (((((φ \land z \in ((X \times X) ∖ \underset{˙}{\sim})) \land H (z) = c) \land x \in X) \land y \in X) \land z = ⟨x, y⟩) \to ⟨F (x), F (y)⟩ \in (Y \times Y)$
102		simp-5r	$⊢ (((((φ \land z \in ((X \times X) ∖ \underset{˙}{\sim})) \land H (z) = c) \land x \in X) \land y \in X) \land z = ⟨x, y⟩) \to z \in ((X \times X) ∖ \underset{˙}{\sim})$
103	88 102	eqeltrrd	$⊢ (((((φ \land z \in ((X \times X) ∖ \underset{˙}{\sim})) \land H (z) = c) \land x \in X) \land y \in X) \land z = ⟨x, y⟩) \to ⟨x, y⟩ \in ((X \times X) ∖ \underset{˙}{\sim})$
104	58	simprbi	$⊢ ⟨x, y⟩ \in ((X \times X) ∖ \underset{˙}{\sim}) \to \neg x \underset{˙}{\sim} y$
105	103 104	syl	$⊢ (((((φ \land z \in ((X \times X) ∖ \underset{˙}{\sim})) \land H (z) = c) \land x \in X) \land y \in X) \land z = ⟨x, y⟩) \to \neg x \underset{˙}{\sim} y$
106	11	ad5antr	$⊢ (((((φ \land z \in ((X \times X) ∖ \underset{˙}{\sim})) \land H (z) = c) \land x \in X) \land y \in X) \land z = ⟨x, y⟩) \to F Fn X$
107	106 91 92 52	syl3anc	$⊢ (((((φ \land z \in ((X \times X) ∖ \underset{˙}{\sim})) \land H (z) = c) \land x \in X) \land y \in X) \land z = ⟨x, y⟩) \to (x \underset{˙}{\sim} y \leftrightarrow F (x) = F (y))$
108	107	necon3bbid	$⊢ (((((φ \land z \in ((X \times X) ∖ \underset{˙}{\sim})) \land H (z) = c) \land x \in X) \land y \in X) \land z = ⟨x, y⟩) \to (\neg x \underset{˙}{\sim} y \leftrightarrow F (x) \neq F (y))$
109	105 108	mpbid	$⊢ (((((φ \land z \in ((X \times X) ∖ \underset{˙}{\sim})) \land H (z) = c) \land x \in X) \land y \in X) \land z = ⟨x, y⟩) \to F (x) \neq F (y)$
110	101 109 48	sylanbrc	$⊢ (((((φ \land z \in ((X \times X) ∖ \underset{˙}{\sim})) \land H (z) = c) \land x \in X) \land y \in X) \land z = ⟨x, y⟩) \to ⟨F (x), F (y)⟩ \in ((Y \times Y) ∖ I)$
111	94 110	eqeltrd	$⊢ (((((φ \land z \in ((X \times X) ∖ \underset{˙}{\sim})) \land H (z) = c) \land x \in X) \land y \in X) \land z = ⟨x, y⟩) \to c \in ((Y \times Y) ∖ I)$
112		eldifi	$⊢ z \in ((X \times X) ∖ \underset{˙}{\sim}) \to z \in (X \times X)$
113	112	adantl	$⊢ (φ \land z \in ((X \times X) ∖ \underset{˙}{\sim})) \to z \in (X \times X)$
114		elxp2	$⊢ z \in (X \times X) \leftrightarrow \exists x \in X \exists y \in X z = ⟨x, y⟩$
115	113 114	sylib	$⊢ (φ \land z \in ((X \times X) ∖ \underset{˙}{\sim})) \to \exists x \in X \exists y \in X z = ⟨x, y⟩$
116	115	adantr	$⊢ ((φ \land z \in ((X \times X) ∖ \underset{˙}{\sim})) \land H (z) = c) \to \exists x \in X \exists y \in X z = ⟨x, y⟩$
117	111 116	r19.29vva	$⊢ ((φ \land z \in ((X \times X) ∖ \underset{˙}{\sim})) \land H (z) = c) \to c \in ((Y \times Y) ∖ I)$
118	117	r19.29an	$⊢ (φ \land \exists z \in ((X \times X) ∖ \underset{˙}{\sim}) H (z) = c) \to c \in ((Y \times Y) ∖ I)$
119	87 118	impbida	$⊢ φ \to (c \in ((Y \times Y) ∖ I) \leftrightarrow \exists z \in ((X \times X) ∖ \underset{˙}{\sim}) H (z) = c)$
120	32 119	bitr4id	$⊢ φ \to (c \in H [(X \times X) ∖ \underset{˙}{\sim}] \leftrightarrow c \in ((Y \times Y) ∖ I))$
121	120	eqrdv	$⊢ φ \to H [(X \times X) ∖ \underset{˙}{\sim}] = (Y \times Y) ∖ I$
122		ssv	$⊢ Y \subseteq V$
123		xpss2	$⊢ Y \subseteq V \to Y \times Y \subseteq Y \times V$
124		difres	$⊢ Y \times Y \subseteq Y \times V \to (Y \times Y) ∖ ({I ↾}_{Y}) = (Y \times Y) ∖ I$
125	122 123 124	mp2b	$⊢ (Y \times Y) ∖ ({I ↾}_{Y}) = (Y \times Y) ∖ I$
126	121 125	eqtr4di	$⊢ φ \to H [(X \times X) ∖ \underset{˙}{\sim}] = (Y \times Y) ∖ ({I ↾}_{Y})$
127	1	toptopon	$⊢ J \in Top \leftrightarrow J \in TopOn (X)$
128	9 127	sylib	$⊢ φ \to J \in TopOn (X)$
129		qtoptopon	$⊢ (J \in TopOn (X) \land F : X \underset{onto}{⟶} Y) \to J qTop F \in TopOn (Y)$
130	128 5 129	syl2anc	$⊢ φ \to J qTop F \in TopOn (Y)$
131	6	ralrimiva	$⊢ φ \to \forall x \in J F [x] \in (J qTop F)$
132		imaeq2	$⊢ x = y \to F [x] = F [y]$
133	132	eleq1d	$⊢ x = y \to (F [x] \in (J qTop F) \leftrightarrow F [y] \in (J qTop F))$
134	133	cbvralvw	$⊢ \forall x \in J F [x] \in (J qTop F) \leftrightarrow \forall y \in J F [y] \in (J qTop F)$
135	131 134	sylib	$⊢ φ \to \forall y \in J F [y] \in (J qTop F)$
136	135	r19.21bi	$⊢ (φ \land y \in J) \to F [y] \in (J qTop F)$
137	1 1	txuni	$⊢ (J \in Top \land J \in Top) \to X \times X = ⋃ (J \times_{t} J)$
138	9 9 137	syl2anc	$⊢ φ \to X \times X = ⋃ (J \times_{t} J)$
139	138	difeq1d	$⊢ φ \to (X \times X) ∖ \underset{˙}{\sim} = ⋃ (J \times_{t} J) ∖ \underset{˙}{\sim}$
140		txtop	$⊢ (J \in Top \land J \in Top) \to J \times_{t} J \in Top$
141	9 9 140	syl2anc	$⊢ φ \to J \times_{t} J \in Top$
142		fcoinver	$⊢ F Fn X \to (F^{-1} \circ F) Er X$
143	11 142	syl	$⊢ φ \to (F^{-1} \circ F) Er X$
144		ereq1	$⊢ \underset{˙}{\sim} = F^{-1} \circ F \to (\underset{˙}{\sim} Er X \leftrightarrow (F^{-1} \circ F) Er X)$
145	2 144	ax-mp	$⊢ \underset{˙}{\sim} Er X \leftrightarrow (F^{-1} \circ F) Er X$
146	143 145	sylibr	$⊢ φ \to \underset{˙}{\sim} Er X$
147		erssxp	$⊢ \underset{˙}{\sim} Er X \to \underset{˙}{\sim} \subseteq X \times X$
148	146 147	syl	$⊢ φ \to \underset{˙}{\sim} \subseteq X \times X$
149	148 138	sseqtrd	$⊢ φ \to \underset{˙}{\sim} \subseteq ⋃ (J \times_{t} J)$
150		eqid	$⊢ ⋃ (J \times_{t} J) = ⋃ (J \times_{t} J)$
151	150	iscld2	$⊢ (J \times_{t} J \in Top \land \underset{˙}{\sim} \subseteq ⋃ (J \times_{t} J)) \to (\underset{˙}{\sim} \in Clsd (J \times_{t} J) \leftrightarrow ⋃ (J \times_{t} J) ∖ \underset{˙}{\sim} \in (J \times_{t} J))$
152	141 149 151	syl2anc	$⊢ φ \to (\underset{˙}{\sim} \in Clsd (J \times_{t} J) \leftrightarrow ⋃ (J \times_{t} J) ∖ \underset{˙}{\sim} \in (J \times_{t} J))$
153	7 152	mpbid	$⊢ φ \to ⋃ (J \times_{t} J) ∖ \underset{˙}{\sim} \in (J \times_{t} J)$
154	139 153	eqeltrd	$⊢ φ \to (X \times X) ∖ \underset{˙}{\sim} \in (J \times_{t} J)$
155	96 96 128 128 130 130 6 136 154 3	txomap	$⊢ φ \to H [(X \times X) ∖ \underset{˙}{\sim}] \in ((J qTop F) \times_{t} (J qTop F))$
156	126 155	eqeltrrd	$⊢ φ \to (Y \times Y) ∖ ({I ↾}_{Y}) \in ((J qTop F) \times_{t} (J qTop F))$
157	27 156	eqeltrd	$⊢ φ \to ⋃ ((J qTop F) \times_{t} (J qTop F)) ∖ ({I ↾}_{⋃ (J qTop F)}) \in ((J qTop F) \times_{t} (J qTop F))$
158		eqid	$⊢ ⋃ ((J qTop F) \times_{t} (J qTop F)) = ⋃ ((J qTop F) \times_{t} (J qTop F))$
159	158	iscld2	$⊢ ((J qTop F) \times_{t} (J qTop F) \in Top \land {I ↾}_{⋃ (J qTop F)} \subseteq ⋃ ((J qTop F) \times_{t} (J qTop F))) \to ({I ↾}_{⋃ (J qTop F)} \in Clsd ((J qTop F) \times_{t} (J qTop F)) \leftrightarrow ⋃ ((J qTop F) \times_{t} (J qTop F)) ∖ ({I ↾}_{⋃ (J qTop F)}) \in ((J qTop F) \times_{t} (J qTop F)))$
160	159	biimpar	$⊢ (((J qTop F) \times_{t} (J qTop F) \in Top \land {I ↾}_{⋃ (J qTop F)} \subseteq ⋃ ((J qTop F) \times_{t} (J qTop F))) \land ⋃ ((J qTop F) \times_{t} (J qTop F)) ∖ ({I ↾}_{⋃ (J qTop F)}) \in ((J qTop F) \times_{t} (J qTop F))) \to {I ↾}_{⋃ (J qTop F)} \in Clsd ((J qTop F) \times_{t} (J qTop F))$
161	15 20 157 160	syl21anc	$⊢ φ \to {I ↾}_{⋃ (J qTop F)} \in Clsd ((J qTop F) \times_{t} (J qTop F))$
162	17	hausdiag	$⊢ J qTop F \in Haus \leftrightarrow (J qTop F \in Top \land {I ↾}_{⋃ (J qTop F)} \in Clsd ((J qTop F) \times_{t} (J qTop F)))$
163	13 161 162	sylanbrc	$⊢ φ \to J qTop F \in Haus$

Metamath Proof Explorer

Theorem qtophaus

Proof