Theorem xkohaus 23999

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 23676	. . 3 ⊢ (𝑆 ∈ Haus → 𝑆 ∈ Top)
2		xkotop 23934	. . 3 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑆 ↑ko 𝑅) ∈ Top)
3	1, 2	sylan2 605	. 2 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) → (𝑆 ↑ko 𝑅) ∈ Top)
4		eqid 2763	. . . . . . . 8 ⊢ (𝑆 ↑ko 𝑅) = (𝑆 ↑ko 𝑅)
5	4	xkouni 23945	. . . . . . 7 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 Cn 𝑆) = ∪ (𝑆 ↑ko 𝑅))
6	1, 5	sylan2 605	. . . . . 6 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) → (𝑅 Cn 𝑆) = ∪ (𝑆 ↑ko 𝑅))
7	6	eleq2d 2850	. . . . 5 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) → (𝑓 ∈ (𝑅 Cn 𝑆) ↔ 𝑓 ∈ ∪ (𝑆 ↑ko 𝑅)))
8	6	eleq2d 2850	. . . . 5 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) → (𝑔 ∈ (𝑅 Cn 𝑆) ↔ 𝑔 ∈ ∪ (𝑆 ↑ko 𝑅)))
9	7, 8	anbi12d 644	. . . 4 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) → ((𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆)) ↔ (𝑓 ∈ ∪ (𝑆 ↑ko 𝑅) ∧ 𝑔 ∈ ∪ (𝑆 ↑ko 𝑅))))
10		simprl 783	. . . . . . . . . 10 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) → 𝑓 ∈ (𝑅 Cn 𝑆))
11		eqid 2763	. . . . . . . . . . 11 ⊢ ∪ 𝑅 = ∪ 𝑅
12		eqid 2763	. . . . . . . . . . 11 ⊢ ∪ 𝑆 = ∪ 𝑆
13	11, 12	cnf 23591	. . . . . . . . . 10 ⊢ (𝑓 ∈ (𝑅 Cn 𝑆) → 𝑓:∪ 𝑅⟶∪ 𝑆)
14	10, 13	syl 18	. . . . . . . . 9 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) → 𝑓:∪ 𝑅⟶∪ 𝑆)
15	14	ffnd 6729	. . . . . . . 8 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) → 𝑓 Fn ∪ 𝑅)
16		simprr 785	. . . . . . . . . 10 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) → 𝑔 ∈ (𝑅 Cn 𝑆))
17	11, 12	cnf 23591	. . . . . . . . . 10 ⊢ (𝑔 ∈ (𝑅 Cn 𝑆) → 𝑔:∪ 𝑅⟶∪ 𝑆)
18	16, 17	syl 18	. . . . . . . . 9 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) → 𝑔:∪ 𝑅⟶∪ 𝑆)
19	18	ffnd 6729	. . . . . . . 8 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) → 𝑔 Fn ∪ 𝑅)
20		eqfnfv 7049	. . . . . . . 8 ⊢ ((𝑓 Fn ∪ 𝑅 ∧ 𝑔 Fn ∪ 𝑅) → (𝑓 = 𝑔 ↔ ∀𝑥 ∈ ∪ 𝑅(𝑓‘𝑥) = (𝑔‘𝑥)))
21	15, 19, 20	syl2anc 596	. . . . . . 7 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) → (𝑓 = 𝑔 ↔ ∀𝑥 ∈ ∪ 𝑅(𝑓‘𝑥) = (𝑔‘𝑥)))
22	21	necon3abid 2995	. . . . . 6 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) → (𝑓 ≠ 𝑔 ↔ ¬ ∀𝑥 ∈ ∪ 𝑅(𝑓‘𝑥) = (𝑔‘𝑥)))
23		rexnal 3118	. . . . . . 7 ⊢ (∃𝑥 ∈ ∪ 𝑅 ¬ (𝑓‘𝑥) = (𝑔‘𝑥) ↔ ¬ ∀𝑥 ∈ ∪ 𝑅(𝑓‘𝑥) = (𝑔‘𝑥))
24		df-ne 2960	. . . . . . . . . 10 ⊢ ((𝑓‘𝑥) ≠ (𝑔‘𝑥) ↔ ¬ (𝑓‘𝑥) = (𝑔‘𝑥))
25		simpllr 788	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ (𝑥 ∈ ∪ 𝑅 ∧ (𝑓‘𝑥) ≠ (𝑔‘𝑥))) → 𝑆 ∈ Haus)
26	14	adantr 486	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ (𝑥 ∈ ∪ 𝑅 ∧ (𝑓‘𝑥) ≠ (𝑔‘𝑥))) → 𝑓:∪ 𝑅⟶∪ 𝑆)
27		simprl 783	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ (𝑥 ∈ ∪ 𝑅 ∧ (𝑓‘𝑥) ≠ (𝑔‘𝑥))) → 𝑥 ∈ ∪ 𝑅)
28	26, 27	ffvelcdmd 7106	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ (𝑥 ∈ ∪ 𝑅 ∧ (𝑓‘𝑥) ≠ (𝑔‘𝑥))) → (𝑓‘𝑥) ∈ ∪ 𝑆)
29	18	adantr 486	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ (𝑥 ∈ ∪ 𝑅 ∧ (𝑓‘𝑥) ≠ (𝑔‘𝑥))) → 𝑔:∪ 𝑅⟶∪ 𝑆)
30	29, 27	ffvelcdmd 7106	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ (𝑥 ∈ ∪ 𝑅 ∧ (𝑓‘𝑥) ≠ (𝑔‘𝑥))) → (𝑔‘𝑥) ∈ ∪ 𝑆)
31		simprr 785	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ (𝑥 ∈ ∪ 𝑅 ∧ (𝑓‘𝑥) ≠ (𝑔‘𝑥))) → (𝑓‘𝑥) ≠ (𝑔‘𝑥))
32	12	hausnei 23673	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ Haus ∧ ((𝑓‘𝑥) ∈ ∪ 𝑆 ∧ (𝑔‘𝑥) ∈ ∪ 𝑆 ∧ (𝑓‘𝑥) ≠ (𝑔‘𝑥))) → ∃𝑎 ∈ 𝑆 ∃𝑏 ∈ 𝑆 ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))
33	25, 28, 30, 31, 32	syl13anc 1400	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ (𝑥 ∈ ∪ 𝑅 ∧ (𝑓‘𝑥) ≠ (𝑔‘𝑥))) → ∃𝑎 ∈ 𝑆 ∃𝑏 ∈ 𝑆 ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))
34	33	expr 462	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) → ((𝑓‘𝑥) ≠ (𝑔‘𝑥) → ∃𝑎 ∈ 𝑆 ∃𝑏 ∈ 𝑆 ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅)))
35	24, 34	biimtrrid 246	. . . . . . . . 9 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) → (¬ (𝑓‘𝑥) = (𝑔‘𝑥) → ∃𝑎 ∈ 𝑆 ∃𝑏 ∈ 𝑆 ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅)))
36		simp-4l 795	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → 𝑅 ∈ Top)
37	1	ad4antlr 746	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → 𝑆 ∈ Top)
38		simplr 781	. . . . . . . . . . . . . 14 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → 𝑥 ∈ ∪ 𝑅)
39	38	snssd 4747	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → {𝑥} ⊆ ∪ 𝑅)
40		toptopon2 23263	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 ∈ Top ↔ 𝑅 ∈ (TopOn‘∪ 𝑅))
41	36, 40	sylib 221	. . . . . . . . . . . . . . 15 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → 𝑅 ∈ (TopOn‘∪ 𝑅))
42		restsn2 23516	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ (TopOn‘∪ 𝑅) ∧ 𝑥 ∈ ∪ 𝑅) → (𝑅 ↾t {𝑥}) = 𝒫 {𝑥})
43	41, 38, 42	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → (𝑅 ↾t {𝑥}) = 𝒫 {𝑥})
44		snfi 9096	. . . . . . . . . . . . . . 15 ⊢ {𝑥} ∈ Fin
45		discmp 23743	. . . . . . . . . . . . . . 15 ⊢ ({𝑥} ∈ Fin ↔ 𝒫 {𝑥} ∈ Comp)
46	44, 45	mpbi 233	. . . . . . . . . . . . . 14 ⊢ 𝒫 {𝑥} ∈ Comp
47	43, 46	eqeltrdi 2872	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → (𝑅 ↾t {𝑥}) ∈ Comp)
48		simprll 791	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → 𝑎 ∈ 𝑆)
49	11, 36, 37, 39, 47, 48	xkoopn 23935	. . . . . . . . . . . 12 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎} ∈ (𝑆 ↑ko 𝑅))
50		simprlr 792	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → 𝑏 ∈ 𝑆)
51	11, 36, 37, 39, 47, 50	xkoopn 23935	. . . . . . . . . . . 12 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑏} ∈ (𝑆 ↑ko 𝑅))
52		imaeq1 6058	. . . . . . . . . . . . . 14 ⊢ (ℎ = 𝑓 → (ℎ “ {𝑥}) = (𝑓 “ {𝑥}))
53	52	sseq1d 3944	. . . . . . . . . . . . 13 ⊢ (ℎ = 𝑓 → ((ℎ “ {𝑥}) ⊆ 𝑎 ↔ (𝑓 “ {𝑥}) ⊆ 𝑎))
54	10	ad2antrr 739	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → 𝑓 ∈ (𝑅 Cn 𝑆))
55	15	ad2antrr 739	. . . . . . . . . . . . . . 15 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → 𝑓 Fn ∪ 𝑅)
56		fnsnfv 6984	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 Fn ∪ 𝑅 ∧ 𝑥 ∈ ∪ 𝑅) → {(𝑓‘𝑥)} = (𝑓 “ {𝑥}))
57	55, 38, 56	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → {(𝑓‘𝑥)} = (𝑓 “ {𝑥}))
58		simprr1 1240	. . . . . . . . . . . . . . 15 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → (𝑓‘𝑥) ∈ 𝑎)
59	58	snssd 4747	. . . . . . . . . . . . . 14 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → {(𝑓‘𝑥)} ⊆ 𝑎)
60	57, 59	eqsstrrd 3948	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → (𝑓 “ {𝑥}) ⊆ 𝑎)
61	53, 54, 60	elrabd 3650	. . . . . . . . . . . 12 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → 𝑓 ∈ {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎})
62		imaeq1 6058	. . . . . . . . . . . . . 14 ⊢ (ℎ = 𝑔 → (ℎ “ {𝑥}) = (𝑔 “ {𝑥}))
63	62	sseq1d 3944	. . . . . . . . . . . . 13 ⊢ (ℎ = 𝑔 → ((ℎ “ {𝑥}) ⊆ 𝑏 ↔ (𝑔 “ {𝑥}) ⊆ 𝑏))
64	16	ad2antrr 739	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → 𝑔 ∈ (𝑅 Cn 𝑆))
65	19	ad2antrr 739	. . . . . . . . . . . . . . 15 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → 𝑔 Fn ∪ 𝑅)
66		fnsnfv 6984	. . . . . . . . . . . . . . 15 ⊢ ((𝑔 Fn ∪ 𝑅 ∧ 𝑥 ∈ ∪ 𝑅) → {(𝑔‘𝑥)} = (𝑔 “ {𝑥}))
67	65, 38, 66	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → {(𝑔‘𝑥)} = (𝑔 “ {𝑥}))
68		simprr2 1241	. . . . . . . . . . . . . . 15 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → (𝑔‘𝑥) ∈ 𝑏)
69	68	snssd 4747	. . . . . . . . . . . . . 14 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → {(𝑔‘𝑥)} ⊆ 𝑏)
70	67, 69	eqsstrrd 3948	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → (𝑔 “ {𝑥}) ⊆ 𝑏)
71	63, 64, 70	elrabd 3650	. . . . . . . . . . . 12 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → 𝑔 ∈ {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑏})
72		inrab 4264	. . . . . . . . . . . . 13 ⊢ ({ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎} ∩ {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑏}) = {ℎ ∈ (𝑅 Cn 𝑆) ∣ ((ℎ “ {𝑥}) ⊆ 𝑎 ∧ (ℎ “ {𝑥}) ⊆ 𝑏)}
73		simpllr 788	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) ∧ ℎ ∈ (𝑅 Cn 𝑆)) → 𝑥 ∈ ∪ 𝑅)
74	11, 12	cnf 23591	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ℎ ∈ (𝑅 Cn 𝑆) → ℎ:∪ 𝑅⟶∪ 𝑆)
75	74	fdmd 6739	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℎ ∈ (𝑅 Cn 𝑆) → dom ℎ = ∪ 𝑅)
76	75	adantl 487	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) ∧ ℎ ∈ (𝑅 Cn 𝑆)) → dom ℎ = ∪ 𝑅)
77	73, 76	eleqtrrd 2867	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) ∧ ℎ ∈ (𝑅 Cn 𝑆)) → 𝑥 ∈ dom ℎ)
78		simprr3 1242	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → (𝑎 ∩ 𝑏) = ∅)
79	78	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) ∧ ℎ ∈ (𝑅 Cn 𝑆)) → (𝑎 ∩ 𝑏) = ∅)
80		sseq0 4357	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℎ “ {𝑥}) ⊆ (𝑎 ∩ 𝑏) ∧ (𝑎 ∩ 𝑏) = ∅) → (ℎ “ {𝑥}) = ∅)
81	80	expcom 419	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ∩ 𝑏) = ∅ → ((ℎ “ {𝑥}) ⊆ (𝑎 ∩ 𝑏) → (ℎ “ {𝑥}) = ∅))
82	79, 81	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) ∧ ℎ ∈ (𝑅 Cn 𝑆)) → ((ℎ “ {𝑥}) ⊆ (𝑎 ∩ 𝑏) → (ℎ “ {𝑥}) = ∅))
83		imadisj 6088	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℎ “ {𝑥}) = ∅ ↔ (dom ℎ ∩ {𝑥}) = ∅)
84		disjsn 4672	. . . . . . . . . . . . . . . . . . 19 ⊢ ((dom ℎ ∩ {𝑥}) = ∅ ↔ ¬ 𝑥 ∈ dom ℎ)
85	83, 84	bitri 278	. . . . . . . . . . . . . . . . . 18 ⊢ ((ℎ “ {𝑥}) = ∅ ↔ ¬ 𝑥 ∈ dom ℎ)
86	82, 85	imbitrdi 254	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) ∧ ℎ ∈ (𝑅 Cn 𝑆)) → ((ℎ “ {𝑥}) ⊆ (𝑎 ∩ 𝑏) → ¬ 𝑥 ∈ dom ℎ))
87	77, 86	mt2d 137	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) ∧ ℎ ∈ (𝑅 Cn 𝑆)) → ¬ (ℎ “ {𝑥}) ⊆ (𝑎 ∩ 𝑏))
88		ssin 4138	. . . . . . . . . . . . . . . 16 ⊢ (((ℎ “ {𝑥}) ⊆ 𝑎 ∧ (ℎ “ {𝑥}) ⊆ 𝑏) ↔ (ℎ “ {𝑥}) ⊆ (𝑎 ∩ 𝑏))
89	87, 88	sylnibr 332	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) ∧ ℎ ∈ (𝑅 Cn 𝑆)) → ¬ ((ℎ “ {𝑥}) ⊆ 𝑎 ∧ (ℎ “ {𝑥}) ⊆ 𝑏))
90	89	ralrimiva 3158	. . . . . . . . . . . . . 14 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → ∀ℎ ∈ (𝑅 Cn 𝑆) ¬ ((ℎ “ {𝑥}) ⊆ 𝑎 ∧ (ℎ “ {𝑥}) ⊆ 𝑏))
91		rabeq0 4341	. . . . . . . . . . . . . 14 ⊢ ({ℎ ∈ (𝑅 Cn 𝑆) ∣ ((ℎ “ {𝑥}) ⊆ 𝑎 ∧ (ℎ “ {𝑥}) ⊆ 𝑏)} = ∅ ↔ ∀ℎ ∈ (𝑅 Cn 𝑆) ¬ ((ℎ “ {𝑥}) ⊆ 𝑎 ∧ (ℎ “ {𝑥}) ⊆ 𝑏))
92	90, 91	sylibr 237	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → {ℎ ∈ (𝑅 Cn 𝑆) ∣ ((ℎ “ {𝑥}) ⊆ 𝑎 ∧ (ℎ “ {𝑥}) ⊆ 𝑏)} = ∅)
93	72, 92	eqtrid 2810	. . . . . . . . . . . 12 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → ({ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎} ∩ {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑏}) = ∅)
94		eleq2 2853	. . . . . . . . . . . . . 14 ⊢ (𝑢 = {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎} → (𝑓 ∈ 𝑢 ↔ 𝑓 ∈ {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎}))
95		ineq1 4113	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎} → (𝑢 ∩ 𝑣) = ({ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎} ∩ 𝑣))
96	95	eqeq1d 2765	. . . . . . . . . . . . . 14 ⊢ (𝑢 = {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎} → ((𝑢 ∩ 𝑣) = ∅ ↔ ({ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎} ∩ 𝑣) = ∅))
97	94, 96	3anbi13d 1467	. . . . . . . . . . . . 13 ⊢ (𝑢 = {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎} → ((𝑓 ∈ 𝑢 ∧ 𝑔 ∈ 𝑣 ∧ (𝑢 ∩ 𝑣) = ∅) ↔ (𝑓 ∈ {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎} ∧ 𝑔 ∈ 𝑣 ∧ ({ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎} ∩ 𝑣) = ∅)))
98		eleq2 2853	. . . . . . . . . . . . . 14 ⊢ (𝑣 = {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑏} → (𝑔 ∈ 𝑣 ↔ 𝑔 ∈ {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑏}))
99		ineq2 4114	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑏} → ({ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎} ∩ 𝑣) = ({ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎} ∩ {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑏}))
100	99	eqeq1d 2765	. . . . . . . . . . . . . 14 ⊢ (𝑣 = {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑏} → (({ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎} ∩ 𝑣) = ∅ ↔ ({ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎} ∩ {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑏}) = ∅))
101	98, 100	3anbi23d 1468	. . . . . . . . . . . . 13 ⊢ (𝑣 = {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑏} → ((𝑓 ∈ {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎} ∧ 𝑔 ∈ 𝑣 ∧ ({ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎} ∩ 𝑣) = ∅) ↔ (𝑓 ∈ {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎} ∧ 𝑔 ∈ {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑏} ∧ ({ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎} ∩ {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑏}) = ∅)))
102	97, 101	rspc2ev 3592	. . . . . . . . . . . 12 ⊢ (({ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎} ∈ (𝑆 ↑ko 𝑅) ∧ {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑏} ∈ (𝑆 ↑ko 𝑅) ∧ (𝑓 ∈ {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎} ∧ 𝑔 ∈ {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑏} ∧ ({ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑎} ∩ {ℎ ∈ (𝑅 Cn 𝑆) ∣ (ℎ “ {𝑥}) ⊆ 𝑏}) = ∅)) → ∃𝑢 ∈ (𝑆 ↑ko 𝑅)∃𝑣 ∈ (𝑆 ↑ko 𝑅)(𝑓 ∈ 𝑢 ∧ 𝑔 ∈ 𝑣 ∧ (𝑢 ∩ 𝑣) = ∅))
103	49, 51, 61, 71, 93, 102	syl113anc 1410	. . . . . . . . . . 11 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅))) → ∃𝑢 ∈ (𝑆 ↑ko 𝑅)∃𝑣 ∈ (𝑆 ↑ko 𝑅)(𝑓 ∈ 𝑢 ∧ 𝑔 ∈ 𝑣 ∧ (𝑢 ∩ 𝑣) = ∅))
104	103	expr 462	. . . . . . . . . 10 ⊢ (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) ∧ (𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆)) → (((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅) → ∃𝑢 ∈ (𝑆 ↑ko 𝑅)∃𝑣 ∈ (𝑆 ↑ko 𝑅)(𝑓 ∈ 𝑢 ∧ 𝑔 ∈ 𝑣 ∧ (𝑢 ∩ 𝑣) = ∅)))
105	104	rexlimdvva 3223	. . . . . . . . 9 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) → (∃𝑎 ∈ 𝑆 ∃𝑏 ∈ 𝑆 ((𝑓‘𝑥) ∈ 𝑎 ∧ (𝑔‘𝑥) ∈ 𝑏 ∧ (𝑎 ∩ 𝑏) = ∅) → ∃𝑢 ∈ (𝑆 ↑ko 𝑅)∃𝑣 ∈ (𝑆 ↑ko 𝑅)(𝑓 ∈ 𝑢 ∧ 𝑔 ∈ 𝑣 ∧ (𝑢 ∩ 𝑣) = ∅)))
106	35, 105	syld 48	. . . . . . . 8 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ 𝑥 ∈ ∪ 𝑅) → (¬ (𝑓‘𝑥) = (𝑔‘𝑥) → ∃𝑢 ∈ (𝑆 ↑ko 𝑅)∃𝑣 ∈ (𝑆 ↑ko 𝑅)(𝑓 ∈ 𝑢 ∧ 𝑔 ∈ 𝑣 ∧ (𝑢 ∩ 𝑣) = ∅)))
107	106	rexlimdva 3167	. . . . . . 7 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) → (∃𝑥 ∈ ∪ 𝑅 ¬ (𝑓‘𝑥) = (𝑔‘𝑥) → ∃𝑢 ∈ (𝑆 ↑ko 𝑅)∃𝑣 ∈ (𝑆 ↑ko 𝑅)(𝑓 ∈ 𝑢 ∧ 𝑔 ∈ 𝑣 ∧ (𝑢 ∩ 𝑣) = ∅)))
108	23, 107	biimtrrid 246	. . . . . 6 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) → (¬ ∀𝑥 ∈ ∪ 𝑅(𝑓‘𝑥) = (𝑔‘𝑥) → ∃𝑢 ∈ (𝑆 ↑ko 𝑅)∃𝑣 ∈ (𝑆 ↑ko 𝑅)(𝑓 ∈ 𝑢 ∧ 𝑔 ∈ 𝑣 ∧ (𝑢 ∩ 𝑣) = ∅)))
109	22, 108	sylbid 243	. . . . 5 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) → (𝑓 ≠ 𝑔 → ∃𝑢 ∈ (𝑆 ↑ko 𝑅)∃𝑣 ∈ (𝑆 ↑ko 𝑅)(𝑓 ∈ 𝑢 ∧ 𝑔 ∈ 𝑣 ∧ (𝑢 ∩ 𝑣) = ∅)))
110	109	ex 418	. . . 4 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) → ((𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆)) → (𝑓 ≠ 𝑔 → ∃𝑢 ∈ (𝑆 ↑ko 𝑅)∃𝑣 ∈ (𝑆 ↑ko 𝑅)(𝑓 ∈ 𝑢 ∧ 𝑔 ∈ 𝑣 ∧ (𝑢 ∩ 𝑣) = ∅))))
111	9, 110	sylbird 263	. . 3 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) → ((𝑓 ∈ ∪ (𝑆 ↑ko 𝑅) ∧ 𝑔 ∈ ∪ (𝑆 ↑ko 𝑅)) → (𝑓 ≠ 𝑔 → ∃𝑢 ∈ (𝑆 ↑ko 𝑅)∃𝑣 ∈ (𝑆 ↑ko 𝑅)(𝑓 ∈ 𝑢 ∧ 𝑔 ∈ 𝑣 ∧ (𝑢 ∩ 𝑣) = ∅))))
112	111	ralrimivv 3207	. 2 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) → ∀𝑓 ∈ ∪ (𝑆 ↑ko 𝑅)∀𝑔 ∈ ∪ (𝑆 ↑ko 𝑅)(𝑓 ≠ 𝑔 → ∃𝑢 ∈ (𝑆 ↑ko 𝑅)∃𝑣 ∈ (𝑆 ↑ko 𝑅)(𝑓 ∈ 𝑢 ∧ 𝑔 ∈ 𝑣 ∧ (𝑢 ∩ 𝑣) = ∅)))
113		eqid 2763	. . 3 ⊢ ∪ (𝑆 ↑ko 𝑅) = ∪ (𝑆 ↑ko 𝑅)
114	113	ishaus 23667	. 2 ⊢ ((𝑆 ↑ko 𝑅) ∈ Haus ↔ ((𝑆 ↑ko 𝑅) ∈ Top ∧ ∀𝑓 ∈ ∪ (𝑆 ↑ko 𝑅)∀𝑔 ∈ ∪ (𝑆 ↑ko 𝑅)(𝑓 ≠ 𝑔 → ∃𝑢 ∈ (𝑆 ↑ko 𝑅)∃𝑣 ∈ (𝑆 ↑ko 𝑅)(𝑓 ∈ 𝑢 ∧ 𝑔 ∈ 𝑣 ∧ (𝑢 ∩ 𝑣) = ∅))))
115	3, 112, 114	sylanbrc 595	1 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) → (𝑆 ↑ko 𝑅) ∈ Haus)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2147   ≠ wne 2959  ∀wral 3080  ∃wrex 3090  {crab 3416   ⊆ wss 3900   ∩ cin 4092  ∅c0 4281  𝒫 cpw 4560  {csn 4588  ∪ cuni 4870  dom cdm 5655   “ cima 5658   Fn wfn 6550  ⟶wf 6551  ‘cfv 6555  (class class class)co 7440  Fincfn 8998   ↾_t crest 17617  Topctop 23238  TopOnctopon 23255   Cn ccn 23569  Hauscha 23653  Compccmp 23731   ↑_ko cxko 23907

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-rep 5235  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7772

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-int 4911  df-iun 4956  df-br 5107  df-opab 5171  df-mpt 5190  df-tr 5216  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-ord 6380  df-on 6381  df-lim 6382  df-suc 6383  df-iota 6509  df-fun 6557  df-fn 6558  df-f 6559  df-f1 6560  df-fo 6561  df-f1o 6562  df-fv 6563  df-ov 7443  df-oprab 7444  df-mpo 7445  df-om 7899  df-1st 8022  df-2nd 8023  df-1o 8501  df-2o 8502  df-map 8874  df-en 8999  df-dom 9000  df-fin 9002  df-fi 9427  df-rest 17619  df-topgen 17640  df-top 23239  df-topon 23256  df-bases 23291  df-cn 23572  df-haus 23660  df-cmp 23732  df-xko 23909

This theorem is used by: (None)