Theorem xkohaus 23601

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.)

Assertion

Ref	Expression
xkohaus	⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) → (𝑆 ↑ko 𝑅) ∈ Haus)

Proof of Theorem xkohaus

Dummy variables 𝑎 𝑏 𝑓 𝑔 ℎ 𝑢 𝑣 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		haustop 23279	. . 3 ⊢ (𝑆 ∈ Haus → 𝑆 ∈ Top)
2		xkotop 23536	. . 3 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑆 ↑ko 𝑅) ∈ Top)
3	1, 2	sylan2 594	. 2 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) → (𝑆 ↑ko 𝑅) ∈ Top)
4		eqid 2737	. . . . . . . 8 ⊢ (𝑆 ↑ko 𝑅) = (𝑆 ↑ko 𝑅)
5	4	xkouni 23547	. . . . . . 7 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 Cn 𝑆) = ∪ (𝑆 ↑ko 𝑅))
6	1, 5	sylan2 594	. . . . . 6 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) → (𝑅 Cn 𝑆) = ∪ (𝑆 ↑ko 𝑅))
7	6	eleq2d 2823	. . . . 5 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) → (𝑓 ∈ (𝑅 Cn 𝑆) ↔ 𝑓 ∈ ∪ (𝑆 ↑ko 𝑅)))
8	6	eleq2d 2823	. . . . 5 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) → (𝑔 ∈ (𝑅 Cn 𝑆) ↔ 𝑔 ∈ ∪ (𝑆 ↑ko 𝑅)))
9	7, 8	anbi12d 633	. . . 4 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) → ((𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆)) ↔ (𝑓 ∈ ∪ (𝑆 ↑ko 𝑅) ∧ 𝑔 ∈ ∪ (𝑆 ↑ko 𝑅))))
10		simprl 771	. . . . . . . . . 10 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) → 𝑓 ∈ (𝑅 Cn 𝑆))
11		eqid 2737	. . . . . . . . . . 11 ⊢ ∪ 𝑅 = ∪ 𝑅
12		eqid 2737	. . . . . . . . . . 11 ⊢ ∪ 𝑆 = ∪ 𝑆
13	11, 12	cnf 23194	. . . . . . . . . 10 ⊢ (𝑓 ∈ (𝑅 Cn 𝑆) → 𝑓:∪ 𝑅⟶∪ 𝑆)
14	10, 13	syl 17	. . . . . . . . 9 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) → 𝑓:∪ 𝑅⟶∪ 𝑆)
15	14	ffnd 6664	. . . . . . . 8 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) → 𝑓 Fn ∪ 𝑅)
16		simprr 773	. . . . . . . . . 10 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) → 𝑔 ∈ (𝑅 Cn 𝑆))
17	11, 12	cnf 23194	. . . . . . . . . 10 ⊢ (𝑔 ∈ (𝑅 Cn 𝑆) → 𝑔:∪ 𝑅⟶∪ 𝑆)
18	16, 17	syl 17	. . . . . . . . 9 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) → 𝑔:∪ 𝑅⟶∪ 𝑆)
19	18	ffnd 6664	. . . . . . . 8 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) → 𝑔 Fn ∪ 𝑅)
20		eqfnfv 6978	. . . . . . . 8 ⊢ ((𝑓 Fn ∪ 𝑅 ∧ 𝑔 Fn ∪ 𝑅) → (𝑓 = 𝑔 ↔ ∀𝑥 ∈ ∪ 𝑅(𝑓‘𝑥) = (𝑔‘𝑥)))
21	15, 19, 20	syl2anc 585	. . . . . . 7 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) → (𝑓 = 𝑔 ↔ ∀𝑥 ∈ ∪ 𝑅(𝑓‘𝑥) = (𝑔‘𝑥)))
22	21	necon3abid 2969	. . . . . 6 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) → (𝑓 ≠ 𝑔 ↔ ¬ ∀𝑥 ∈ ∪ 𝑅(𝑓‘𝑥) = (𝑔‘𝑥)))
23		rexnal 3089	. . . . . . 7 ⊢ (∃𝑥 ∈ ∪ 𝑅 ¬ (𝑓‘𝑥) = (𝑔‘𝑥) ↔ ¬ ∀𝑥 ∈ ∪ 𝑅(𝑓‘𝑥) = (𝑔‘𝑥))
24		df-ne 2934	. . . . . . . . . 10 ⊢ ((𝑓‘𝑥) ≠ (𝑔‘𝑥) ↔ ¬ (𝑓‘𝑥) = (𝑔‘𝑥))
25		simpllr 776	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ (𝑥 ∈ ∪ 𝑅 ∧ (𝑓‘𝑥) ≠ (𝑔‘𝑥))) → 𝑆 ∈ Haus)
26	14	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ (𝑥 ∈ ∪ 𝑅 ∧ (𝑓‘𝑥) ≠ (𝑔‘𝑥))) → 𝑓:∪ 𝑅⟶∪ 𝑆)
27		simprl 771	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ (𝑥 ∈ ∪ 𝑅 ∧ (𝑓‘𝑥) ≠ (𝑔‘𝑥))) → 𝑥 ∈ ∪ 𝑅)
28	26, 27	ffvelcdmd 7032	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ (𝑥 ∈ ∪ 𝑅 ∧ (𝑓‘𝑥) ≠ (𝑔‘𝑥))) → (𝑓‘𝑥) ∈ ∪ 𝑆)
29	18	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ (𝑥 ∈ ∪ 𝑅 ∧ (𝑓‘𝑥) ≠ (𝑔‘𝑥))) → 𝑔:∪ 𝑅⟶∪ 𝑆)
30	29, 27	ffvelcdmd 7032	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ (𝑥 ∈ ∪ 𝑅 ∧ (𝑓‘𝑥) ≠ (𝑔‘𝑥))) → (𝑔‘𝑥) ∈ ∪ 𝑆)
31		simprr 773	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ (𝑥 ∈ ∪ 𝑅 ∧ (𝑓‘𝑥) ≠ (𝑔‘𝑥))) → (𝑓‘𝑥) ≠ (𝑔‘𝑥))
32	12	hausnei 23276	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ Haus ∧ ((𝑓‘𝑥) ∈ ∪ 𝑆 ∧ (𝑔‘𝑥) ∈ ∪ 𝑆 ∧ (𝑓‘𝑥) ≠ (𝑔‘𝑥))) → ∃𝑎 ∈ 𝑆 ∃𝑏 ∈ 𝑆 ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))
33	25, 28, 30, 31, 32	syl13anc 1375	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ (𝑥 ∈ ∪ 𝑅 ∧ (𝑓‘𝑥) ≠ (𝑔‘𝑥))) → ∃𝑎 ∈ 𝑆 ∃𝑏 ∈ 𝑆 ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))
34	33	expr 456	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) → ((𝑓‘𝑥) ≠ (𝑔‘𝑥) → ∃𝑎 ∈ 𝑆 ∃𝑏 ∈ 𝑆 ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅)))
35	24, 34	biimtrrid 243	. . . . . . . . 9 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) → (¬ (𝑓‘𝑥) = (𝑔‘𝑥) → ∃𝑎 ∈ 𝑆 ∃𝑏 ∈ 𝑆 ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅)))
36		simp-4l 783	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → 𝑅 ∈ Top)
37	1	ad4antlr 734	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → 𝑆 ∈ Top)
38		simplr 769	. . . . . . . . . . . . . 14 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → 𝑥 ∈ ∪ 𝑅)
39	38	snssd 4766	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → {𝑥} ⊆ ∪ 𝑅)
40		toptopon2 22866	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 ∈ Top ↔ 𝑅 ∈ (TopOn‘∪ 𝑅))
41	36, 40	sylib 218	. . . . . . . . . . . . . . 15 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → 𝑅 ∈ (TopOn‘∪ 𝑅))
42		restsn2 23119	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ (TopOn‘∪ 𝑅) ∧ 𝑥 ∈ ∪ 𝑅) → (𝑅 ↾t {𝑥}) = 𝒫 {𝑥})
43	41, 38, 42	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → (𝑅 ↾t {𝑥}) = 𝒫 {𝑥})
44		snfi 8984	. . . . . . . . . . . . . . 15 ⊢ {𝑥} ∈ Fin
45		discmp 23346	. . . . . . . . . . . . . . 15 ⊢ ({𝑥} ∈ Fin ↔ 𝒫 {𝑥} ∈ Comp)
46	44, 45	mpbi 230	. . . . . . . . . . . . . 14 ⊢ 𝒫 {𝑥} ∈ Comp
47	43, 46	eqeltrdi 2845	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → (𝑅 ↾t {𝑥}) ∈ Comp)
48		simprll 779	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → 𝑎 ∈ 𝑆)
49	11, 36, 37, 39, 47, 48	xkoopn 23537	. . . . . . . . . . . 12 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎} ∈ (𝑆 ↑ko 𝑅))
50		simprlr 780	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → 𝑏 ∈ 𝑆)
51	11, 36, 37, 39, 47, 50	xkoopn 23537	. . . . . . . . . . . 12 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑏} ∈ (𝑆 ↑ko 𝑅))
52		imaeq1 6015	. . . . . . . . . . . . . 14 ⊢ (ℎ = 𝑓 → (ℎ “ {𝑥}) = (𝑓 “ {𝑥}))
53	52	sseq1d 3966	. . . . . . . . . . . . 13 ⊢ (ℎ = 𝑓 → ((ℎ “ {𝑥}) ⊆ 𝑎 ↔ (𝑓 “ {𝑥}) ⊆ 𝑎))
54	10	ad2antrr 727	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → 𝑓 ∈ (𝑅 Cn 𝑆))
55	15	ad2antrr 727	. . . . . . . . . . . . . . 15 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → 𝑓 Fn ∪ 𝑅)
56		fnsnfv 6914	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 Fn ∪ 𝑅 ∧ 𝑥 ∈ ∪ 𝑅) → {(𝑓‘𝑥)} = (𝑓 “ {𝑥}))
57	55, 38, 56	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → {(𝑓‘𝑥)} = (𝑓 “ {𝑥}))
58		simprr1 1223	. . . . . . . . . . . . . . 15 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → (𝑓‘𝑥) ∈ 𝑎)
59	58	snssd 4766	. . . . . . . . . . . . . 14 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → {(𝑓‘𝑥)} ⊆ 𝑎)
60	57, 59	eqsstrrd 3970	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → (𝑓 “ {𝑥}) ⊆ 𝑎)
61	53, 54, 60	elrabd 3649	. . . . . . . . . . . 12 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → 𝑓 ∈ {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎})
62		imaeq1 6015	. . . . . . . . . . . . . 14 ⊢ (ℎ = 𝑔 → (ℎ “ {𝑥}) = (𝑔 “ {𝑥}))
63	62	sseq1d 3966	. . . . . . . . . . . . 13 ⊢ (ℎ = 𝑔 → ((ℎ “ {𝑥}) ⊆ 𝑏 ↔ (𝑔 “ {𝑥}) ⊆ 𝑏))
64	16	ad2antrr 727	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → 𝑔 ∈ (𝑅 Cn 𝑆))
65	19	ad2antrr 727	. . . . . . . . . . . . . . 15 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → 𝑔 Fn ∪ 𝑅)
66		fnsnfv 6914	. . . . . . . . . . . . . . 15 ⊢ ((𝑔 Fn ∪ 𝑅 ∧ 𝑥 ∈ ∪ 𝑅) → {(𝑔‘𝑥)} = (𝑔 “ {𝑥}))
67	65, 38, 66	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → {(𝑔‘𝑥)} = (𝑔 “ {𝑥}))
68		simprr2 1224	. . . . . . . . . . . . . . 15 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → (𝑔‘𝑥) ∈ 𝑏)
69	68	snssd 4766	. . . . . . . . . . . . . 14 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → {(𝑔‘𝑥)} ⊆ 𝑏)
70	67, 69	eqsstrrd 3970	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → (𝑔 “ {𝑥}) ⊆ 𝑏)
71	63, 64, 70	elrabd 3649	. . . . . . . . . . . 12 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → 𝑔 ∈ {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑏})
72		inrab 4269	. . . . . . . . . . . . 13 ⊢ ({ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎} ∩ {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑏}) = {ℎ ∈ (𝑅 Cn 𝑆) ∣ ((ℎ “ {𝑥}) ⊆ 𝑎 ∧ (ℎ “ {𝑥}) ⊆ 𝑏)}
73		simpllr 776	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) ∧ ℎ ∈ (𝑅 Cn 𝑆)) → 𝑥 ∈ ∪ 𝑅)
74	11, 12	cnf 23194	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ℎ ∈ (𝑅 Cn 𝑆) → ℎ:∪ 𝑅⟶∪ 𝑆)
75	74	fdmd 6673	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℎ ∈ (𝑅 Cn 𝑆) → dom ℎ = ∪ 𝑅)
76	75	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) ∧ ℎ ∈ (𝑅 Cn 𝑆)) → dom ℎ = ∪ 𝑅)
77	73, 76	eleqtrrd 2840	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) ∧ ℎ ∈ (𝑅 Cn 𝑆)) → 𝑥 ∈ dom ℎ)
78		simprr3 1225	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → (𝑎 ∩ 𝑏) = ∅)
79	78	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) ∧ ℎ ∈ (𝑅 Cn 𝑆)) → (𝑎 ∩ 𝑏) = ∅)
80		sseq0 4356	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℎ “ {𝑥}) ⊆ (𝑎 ∩ 𝑏) ∧ (𝑎 ∩ 𝑏) = ∅) → (ℎ “ {𝑥}) = ∅)
81	80	expcom 413	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ∩ 𝑏) = ∅ → ((ℎ “ {𝑥}) ⊆ (𝑎 ∩ 𝑏) → (ℎ “ {𝑥}) = ∅))
82	79, 81	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) ∧ ℎ ∈ (𝑅 Cn 𝑆)) → ((ℎ “ {𝑥}) ⊆ (𝑎 ∩ 𝑏) → (ℎ “ {𝑥}) = ∅))
83		imadisj 6040	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℎ “ {𝑥}) = ∅ ↔ (dom ℎ ∩ {𝑥}) = ∅)
84		disjsn 4669	. . . . . . . . . . . . . . . . . . 19 ⊢ ((dom ℎ ∩ {𝑥}) = ∅ ↔ ¬ 𝑥 ∈ dom ℎ)
85	83, 84	bitri 275	. . . . . . . . . . . . . . . . . 18 ⊢ ((ℎ “ {𝑥}) = ∅ ↔ ¬ 𝑥 ∈ dom ℎ)
86	82, 85	imbitrdi 251	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) ∧ ℎ ∈ (𝑅 Cn 𝑆)) → ((ℎ “ {𝑥}) ⊆ (𝑎 ∩ 𝑏) → ¬ 𝑥 ∈ dom ℎ))
87	77, 86	mt2d 136	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) ∧ ℎ ∈ (𝑅 Cn 𝑆)) → ¬ (ℎ “ {𝑥}) ⊆ (𝑎 ∩ 𝑏))
88		ssin 4192	. . . . . . . . . . . . . . . 16 ⊢ (((ℎ “ {𝑥}) ⊆ 𝑎 ∧ (ℎ “ {𝑥}) ⊆ 𝑏) ↔ (ℎ “ {𝑥}) ⊆ (𝑎 ∩ 𝑏))
89	87, 88	sylnibr 329	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) ∧ ℎ ∈ (𝑅 Cn 𝑆)) → ¬ ((ℎ “ {𝑥}) ⊆ 𝑎 ∧ (ℎ “ {𝑥}) ⊆ 𝑏))
90	89	ralrimiva 3129	. . . . . . . . . . . . . 14 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → ∀ℎ ∈ (𝑅 Cn 𝑆) ¬ ((ℎ “ {𝑥}) ⊆ 𝑎 ∧ (ℎ “ {𝑥}) ⊆ 𝑏))
91		rabeq0 4341	. . . . . . . . . . . . . 14 ⊢ ({ℎ ∈ (𝑅 Cn 𝑆) ∣ ((ℎ “ {𝑥}) ⊆ 𝑎 ∧ (ℎ “ {𝑥}) ⊆ 𝑏)} = ∅ ↔ ∀ℎ ∈ (𝑅 Cn 𝑆) ¬ ((ℎ “ {𝑥}) ⊆ 𝑎 ∧ (ℎ “ {𝑥}) ⊆ 𝑏))
92	90, 91	sylibr 234	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → {ℎ ∈ (𝑅 Cn 𝑆) ∣ ((ℎ “ {𝑥}) ⊆ 𝑎 ∧ (ℎ “ {𝑥}) ⊆ 𝑏)} = ∅)
93	72, 92	eqtrid 2784	. . . . . . . . . . . 12 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → ({ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎} ∩ {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑏}) = ∅)
94		eleq2 2826	. . . . . . . . . . . . . 14 ⊢ (𝑢 = {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎} → (𝑓 ∈ 𝑢 ↔ 𝑓 ∈ {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎}))
95		ineq1 4166	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎} → (𝑢 ∩ 𝑣) = ({ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎} ∩ 𝑣))
96	95	eqeq1d 2739	. . . . . . . . . . . . . 14 ⊢ (𝑢 = {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎} → ((𝑢 ∩ 𝑣) = ∅ ↔ ({ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎} ∩ 𝑣) = ∅))
97	94, 96	3anbi13d 1441	. . . . . . . . . . . . 13 ⊢ (𝑢 = {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎} → ((𝑓 ∈ 𝑢 ∧ 𝑔 ∈ 𝑣 ∧ (𝑢 ∩ 𝑣) = ∅) ↔ (𝑓 ∈ {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎} ∧ 𝑔 ∈ 𝑣 ∧ ({ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎} ∩ 𝑣) = ∅)))
98		eleq2 2826	. . . . . . . . . . . . . 14 ⊢ (𝑣 = {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑏} → (𝑔 ∈ 𝑣 ↔ 𝑔 ∈ {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑏}))
99		ineq2 4167	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑏} → ({ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎} ∩ 𝑣) = ({ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎} ∩ {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑏}))
100	99	eqeq1d 2739	. . . . . . . . . . . . . 14 ⊢ (𝑣 = {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑏} → (({ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎} ∩ 𝑣) = ∅ ↔ ({ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎} ∩ {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑏}) = ∅))
101	98, 100	3anbi23d 1442	. . . . . . . . . . . . 13 ⊢ (𝑣 = {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑏} → ((𝑓 ∈ {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎} ∧ 𝑔 ∈ 𝑣 ∧ ({ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎} ∩ 𝑣) = ∅) ↔ (𝑓 ∈ {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎} ∧ 𝑔 ∈ {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑏} ∧ ({ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎} ∩ {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑏}) = ∅)))
102	97, 101	rspc2ev 3590	. . . . . . . . . . . 12 ⊢ (({ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎} ∈ (𝑆 ↑ko 𝑅) ∧ {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑏} ∈ (𝑆 ↑ko 𝑅) ∧ (𝑓 ∈ {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎} ∧ 𝑔 ∈ {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑏} ∧ ({ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎} ∩ {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑏}) = ∅)) → ∃𝑢 ∈ (𝑆 ↑ko 𝑅)∃𝑣 ∈ (𝑆 ↑ko 𝑅)(𝑓 ∈ 𝑢 ∧ 𝑔 ∈ 𝑣 ∧ (𝑢 ∩ 𝑣) = ∅))
103	49, 51, 61, 71, 93, 102	syl113anc 1385	. . . . . . . . . . 11 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → ∃𝑢 ∈ (𝑆 ↑ko 𝑅)∃𝑣 ∈ (𝑆 ↑ko 𝑅)(𝑓 ∈ 𝑢 ∧ 𝑔 ∈ 𝑣 ∧ (𝑢 ∩ 𝑣) = ∅))
104	103	expr 456	. . . . . . . . . 10 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ (𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆)) → (((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅) → ∃𝑢 ∈ (𝑆 ↑ko 𝑅)∃𝑣 ∈ (𝑆 ↑ko 𝑅)(𝑓 ∈ 𝑢 ∧ 𝑔 ∈ 𝑣 ∧ (𝑢 ∩ 𝑣) = ∅)))
105	104	rexlimdvva 3194	. . . . . . . . 9 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) → (∃𝑎 ∈ 𝑆 ∃𝑏 ∈ 𝑆 ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅) → ∃𝑢 ∈ (𝑆 ↑ko 𝑅)∃𝑣 ∈ (𝑆 ↑ko 𝑅)(𝑓 ∈ 𝑢 ∧ 𝑔 ∈ 𝑣 ∧ (𝑢 ∩ 𝑣) = ∅)))
106	35, 105	syld 47	. . . . . . . 8 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) → (¬ (𝑓‘𝑥) = (𝑔‘𝑥) → ∃𝑢 ∈ (𝑆 ↑ko 𝑅)∃𝑣 ∈ (𝑆 ↑ko 𝑅)(𝑓 ∈ 𝑢 ∧ 𝑔 ∈ 𝑣 ∧ (𝑢 ∩ 𝑣) = ∅)))
107	106	rexlimdva 3138	. . . . . . 7 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) → (∃𝑥 ∈ ∪ 𝑅 ¬ (𝑓‘𝑥) = (𝑔‘𝑥) → ∃𝑢 ∈ (𝑆 ↑ko 𝑅)∃𝑣 ∈ (𝑆 ↑ko 𝑅)(𝑓 ∈ 𝑢 ∧ 𝑔 ∈ 𝑣 ∧ (𝑢 ∩ 𝑣) = ∅)))
108	23, 107	biimtrrid 243	. . . . . 6 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) → (¬ ∀𝑥 ∈ ∪ 𝑅(𝑓‘𝑥) = (𝑔‘𝑥) → ∃𝑢 ∈ (𝑆 ↑ko 𝑅)∃𝑣 ∈ (𝑆 ↑ko 𝑅)(𝑓 ∈ 𝑢 ∧ 𝑔 ∈ 𝑣 ∧ (𝑢 ∩ 𝑣) = ∅)))
109	22, 108	sylbid 240	. . . . 5 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) → (𝑓 ≠ 𝑔 → ∃𝑢 ∈ (𝑆 ↑ko 𝑅)∃𝑣 ∈ (𝑆 ↑ko 𝑅)(𝑓 ∈ 𝑢 ∧ 𝑔 ∈ 𝑣 ∧ (𝑢 ∩ 𝑣) = ∅)))
110	109	ex 412	. . . 4 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) → ((𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆)) → (𝑓 ≠ 𝑔 → ∃𝑢 ∈ (𝑆 ↑ko 𝑅)∃𝑣 ∈ (𝑆 ↑ko 𝑅)(𝑓 ∈ 𝑢 ∧ 𝑔 ∈ 𝑣 ∧ (𝑢 ∩ 𝑣) = ∅))))
111	9, 110	sylbird 260	. . 3 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) → ((𝑓 ∈ ∪ (𝑆 ↑ko 𝑅) ∧ 𝑔 ∈ ∪ (𝑆 ↑ko 𝑅)) → (𝑓 ≠ 𝑔 → ∃𝑢 ∈ (𝑆 ↑ko 𝑅)∃𝑣 ∈ (𝑆 ↑ko 𝑅)(𝑓 ∈ 𝑢 ∧ 𝑔 ∈ 𝑣 ∧ (𝑢 ∩ 𝑣) = ∅))))
112	111	ralrimivv 3178	. 2 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) → ∀𝑓 ∈ ∪ (𝑆 ↑ko 𝑅)∀𝑔 ∈ ∪ (𝑆 ↑ko 𝑅)(𝑓 ≠ 𝑔 → ∃𝑢 ∈ (𝑆 ↑ko 𝑅)∃𝑣 ∈ (𝑆 ↑ko 𝑅)(𝑓 ∈ 𝑢 ∧ 𝑔 ∈ 𝑣 ∧ (𝑢 ∩ 𝑣) = ∅)))
113		eqid 2737	. . 3 ⊢ ∪ (𝑆 ↑ko 𝑅) = ∪ (𝑆 ↑ko 𝑅)
114	113	ishaus 23270	. 2 ⊢ ((𝑆 ↑ko 𝑅) ∈ Haus ↔ ((𝑆 ↑ko 𝑅) ∈ Top ∧ ∀𝑓 ∈ ∪ (𝑆 ↑ko 𝑅)∀𝑔 ∈ ∪ (𝑆 ↑ko 𝑅)(𝑓 ≠ 𝑔 → ∃𝑢 ∈ (𝑆 ↑ko 𝑅)∃𝑣 ∈ (𝑆 ↑ko 𝑅)(𝑓 ∈ 𝑢 ∧ 𝑔 ∈ 𝑣 ∧ (𝑢 ∩ 𝑣) = ∅))))
115	3, 112, 114	sylanbrc 584	1 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) → (𝑆 ↑ko 𝑅) ∈ Haus)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114   ≠ wne 2933  ∀wral 3052  ∃wrex 3061  {crab 3400   ∩ cin 3901   ⊆ wss 3902  ∅c0 4286  𝒫 cpw 4555  {csn 4581  ∪ cuni 4864  dom cdm 5625   “ cima 5628   Fn wfn 6488  ⟶wf 6489  ‘cfv 6493  (class class class)co 7360  Fincfn 8887   ↾_t crest 17344  Topctop 22841  TopOnctopon 22858   Cn ccn 23172  Hauscha 23256  Compccmp 23334   ↑_ko cxko 23509

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5225  ax-sep 5242  ax-nul 5252  ax-pow 5311  ax-pr 5378  ax-un 7682

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-reu 3352  df-rab 3401  df-v 3443  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4287  df-if 4481  df-pw 4557  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-int 4904  df-iun 4949  df-br 5100  df-opab 5162  df-mpt 5181  df-tr 5207  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-ov 7363  df-oprab 7364  df-mpo 7365  df-om 7811  df-1st 7935  df-2nd 7936  df-1o 8399  df-2o 8400  df-map 8769  df-en 8888  df-dom 8889  df-fin 8891  df-fi 9318  df-rest 17346  df-topgen 17367  df-top 22842  df-topon 22859  df-bases 22894  df-cn 23175  df-haus 23263  df-cmp 23335  df-xko 23511

This theorem is referenced by: (None)