xkohaus

Description: If the codomain space is Hausdorff, then the compact-open topology of continuous functions is also Hausdorff. (Contributed by Mario Carneiro, 19-Mar-2015)

		Ref	Expression
	Assertion	xkohaus	$⊢ (R \in Top \land S \in Haus) \to S^_{ko} R \in Haus$

Proof

Step	Hyp	Ref	Expression
1		haustop	$⊢ S \in Haus \to S \in Top$
2		xkotop	$⊢ (R \in Top \land S \in Top) \to S^_{ko} R \in Top$
3	1 2	sylan2	$⊢ (R \in Top \land S \in Haus) \to S^_{ko} R \in Top$
4		eqid	$⊢ S^_{ko} R = S^_{ko} R$
5	4	xkouni	$⊢ (R \in Top \land S \in Top) \to R Cn S = ⋃ (S^_{ko} R)$
6	1 5	sylan2	$⊢ (R \in Top \land S \in Haus) \to R Cn S = ⋃ (S^_{ko} R)$
7	6	eleq2d	$⊢ (R \in Top \land S \in Haus) \to (f \in (R Cn S) \leftrightarrow f \in ⋃ (S^_{ko} R))$
8	6	eleq2d	$⊢ (R \in Top \land S \in Haus) \to (g \in (R Cn S) \leftrightarrow g \in ⋃ (S^_{ko} R))$
9	7 8	anbi12d	$⊢ (R \in Top \land S \in Haus) \to ((f \in (R Cn S) \land g \in (R Cn S)) \leftrightarrow (f \in ⋃ (S^_{ko} R) \land g \in ⋃ (S^_{ko} R)))$
10		simprl	$⊢ ((R \in Top \land S \in Haus) \land (f \in (R Cn S) \land g \in (R Cn S))) \to f \in (R Cn S)$
11		eqid	$⊢ ⋃ R = ⋃ R$
12		eqid	$⊢ ⋃ S = ⋃ S$
13	11 12	cnf	$⊢ f \in (R Cn S) \to f : ⋃ R ⟶ ⋃ S$
14	10 13	syl	$⊢ ((R \in Top \land S \in Haus) \land (f \in (R Cn S) \land g \in (R Cn S))) \to f : ⋃ R ⟶ ⋃ S$
15	14	ffnd	$⊢ ((R \in Top \land S \in Haus) \land (f \in (R Cn S) \land g \in (R Cn S))) \to f Fn ⋃ R$
16		simprr	$⊢ ((R \in Top \land S \in Haus) \land (f \in (R Cn S) \land g \in (R Cn S))) \to g \in (R Cn S)$
17	11 12	cnf	$⊢ g \in (R Cn S) \to g : ⋃ R ⟶ ⋃ S$
18	16 17	syl	$⊢ ((R \in Top \land S \in Haus) \land (f \in (R Cn S) \land g \in (R Cn S))) \to g : ⋃ R ⟶ ⋃ S$
19	18	ffnd	$⊢ ((R \in Top \land S \in Haus) \land (f \in (R Cn S) \land g \in (R Cn S))) \to g Fn ⋃ R$
20		eqfnfv	$⊢ (f Fn ⋃ R \land g Fn ⋃ R) \to (f = g \leftrightarrow \forall x \in ⋃ R f (x) = g (x))$
21	15 19 20	syl2anc	$⊢ ((R \in Top \land S \in Haus) \land (f \in (R Cn S) \land g \in (R Cn S))) \to (f = g \leftrightarrow \forall x \in ⋃ R f (x) = g (x))$
22	21	necon3abid	$⊢ ((R \in Top \land S \in Haus) \land (f \in (R Cn S) \land g \in (R Cn S))) \to (f \neq g \leftrightarrow \neg \forall x \in ⋃ R f (x) = g (x))$
23		rexnal	$⊢ \exists x \in ⋃ R \neg f (x) = g (x) \leftrightarrow \neg \forall x \in ⋃ R f (x) = g (x)$
24		df-ne	$⊢ f (x) \neq g (x) \leftrightarrow \neg f (x) = g (x)$
25		simpllr	$⊢ (((R \in Top \land S \in Haus) \land (f \in (R Cn S) \land g \in (R Cn S))) \land (x \in ⋃ R \land f (x) \neq g (x))) \to S \in Haus$
26	14	adantr	$⊢ (((R \in Top \land S \in Haus) \land (f \in (R Cn S) \land g \in (R Cn S))) \land (x \in ⋃ R \land f (x) \neq g (x))) \to f : ⋃ R ⟶ ⋃ S$
27		simprl	$⊢ (((R \in Top \land S \in Haus) \land (f \in (R Cn S) \land g \in (R Cn S))) \land (x \in ⋃ R \land f (x) \neq g (x))) \to x \in ⋃ R$
28	26 27	ffvelrnd	$⊢ (((R \in Top \land S \in Haus) \land (f \in (R Cn S) \land g \in (R Cn S))) \land (x \in ⋃ R \land f (x) \neq g (x))) \to f (x) \in ⋃ S$
29	18	adantr	$⊢ (((R \in Top \land S \in Haus) \land (f \in (R Cn S) \land g \in (R Cn S))) \land (x \in ⋃ R \land f (x) \neq g (x))) \to g : ⋃ R ⟶ ⋃ S$
30	29 27	ffvelrnd	$⊢ (((R \in Top \land S \in Haus) \land (f \in (R Cn S) \land g \in (R Cn S))) \land (x \in ⋃ R \land f (x) \neq g (x))) \to g (x) \in ⋃ S$
31		simprr	$⊢ (((R \in Top \land S \in Haus) \land (f \in (R Cn S) \land g \in (R Cn S))) \land (x \in ⋃ R \land f (x) \neq g (x))) \to f (x) \neq g (x)$
32	12	hausnei	$⊢ (S \in Haus \land (f (x) \in ⋃ S \land g (x) \in ⋃ S \land f (x) \neq g (x))) \to \exists a \in S \exists b \in S (f (x) \in a \land g (x) \in b \land a \cap b = \emptyset)$
33	25 28 30 31 32	syl13anc	$⊢ (((R \in Top \land S \in Haus) \land (f \in (R Cn S) \land g \in (R Cn S))) \land (x \in ⋃ R \land f (x) \neq g (x))) \to \exists a \in S \exists b \in S (f (x) \in a \land g (x) \in b \land a \cap b = \emptyset)$
34	33	expr	$⊢ (((R \in Top \land S \in Haus) \land (f \in (R Cn S) \land g \in (R Cn S))) \land x \in ⋃ R) \to (f (x) \neq g (x) \to \exists a \in S \exists b \in S (f (x) \in a \land g (x) \in b \land a \cap b = \emptyset))$
35	24 34	syl5bir	$⊢ (((R \in Top \land S \in Haus) \land (f \in (R Cn S) \land g \in (R Cn S))) \land x \in ⋃ R) \to (\neg f (x) = g (x) \to \exists a \in S \exists b \in S (f (x) \in a \land g (x) \in b \land a \cap b = \emptyset))$
36		simp-4l	$⊢ ((((R \in Top \land S \in Haus) \land (f \in (R Cn S) \land g \in (R Cn S))) \land x \in ⋃ R) \land ((a \in S \land b \in S) \land (f (x) \in a \land g (x) \in b \land a \cap b = \emptyset))) \to R \in Top$
37	1	ad4antlr	$⊢ ((((R \in Top \land S \in Haus) \land (f \in (R Cn S) \land g \in (R Cn S))) \land x \in ⋃ R) \land ((a \in S \land b \in S) \land (f (x) \in a \land g (x) \in b \land a \cap b = \emptyset))) \to S \in Top$
38		simplr	$⊢ ((((R \in Top \land S \in Haus) \land (f \in (R Cn S) \land g \in (R Cn S))) \land x \in ⋃ R) \land ((a \in S \land b \in S) \land (f (x) \in a \land g (x) \in b \land a \cap b = \emptyset))) \to x \in ⋃ R$
39	38	snssd	$⊢ ((((R \in Top \land S \in Haus) \land (f \in (R Cn S) \land g \in (R Cn S))) \land x \in ⋃ R) \land ((a \in S \land b \in S) \land (f (x) \in a \land g (x) \in b \land a \cap b = \emptyset))) \to \{x\} \subseteq ⋃ R$
40		toptopon2	$⊢ R \in Top \leftrightarrow R \in TopOn (⋃ R)$
41	36 40	sylib	$⊢ ((((R \in Top \land S \in Haus) \land (f \in (R Cn S) \land g \in (R Cn S))) \land x \in ⋃ R) \land ((a \in S \land b \in S) \land (f (x) \in a \land g (x) \in b \land a \cap b = \emptyset))) \to R \in TopOn (⋃ R)$
42		restsn2	$⊢ (R \in TopOn (⋃ R) \land x \in ⋃ R) \to R ↾_{𝑡} \{x\} = 𝒫 \{x\}$
43	41 38 42	syl2anc	$⊢ ((((R \in Top \land S \in Haus) \land (f \in (R Cn S) \land g \in (R Cn S))) \land x \in ⋃ R) \land ((a \in S \land b \in S) \land (f (x) \in a \land g (x) \in b \land a \cap b = \emptyset))) \to R ↾_{𝑡} \{x\} = 𝒫 \{x\}$
44		snfi	$⊢ \{x\} \in Fin$
45		discmp	$⊢ \{x\} \in Fin \leftrightarrow 𝒫 \{x\} \in Comp$
46	44 45	mpbi	$⊢ 𝒫 \{x\} \in Comp$
47	43 46	eqeltrdi	$⊢ ((((R \in Top \land S \in Haus) \land (f \in (R Cn S) \land g \in (R Cn S))) \land x \in ⋃ R) \land ((a \in S \land b \in S) \land (f (x) \in a \land g (x) \in b \land a \cap b = \emptyset))) \to R ↾_{𝑡} \{x\} \in Comp$
48		simprll	$⊢ ((((R \in Top \land S \in Haus) \land (f \in (R Cn S) \land g \in (R Cn S))) \land x \in ⋃ R) \land ((a \in S \land b \in S) \land (f (x) \in a \land g (x) \in b \land a \cap b = \emptyset))) \to a \in S$
49	11 36 37 39 47 48	xkoopn	$⊢ ((((R \in Top \land S \in Haus) \land (f \in (R Cn S) \land g \in (R Cn S))) \land x \in ⋃ R) \land ((a \in S \land b \in S) \land (f (x) \in a \land g (x) \in b \land a \cap b = \emptyset))) \to \{h \in (R Cn S) \| h [\{x\}] \subseteq a\} \in (S^_{ko} R)$
50		simprlr	$⊢ ((((R \in Top \land S \in Haus) \land (f \in (R Cn S) \land g \in (R Cn S))) \land x \in ⋃ R) \land ((a \in S \land b \in S) \land (f (x) \in a \land g (x) \in b \land a \cap b = \emptyset))) \to b \in S$
51	11 36 37 39 47 50	xkoopn	$⊢ ((((R \in Top \land S \in Haus) \land (f \in (R Cn S) \land g \in (R Cn S))) \land x \in ⋃ R) \land ((a \in S \land b \in S) \land (f (x) \in a \land g (x) \in b \land a \cap b = \emptyset))) \to \{h \in (R Cn S) \| h [\{x\}] \subseteq b\} \in (S^_{ko} R)$
52		imaeq1	$⊢ h = f \to h [\{x\}] = f [\{x\}]$
53	52	sseq1d	$⊢ h = f \to (h [\{x\}] \subseteq a \leftrightarrow f [\{x\}] \subseteq a)$
54	10	ad2antrr	$⊢ ((((R \in Top \land S \in Haus) \land (f \in (R Cn S) \land g \in (R Cn S))) \land x \in ⋃ R) \land ((a \in S \land b \in S) \land (f (x) \in a \land g (x) \in b \land a \cap b = \emptyset))) \to f \in (R Cn S)$
55	15	ad2antrr	$⊢ ((((R \in Top \land S \in Haus) \land (f \in (R Cn S) \land g \in (R Cn S))) \land x \in ⋃ R) \land ((a \in S \land b \in S) \land (f (x) \in a \land g (x) \in b \land a \cap b = \emptyset))) \to f Fn ⋃ R$
56		fnsnfv	$⊢ (f Fn ⋃ R \land x \in ⋃ R) \to \{f (x)\} = f [\{x\}]$
57	55 38 56	syl2anc	$⊢ ((((R \in Top \land S \in Haus) \land (f \in (R Cn S) \land g \in (R Cn S))) \land x \in ⋃ R) \land ((a \in S \land b \in S) \land (f (x) \in a \land g (x) \in b \land a \cap b = \emptyset))) \to \{f (x)\} = f [\{x\}]$
58		simprr1	$⊢ ((((R \in Top \land S \in Haus) \land (f \in (R Cn S) \land g \in (R Cn S))) \land x \in ⋃ R) \land ((a \in S \land b \in S) \land (f (x) \in a \land g (x) \in b \land a \cap b = \emptyset))) \to f (x) \in a$
59	58	snssd	$⊢ ((((R \in Top \land S \in Haus) \land (f \in (R Cn S) \land g \in (R Cn S))) \land x \in ⋃ R) \land ((a \in S \land b \in S) \land (f (x) \in a \land g (x) \in b \land a \cap b = \emptyset))) \to \{f (x)\} \subseteq a$
60	57 59	eqsstrrd	$⊢ ((((R \in Top \land S \in Haus) \land (f \in (R Cn S) \land g \in (R Cn S))) \land x \in ⋃ R) \land ((a \in S \land b \in S) \land (f (x) \in a \land g (x) \in b \land a \cap b = \emptyset))) \to f [\{x\}] \subseteq a$
61	53 54 60	elrabd	$⊢ ((((R \in Top \land S \in Haus) \land (f \in (R Cn S) \land g \in (R Cn S))) \land x \in ⋃ R) \land ((a \in S \land b \in S) \land (f (x) \in a \land g (x) \in b \land a \cap b = \emptyset))) \to f \in \{h \in (R Cn S) \| h [\{x\}] \subseteq a\}$
62		imaeq1	$⊢ h = g \to h [\{x\}] = g [\{x\}]$
63	62	sseq1d	$⊢ h = g \to (h [\{x\}] \subseteq b \leftrightarrow g [\{x\}] \subseteq b)$
64	16	ad2antrr	$⊢ ((((R \in Top \land S \in Haus) \land (f \in (R Cn S) \land g \in (R Cn S))) \land x \in ⋃ R) \land ((a \in S \land b \in S) \land (f (x) \in a \land g (x) \in b \land a \cap b = \emptyset))) \to g \in (R Cn S)$
65	19	ad2antrr	$⊢ ((((R \in Top \land S \in Haus) \land (f \in (R Cn S) \land g \in (R Cn S))) \land x \in ⋃ R) \land ((a \in S \land b \in S) \land (f (x) \in a \land g (x) \in b \land a \cap b = \emptyset))) \to g Fn ⋃ R$
66		fnsnfv	$⊢ (g Fn ⋃ R \land x \in ⋃ R) \to \{g (x)\} = g [\{x\}]$
67	65 38 66	syl2anc	$⊢ ((((R \in Top \land S \in Haus) \land (f \in (R Cn S) \land g \in (R Cn S))) \land x \in ⋃ R) \land ((a \in S \land b \in S) \land (f (x) \in a \land g (x) \in b \land a \cap b = \emptyset))) \to \{g (x)\} = g [\{x\}]$
68		simprr2	$⊢ ((((R \in Top \land S \in Haus) \land (f \in (R Cn S) \land g \in (R Cn S))) \land x \in ⋃ R) \land ((a \in S \land b \in S) \land (f (x) \in a \land g (x) \in b \land a \cap b = \emptyset))) \to g (x) \in b$
69	68	snssd	$⊢ ((((R \in Top \land S \in Haus) \land (f \in (R Cn S) \land g \in (R Cn S))) \land x \in ⋃ R) \land ((a \in S \land b \in S) \land (f (x) \in a \land g (x) \in b \land a \cap b = \emptyset))) \to \{g (x)\} \subseteq b$
70	67 69	eqsstrrd	$⊢ ((((R \in Top \land S \in Haus) \land (f \in (R Cn S) \land g \in (R Cn S))) \land x \in ⋃ R) \land ((a \in S \land b \in S) \land (f (x) \in a \land g (x) \in b \land a \cap b = \emptyset))) \to g [\{x\}] \subseteq b$
71	63 64 70	elrabd	$⊢ ((((R \in Top \land S \in Haus) \land (f \in (R Cn S) \land g \in (R Cn S))) \land x \in ⋃ R) \land ((a \in S \land b \in S) \land (f (x) \in a \land g (x) \in b \land a \cap b = \emptyset))) \to g \in \{h \in (R Cn S) \| h [\{x\}] \subseteq b\}$
72		inrab	$⊢ \{h \in (R Cn S) \| h [\{x\}] \subseteq a\} \cap \{h \in (R Cn S) \| h [\{x\}] \subseteq b\} = \{h \in (R Cn S) \| (h [\{x\}] \subseteq a \land h [\{x\}] \subseteq b)\}$
73		simpllr	$⊢ (((((R \in Top \land S \in Haus) \land (f \in (R Cn S) \land g \in (R Cn S))) \land x \in ⋃ R) \land ((a \in S \land b \in S) \land (f (x) \in a \land g (x) \in b \land a \cap b = \emptyset))) \land h \in (R Cn S)) \to x \in ⋃ R$
74	11 12	cnf	$⊢ h \in (R Cn S) \to h : ⋃ R ⟶ ⋃ S$
75	74	fdmd	$⊢ h \in (R Cn S) \to dom h = ⋃ R$
76	75	adantl	$⊢ (((((R \in Top \land S \in Haus) \land (f \in (R Cn S) \land g \in (R Cn S))) \land x \in ⋃ R) \land ((a \in S \land b \in S) \land (f (x) \in a \land g (x) \in b \land a \cap b = \emptyset))) \land h \in (R Cn S)) \to dom h = ⋃ R$
77	73 76	eleqtrrd	$⊢ (((((R \in Top \land S \in Haus) \land (f \in (R Cn S) \land g \in (R Cn S))) \land x \in ⋃ R) \land ((a \in S \land b \in S) \land (f (x) \in a \land g (x) \in b \land a \cap b = \emptyset))) \land h \in (R Cn S)) \to x \in dom h$
78		simprr3	$⊢ ((((R \in Top \land S \in Haus) \land (f \in (R Cn S) \land g \in (R Cn S))) \land x \in ⋃ R) \land ((a \in S \land b \in S) \land (f (x) \in a \land g (x) \in b \land a \cap b = \emptyset))) \to a \cap b = \emptyset$
79	78	adantr	$⊢ (((((R \in Top \land S \in Haus) \land (f \in (R Cn S) \land g \in (R Cn S))) \land x \in ⋃ R) \land ((a \in S \land b \in S) \land (f (x) \in a \land g (x) \in b \land a \cap b = \emptyset))) \land h \in (R Cn S)) \to a \cap b = \emptyset$
80		sseq0	$⊢ (h [\{x\}] \subseteq a \cap b \land a \cap b = \emptyset) \to h [\{x\}] = \emptyset$
81	80	expcom	$⊢ a \cap b = \emptyset \to (h [\{x\}] \subseteq a \cap b \to h [\{x\}] = \emptyset)$
82	79 81	syl	$⊢ (((((R \in Top \land S \in Haus) \land (f \in (R Cn S) \land g \in (R Cn S))) \land x \in ⋃ R) \land ((a \in S \land b \in S) \land (f (x) \in a \land g (x) \in b \land a \cap b = \emptyset))) \land h \in (R Cn S)) \to (h [\{x\}] \subseteq a \cap b \to h [\{x\}] = \emptyset)$
83		imadisj	$⊢ h [\{x\}] = \emptyset \leftrightarrow dom h \cap \{x\} = \emptyset$
84		disjsn	$⊢ dom h \cap \{x\} = \emptyset \leftrightarrow \neg x \in dom h$
85	83 84	bitri	$⊢ h [\{x\}] = \emptyset \leftrightarrow \neg x \in dom h$
86	82 85	syl6ib	$⊢ (((((R \in Top \land S \in Haus) \land (f \in (R Cn S) \land g \in (R Cn S))) \land x \in ⋃ R) \land ((a \in S \land b \in S) \land (f (x) \in a \land g (x) \in b \land a \cap b = \emptyset))) \land h \in (R Cn S)) \to (h [\{x\}] \subseteq a \cap b \to \neg x \in dom h)$
87	77 86	mt2d	$⊢ (((((R \in Top \land S \in Haus) \land (f \in (R Cn S) \land g \in (R Cn S))) \land x \in ⋃ R) \land ((a \in S \land b \in S) \land (f (x) \in a \land g (x) \in b \land a \cap b = \emptyset))) \land h \in (R Cn S)) \to \neg h [\{x\}] \subseteq a \cap b$
88		ssin	$⊢ (h [\{x\}] \subseteq a \land h [\{x\}] \subseteq b) \leftrightarrow h [\{x\}] \subseteq a \cap b$
89	87 88	sylnibr	$⊢ (((((R \in Top \land S \in Haus) \land (f \in (R Cn S) \land g \in (R Cn S))) \land x \in ⋃ R) \land ((a \in S \land b \in S) \land (f (x) \in a \land g (x) \in b \land a \cap b = \emptyset))) \land h \in (R Cn S)) \to \neg (h [\{x\}] \subseteq a \land h [\{x\}] \subseteq b)$
90	89	ralrimiva	$⊢ ((((R \in Top \land S \in Haus) \land (f \in (R Cn S) \land g \in (R Cn S))) \land x \in ⋃ R) \land ((a \in S \land b \in S) \land (f (x) \in a \land g (x) \in b \land a \cap b = \emptyset))) \to \forall h \in (R Cn S) \neg (h [\{x\}] \subseteq a \land h [\{x\}] \subseteq b)$
91		rabeq0	$⊢ \{h \in (R Cn S) \| (h [\{x\}] \subseteq a \land h [\{x\}] \subseteq b)\} = \emptyset \leftrightarrow \forall h \in (R Cn S) \neg (h [\{x\}] \subseteq a \land h [\{x\}] \subseteq b)$
92	90 91	sylibr	$⊢ ((((R \in Top \land S \in Haus) \land (f \in (R Cn S) \land g \in (R Cn S))) \land x \in ⋃ R) \land ((a \in S \land b \in S) \land (f (x) \in a \land g (x) \in b \land a \cap b = \emptyset))) \to \{h \in (R Cn S) \| (h [\{x\}] \subseteq a \land h [\{x\}] \subseteq b)\} = \emptyset$
93	72 92	syl5eq	$⊢ ((((R \in Top \land S \in Haus) \land (f \in (R Cn S) \land g \in (R Cn S))) \land x \in ⋃ R) \land ((a \in S \land b \in S) \land (f (x) \in a \land g (x) \in b \land a \cap b = \emptyset))) \to \{h \in (R Cn S) \| h [\{x\}] \subseteq a\} \cap \{h \in (R Cn S) \| h [\{x\}] \subseteq b\} = \emptyset$
94		eleq2	$⊢ u = \{h \in (R Cn S) \| h [\{x\}] \subseteq a\} \to (f \in u \leftrightarrow f \in \{h \in (R Cn S) \| h [\{x\}] \subseteq a\})$
95		ineq1	$⊢ u = \{h \in (R Cn S) \| h [\{x\}] \subseteq a\} \to u \cap v = \{h \in (R Cn S) \| h [\{x\}] \subseteq a\} \cap v$
96	95	eqeq1d	$⊢ u = \{h \in (R Cn S) \| h [\{x\}] \subseteq a\} \to (u \cap v = \emptyset \leftrightarrow \{h \in (R Cn S) \| h [\{x\}] \subseteq a\} \cap v = \emptyset)$
97	94 96	3anbi13d	$⊢ u = \{h \in (R Cn S) \| h [\{x\}] \subseteq a\} \to ((f \in u \land g \in v \land u \cap v = \emptyset) \leftrightarrow (f \in \{h \in (R Cn S) \| h [\{x\}] \subseteq a\} \land g \in v \land \{h \in (R Cn S) \| h [\{x\}] \subseteq a\} \cap v = \emptyset))$
98		eleq2	$⊢ v = \{h \in (R Cn S) \| h [\{x\}] \subseteq b\} \to (g \in v \leftrightarrow g \in \{h \in (R Cn S) \| h [\{x\}] \subseteq b\})$
99		ineq2	$⊢ v = \{h \in (R Cn S) \| h [\{x\}] \subseteq b\} \to \{h \in (R Cn S) \| h [\{x\}] \subseteq a\} \cap v = \{h \in (R Cn S) \| h [\{x\}] \subseteq a\} \cap \{h \in (R Cn S) \| h [\{x\}] \subseteq b\}$
100	99	eqeq1d	$⊢ v = \{h \in (R Cn S) \| h [\{x\}] \subseteq b\} \to (\{h \in (R Cn S) \| h [\{x\}] \subseteq a\} \cap v = \emptyset \leftrightarrow \{h \in (R Cn S) \| h [\{x\}] \subseteq a\} \cap \{h \in (R Cn S) \| h [\{x\}] \subseteq b\} = \emptyset)$
101	98 100	3anbi23d	$⊢ v = \{h \in (R Cn S) \| h [\{x\}] \subseteq b\} \to ((f \in \{h \in (R Cn S) \| h [\{x\}] \subseteq a\} \land g \in v \land \{h \in (R Cn S) \| h [\{x\}] \subseteq a\} \cap v = \emptyset) \leftrightarrow (f \in \{h \in (R Cn S) \| h [\{x\}] \subseteq a\} \land g \in \{h \in (R Cn S) \| h [\{x\}] \subseteq b\} \land \{h \in (R Cn S) \| h [\{x\}] \subseteq a\} \cap \{h \in (R Cn S) \| h [\{x\}] \subseteq b\} = \emptyset))$
102	97 101	rspc2ev	$⊢ (\{h \in (R Cn S) \| h [\{x\}] \subseteq a\} \in (S^_{ko} R) \land \{h \in (R Cn S) \| h [\{x\}] \subseteq b\} \in (S^_{ko} R) \land (f \in \{h \in (R Cn S) \| h [\{x\}] \subseteq a\} \land g \in \{h \in (R Cn S) \| h [\{x\}] \subseteq b\} \land \{h \in (R Cn S) \| h [\{x\}] \subseteq a\} \cap \{h \in (R Cn S) \| h [\{x\}] \subseteq b\} = \emptyset)) \to \exists u \in (S^_{ko} R) \exists v \in (S^_{ko} R) (f \in u \land g \in v \land u \cap v = \emptyset)$
103	49 51 61 71 93 102	syl113anc	$⊢ ((((R \in Top \land S \in Haus) \land (f \in (R Cn S) \land g \in (R Cn S))) \land x \in ⋃ R) \land ((a \in S \land b \in S) \land (f (x) \in a \land g (x) \in b \land a \cap b = \emptyset))) \to \exists u \in (S^_{ko} R) \exists v \in (S^_{ko} R) (f \in u \land g \in v \land u \cap v = \emptyset)$
104	103	expr	$⊢ ((((R \in Top \land S \in Haus) \land (f \in (R Cn S) \land g \in (R Cn S))) \land x \in ⋃ R) \land (a \in S \land b \in S)) \to ((f (x) \in a \land g (x) \in b \land a \cap b = \emptyset) \to \exists u \in (S^_{ko} R) \exists v \in (S^_{ko} R) (f \in u \land g \in v \land u \cap v = \emptyset))$
105	104	rexlimdvva	$⊢ (((R \in Top \land S \in Haus) \land (f \in (R Cn S) \land g \in (R Cn S))) \land x \in ⋃ R) \to (\exists a \in S \exists b \in S (f (x) \in a \land g (x) \in b \land a \cap b = \emptyset) \to \exists u \in (S^_{ko} R) \exists v \in (S^_{ko} R) (f \in u \land g \in v \land u \cap v = \emptyset))$
106	35 105	syld	$⊢ (((R \in Top \land S \in Haus) \land (f \in (R Cn S) \land g \in (R Cn S))) \land x \in ⋃ R) \to (\neg f (x) = g (x) \to \exists u \in (S^_{ko} R) \exists v \in (S^_{ko} R) (f \in u \land g \in v \land u \cap v = \emptyset))$
107	106	rexlimdva	$⊢ ((R \in Top \land S \in Haus) \land (f \in (R Cn S) \land g \in (R Cn S))) \to (\exists x \in ⋃ R \neg f (x) = g (x) \to \exists u \in (S^_{ko} R) \exists v \in (S^_{ko} R) (f \in u \land g \in v \land u \cap v = \emptyset))$
108	23 107	syl5bir	$⊢ ((R \in Top \land S \in Haus) \land (f \in (R Cn S) \land g \in (R Cn S))) \to (\neg \forall x \in ⋃ R f (x) = g (x) \to \exists u \in (S^_{ko} R) \exists v \in (S^_{ko} R) (f \in u \land g \in v \land u \cap v = \emptyset))$
109	22 108	sylbid	$⊢ ((R \in Top \land S \in Haus) \land (f \in (R Cn S) \land g \in (R Cn S))) \to (f \neq g \to \exists u \in (S^_{ko} R) \exists v \in (S^_{ko} R) (f \in u \land g \in v \land u \cap v = \emptyset))$
110	109	ex	$⊢ (R \in Top \land S \in Haus) \to ((f \in (R Cn S) \land g \in (R Cn S)) \to (f \neq g \to \exists u \in (S^_{ko} R) \exists v \in (S^_{ko} R) (f \in u \land g \in v \land u \cap v = \emptyset)))$
111	9 110	sylbird	$⊢ (R \in Top \land S \in Haus) \to ((f \in ⋃ (S^_{ko} R) \land g \in ⋃ (S^_{ko} R)) \to (f \neq g \to \exists u \in (S^_{ko} R) \exists v \in (S^_{ko} R) (f \in u \land g \in v \land u \cap v = \emptyset)))$
112	111	ralrimivv	$⊢ (R \in Top \land S \in Haus) \to \forall f \in ⋃ (S^_{ko} R) \forall g \in ⋃ (S^_{ko} R) (f \neq g \to \exists u \in (S^_{ko} R) \exists v \in (S^_{ko} R) (f \in u \land g \in v \land u \cap v = \emptyset))$
113		eqid	$⊢ ⋃ (S^_{ko} R) = ⋃ (S^_{ko} R)$
114	113	ishaus	$⊢ S^_{ko} R \in Haus \leftrightarrow (S^_{ko} R \in Top \land \forall f \in ⋃ (S^_{ko} R) \forall g \in ⋃ (S^_{ko} R) (f \neq g \to \exists u \in (S^_{ko} R) \exists v \in (S^_{ko} R) (f \in u \land g \in v \land u \cap v = \emptyset)))$
115	3 112 114	sylanbrc	$⊢ (R \in Top \land S \in Haus) \to S^_{ko} R \in Haus$

Metamath Proof Explorer

Theorem xkohaus

Proof