MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xkohaus Structured version   Visualization version   GIF version
Theorem xkohaus 23148
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.
StepHypRef Expression
1 haustop 22826 . . 3 (𝑆 ∈ Haus β†’ 𝑆 ∈ Top)
2 xkotop 23083 . . 3 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (𝑆 ↑ko 𝑅) ∈ Top)
31, 2sylan2 593 . 2 ((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) β†’ (𝑆 ↑ko 𝑅) ∈ Top)
4 eqid 2732 . . . . . . . 8 (𝑆 ↑ko 𝑅) = (𝑆 ↑ko 𝑅)
54xkouni 23094 . . . . . . 7 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (𝑅 Cn 𝑆) = βˆͺ (𝑆 ↑ko 𝑅))
61, 5sylan2 593 . . . . . 6 ((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) β†’ (𝑅 Cn 𝑆) = βˆͺ (𝑆 ↑ko 𝑅))
76eleq2d 2819 . . . . 5 ((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) β†’ (𝑓 ∈ (𝑅 Cn 𝑆) ↔ 𝑓 ∈ βˆͺ (𝑆 ↑ko 𝑅)))
86eleq2d 2819 . . . . 5 ((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) β†’ (𝑔 ∈ (𝑅 Cn 𝑆) ↔ 𝑔 ∈ βˆͺ (𝑆 ↑ko 𝑅)))
97, 8anbi12d 631 . . . 4 ((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) β†’ ((𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆)) ↔ (𝑓 ∈ βˆͺ (𝑆 ↑ko 𝑅) ∧ 𝑔 ∈ βˆͺ (𝑆 ↑ko 𝑅))))
10 simprl 769 . . . . . . . . . 10 (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) β†’ 𝑓 ∈ (𝑅 Cn 𝑆))
11 eqid 2732 . . . . . . . . . . 11 βˆͺ 𝑅 = βˆͺ 𝑅
12 eqid 2732 . . . . . . . . . . 11 βˆͺ 𝑆 = βˆͺ 𝑆
1311, 12cnf 22741 . . . . . . . . . 10 (𝑓 ∈ (𝑅 Cn 𝑆) β†’ 𝑓:βˆͺ π‘…βŸΆβˆͺ 𝑆)
1410, 13syl 17 . . . . . . . . 9 (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) β†’ 𝑓:βˆͺ π‘…βŸΆβˆͺ 𝑆)
1514ffnd 6715 . . . . . . . 8 (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) β†’ 𝑓 Fn βˆͺ 𝑅)
16 simprr 771 . . . . . . . . . 10 (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) β†’ 𝑔 ∈ (𝑅 Cn 𝑆))
1711, 12cnf 22741 . . . . . . . . . 10 (𝑔 ∈ (𝑅 Cn 𝑆) β†’ 𝑔:βˆͺ π‘…βŸΆβˆͺ 𝑆)
1816, 17syl 17 . . . . . . . . 9 (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) β†’ 𝑔:βˆͺ π‘…βŸΆβˆͺ 𝑆)
1918ffnd 6715 . . . . . . . 8 (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) β†’ 𝑔 Fn βˆͺ 𝑅)
20 eqfnfv 7029 . . . . . . . 8 ((𝑓 Fn βˆͺ 𝑅 ∧ 𝑔 Fn βˆͺ 𝑅) β†’ (𝑓 = 𝑔 ↔ βˆ€π‘₯ ∈ βˆͺ 𝑅(π‘“β€˜π‘₯) = (π‘”β€˜π‘₯)))
2115, 19, 20syl2anc 584 . . . . . . 7 (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) β†’ (𝑓 = 𝑔 ↔ βˆ€π‘₯ ∈ βˆͺ 𝑅(π‘“β€˜π‘₯) = (π‘”β€˜π‘₯)))
2221necon3abid 2977 . . . . . 6 (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) β†’ (𝑓 β‰  𝑔 ↔ Β¬ βˆ€π‘₯ ∈ βˆͺ 𝑅(π‘“β€˜π‘₯) = (π‘”β€˜π‘₯)))
23 rexnal 3100 . . . . . . 7 (βˆƒπ‘₯ ∈ βˆͺ 𝑅 Β¬ (π‘“β€˜π‘₯) = (π‘”β€˜π‘₯) ↔ Β¬ βˆ€π‘₯ ∈ βˆͺ 𝑅(π‘“β€˜π‘₯) = (π‘”β€˜π‘₯))
24 df-ne 2941 . . . . . . . . . 10 ((π‘“β€˜π‘₯) β‰  (π‘”β€˜π‘₯) ↔ Β¬ (π‘“β€˜π‘₯) = (π‘”β€˜π‘₯))
25 simpllr 774 . . . . . . . . . . . 12 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ (π‘₯ ∈ βˆͺ 𝑅 ∧ (π‘“β€˜π‘₯) β‰  (π‘”β€˜π‘₯))) β†’ 𝑆 ∈ Haus)
2614adantr 481 . . . . . . . . . . . . 13 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ (π‘₯ ∈ βˆͺ 𝑅 ∧ (π‘“β€˜π‘₯) β‰  (π‘”β€˜π‘₯))) β†’ 𝑓:βˆͺ π‘…βŸΆβˆͺ 𝑆)
27 simprl 769 . . . . . . . . . . . . 13 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ (π‘₯ ∈ βˆͺ 𝑅 ∧ (π‘“β€˜π‘₯) β‰  (π‘”β€˜π‘₯))) β†’ π‘₯ ∈ βˆͺ 𝑅)
2826, 27ffvelcdmd 7084 . . . . . . . . . . . 12 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ (π‘₯ ∈ βˆͺ 𝑅 ∧ (π‘“β€˜π‘₯) β‰  (π‘”β€˜π‘₯))) β†’ (π‘“β€˜π‘₯) ∈ βˆͺ 𝑆)
2918adantr 481 . . . . . . . . . . . . 13 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ (π‘₯ ∈ βˆͺ 𝑅 ∧ (π‘“β€˜π‘₯) β‰  (π‘”β€˜π‘₯))) β†’ 𝑔:βˆͺ π‘…βŸΆβˆͺ 𝑆)
3029, 27ffvelcdmd 7084 . . . . . . . . . . . 12 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ (π‘₯ ∈ βˆͺ 𝑅 ∧ (π‘“β€˜π‘₯) β‰  (π‘”β€˜π‘₯))) β†’ (π‘”β€˜π‘₯) ∈ βˆͺ 𝑆)
31 simprr 771 . . . . . . . . . . . 12 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ (π‘₯ ∈ βˆͺ 𝑅 ∧ (π‘“β€˜π‘₯) β‰  (π‘”β€˜π‘₯))) β†’ (π‘“β€˜π‘₯) β‰  (π‘”β€˜π‘₯))
3212hausnei 22823 . . . . . . . . . . . 12 ((𝑆 ∈ Haus ∧ ((π‘“β€˜π‘₯) ∈ βˆͺ 𝑆 ∧ (π‘”β€˜π‘₯) ∈ βˆͺ 𝑆 ∧ (π‘“β€˜π‘₯) β‰  (π‘”β€˜π‘₯))) β†’ βˆƒπ‘Ž ∈ 𝑆 βˆƒπ‘ ∈ 𝑆 ((π‘“β€˜π‘₯) ∈ π‘Ž ∧ (π‘”β€˜π‘₯) ∈ 𝑏 ∧ (π‘Ž ∩ 𝑏) = βˆ…))
3325, 28, 30, 31, 32syl13anc 1372 . . . . . . . . . . 11 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ (π‘₯ ∈ βˆͺ 𝑅 ∧ (π‘“β€˜π‘₯) β‰  (π‘”β€˜π‘₯))) β†’ βˆƒπ‘Ž ∈ 𝑆 βˆƒπ‘ ∈ 𝑆 ((π‘“β€˜π‘₯) ∈ π‘Ž ∧ (π‘”β€˜π‘₯) ∈ 𝑏 ∧ (π‘Ž ∩ 𝑏) = βˆ…))
3433expr 457 . . . . . . . . . 10 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ π‘₯ ∈ βˆͺ 𝑅) β†’ ((π‘“β€˜π‘₯) β‰  (π‘”β€˜π‘₯) β†’ βˆƒπ‘Ž ∈ 𝑆 βˆƒπ‘ ∈ 𝑆 ((π‘“β€˜π‘₯) ∈ π‘Ž ∧ (π‘”β€˜π‘₯) ∈ 𝑏 ∧ (π‘Ž ∩ 𝑏) = βˆ…)))
3524, 34biimtrrid 242 . . . . . . . . 9 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ π‘₯ ∈ βˆͺ 𝑅) β†’ (Β¬ (π‘“β€˜π‘₯) = (π‘”β€˜π‘₯) β†’ βˆƒπ‘Ž ∈ 𝑆 βˆƒπ‘ ∈ 𝑆 ((π‘“β€˜π‘₯) ∈ π‘Ž ∧ (π‘”β€˜π‘₯) ∈ 𝑏 ∧ (π‘Ž ∩ 𝑏) = βˆ…)))
36 simp-4l 781 . . . . . . . . . . . . 13 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ π‘₯ ∈ βˆͺ 𝑅) ∧ ((π‘Ž ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((π‘“β€˜π‘₯) ∈ π‘Ž ∧ (π‘”β€˜π‘₯) ∈ 𝑏 ∧ (π‘Ž ∩ 𝑏) = βˆ…))) β†’ 𝑅 ∈ Top)
371ad4antlr 731 . . . . . . . . . . . . 13 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ π‘₯ ∈ βˆͺ 𝑅) ∧ ((π‘Ž ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((π‘“β€˜π‘₯) ∈ π‘Ž ∧ (π‘”β€˜π‘₯) ∈ 𝑏 ∧ (π‘Ž ∩ 𝑏) = βˆ…))) β†’ 𝑆 ∈ Top)
38 simplr 767 . . . . . . . . . . . . . 14 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ π‘₯ ∈ βˆͺ 𝑅) ∧ ((π‘Ž ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((π‘“β€˜π‘₯) ∈ π‘Ž ∧ (π‘”β€˜π‘₯) ∈ 𝑏 ∧ (π‘Ž ∩ 𝑏) = βˆ…))) β†’ π‘₯ ∈ βˆͺ 𝑅)
3938snssd 4811 . . . . . . . . . . . . 13 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ π‘₯ ∈ βˆͺ 𝑅) ∧ ((π‘Ž ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((π‘“β€˜π‘₯) ∈ π‘Ž ∧ (π‘”β€˜π‘₯) ∈ 𝑏 ∧ (π‘Ž ∩ 𝑏) = βˆ…))) β†’ {π‘₯} βŠ† βˆͺ 𝑅)
40 toptopon2 22411 . . . . . . . . . . . . . . . 16 (𝑅 ∈ Top ↔ 𝑅 ∈ (TopOnβ€˜βˆͺ 𝑅))
4136, 40sylib 217 . . . . . . . . . . . . . . 15 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ π‘₯ ∈ βˆͺ 𝑅) ∧ ((π‘Ž ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((π‘“β€˜π‘₯) ∈ π‘Ž ∧ (π‘”β€˜π‘₯) ∈ 𝑏 ∧ (π‘Ž ∩ 𝑏) = βˆ…))) β†’ 𝑅 ∈ (TopOnβ€˜βˆͺ 𝑅))
42 restsn2 22666 . . . . . . . . . . . . . . 15 ((𝑅 ∈ (TopOnβ€˜βˆͺ 𝑅) ∧ π‘₯ ∈ βˆͺ 𝑅) β†’ (𝑅 β†Ύt {π‘₯}) = 𝒫 {π‘₯})
4341, 38, 42syl2anc 584 . . . . . . . . . . . . . 14 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ π‘₯ ∈ βˆͺ 𝑅) ∧ ((π‘Ž ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((π‘“β€˜π‘₯) ∈ π‘Ž ∧ (π‘”β€˜π‘₯) ∈ 𝑏 ∧ (π‘Ž ∩ 𝑏) = βˆ…))) β†’ (𝑅 β†Ύt {π‘₯}) = 𝒫 {π‘₯})
44 snfi 9040 . . . . . . . . . . . . . . 15 {π‘₯} ∈ Fin
45 discmp 22893 . . . . . . . . . . . . . . 15 ({π‘₯} ∈ Fin ↔ 𝒫 {π‘₯} ∈ Comp)
4644, 45mpbi 229 . . . . . . . . . . . . . 14 𝒫 {π‘₯} ∈ Comp
4743, 46eqeltrdi 2841 . . . . . . . . . . . . 13 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ π‘₯ ∈ βˆͺ 𝑅) ∧ ((π‘Ž ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((π‘“β€˜π‘₯) ∈ π‘Ž ∧ (π‘”β€˜π‘₯) ∈ 𝑏 ∧ (π‘Ž ∩ 𝑏) = βˆ…))) β†’ (𝑅 β†Ύt {π‘₯}) ∈ Comp)
48 simprll 777 . . . . . . . . . . . . 13 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ π‘₯ ∈ βˆͺ 𝑅) ∧ ((π‘Ž ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((π‘“β€˜π‘₯) ∈ π‘Ž ∧ (π‘”β€˜π‘₯) ∈ 𝑏 ∧ (π‘Ž ∩ 𝑏) = βˆ…))) β†’ π‘Ž ∈ 𝑆)
4911, 36, 37, 39, 47, 48xkoopn 23084 . . . . . . . . . . . 12 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ π‘₯ ∈ βˆͺ 𝑅) ∧ ((π‘Ž ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((π‘“β€˜π‘₯) ∈ π‘Ž ∧ (π‘”β€˜π‘₯) ∈ 𝑏 ∧ (π‘Ž ∩ 𝑏) = βˆ…))) β†’ {β„Ž ∈ (𝑅 Cn 𝑆) ∣ (β„Ž β€œ {π‘₯}) βŠ† π‘Ž} ∈ (𝑆 ↑ko 𝑅))
50 simprlr 778 . . . . . . . . . . . . 13 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ π‘₯ ∈ βˆͺ 𝑅) ∧ ((π‘Ž ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((π‘“β€˜π‘₯) ∈ π‘Ž ∧ (π‘”β€˜π‘₯) ∈ 𝑏 ∧ (π‘Ž ∩ 𝑏) = βˆ…))) β†’ 𝑏 ∈ 𝑆)
5111, 36, 37, 39, 47, 50xkoopn 23084 . . . . . . . . . . . 12 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ π‘₯ ∈ βˆͺ 𝑅) ∧ ((π‘Ž ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((π‘“β€˜π‘₯) ∈ π‘Ž ∧ (π‘”β€˜π‘₯) ∈ 𝑏 ∧ (π‘Ž ∩ 𝑏) = βˆ…))) β†’ {β„Ž ∈ (𝑅 Cn 𝑆) ∣ (β„Ž β€œ {π‘₯}) βŠ† 𝑏} ∈ (𝑆 ↑ko 𝑅))
52 imaeq1 6052 . . . . . . . . . . . . . 14 (β„Ž = 𝑓 β†’ (β„Ž β€œ {π‘₯}) = (𝑓 β€œ {π‘₯}))
5352sseq1d 4012 . . . . . . . . . . . . 13 (β„Ž = 𝑓 β†’ ((β„Ž β€œ {π‘₯}) βŠ† π‘Ž ↔ (𝑓 β€œ {π‘₯}) βŠ† π‘Ž))
5410ad2antrr 724 . . . . . . . . . . . . 13 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ π‘₯ ∈ βˆͺ 𝑅) ∧ ((π‘Ž ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((π‘“β€˜π‘₯) ∈ π‘Ž ∧ (π‘”β€˜π‘₯) ∈ 𝑏 ∧ (π‘Ž ∩ 𝑏) = βˆ…))) β†’ 𝑓 ∈ (𝑅 Cn 𝑆))
5515ad2antrr 724 . . . . . . . . . . . . . . 15 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ π‘₯ ∈ βˆͺ 𝑅) ∧ ((π‘Ž ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((π‘“β€˜π‘₯) ∈ π‘Ž ∧ (π‘”β€˜π‘₯) ∈ 𝑏 ∧ (π‘Ž ∩ 𝑏) = βˆ…))) β†’ 𝑓 Fn βˆͺ 𝑅)
56 fnsnfv 6967 . . . . . . . . . . . . . . 15 ((𝑓 Fn βˆͺ 𝑅 ∧ π‘₯ ∈ βˆͺ 𝑅) β†’ {(π‘“β€˜π‘₯)} = (𝑓 β€œ {π‘₯}))
5755, 38, 56syl2anc 584 . . . . . . . . . . . . . 14 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ π‘₯ ∈ βˆͺ 𝑅) ∧ ((π‘Ž ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((π‘“β€˜π‘₯) ∈ π‘Ž ∧ (π‘”β€˜π‘₯) ∈ 𝑏 ∧ (π‘Ž ∩ 𝑏) = βˆ…))) β†’ {(π‘“β€˜π‘₯)} = (𝑓 β€œ {π‘₯}))
58 simprr1 1221 . . . . . . . . . . . . . . 15 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ π‘₯ ∈ βˆͺ 𝑅) ∧ ((π‘Ž ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((π‘“β€˜π‘₯) ∈ π‘Ž ∧ (π‘”β€˜π‘₯) ∈ 𝑏 ∧ (π‘Ž ∩ 𝑏) = βˆ…))) β†’ (π‘“β€˜π‘₯) ∈ π‘Ž)
5958snssd 4811 . . . . . . . . . . . . . 14 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ π‘₯ ∈ βˆͺ 𝑅) ∧ ((π‘Ž ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((π‘“β€˜π‘₯) ∈ π‘Ž ∧ (π‘”β€˜π‘₯) ∈ 𝑏 ∧ (π‘Ž ∩ 𝑏) = βˆ…))) β†’ {(π‘“β€˜π‘₯)} βŠ† π‘Ž)
6057, 59eqsstrrd 4020 . . . . . . . . . . . . 13 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ π‘₯ ∈ βˆͺ 𝑅) ∧ ((π‘Ž ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((π‘“β€˜π‘₯) ∈ π‘Ž ∧ (π‘”β€˜π‘₯) ∈ 𝑏 ∧ (π‘Ž ∩ 𝑏) = βˆ…))) β†’ (𝑓 β€œ {π‘₯}) βŠ† π‘Ž)
6153, 54, 60elrabd 3684 . . . . . . . . . . . 12 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ π‘₯ ∈ βˆͺ 𝑅) ∧ ((π‘Ž ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((π‘“β€˜π‘₯) ∈ π‘Ž ∧ (π‘”β€˜π‘₯) ∈ 𝑏 ∧ (π‘Ž ∩ 𝑏) = βˆ…))) β†’ 𝑓 ∈ {β„Ž ∈ (𝑅 Cn 𝑆) ∣ (β„Ž β€œ {π‘₯}) βŠ† π‘Ž})
62 imaeq1 6052 . . . . . . . . . . . . . 14 (β„Ž = 𝑔 β†’ (β„Ž β€œ {π‘₯}) = (𝑔 β€œ {π‘₯}))
6362sseq1d 4012 . . . . . . . . . . . . 13 (β„Ž = 𝑔 β†’ ((β„Ž β€œ {π‘₯}) βŠ† 𝑏 ↔ (𝑔 β€œ {π‘₯}) βŠ† 𝑏))
6416ad2antrr 724 . . . . . . . . . . . . 13 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ π‘₯ ∈ βˆͺ 𝑅) ∧ ((π‘Ž ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((π‘“β€˜π‘₯) ∈ π‘Ž ∧ (π‘”β€˜π‘₯) ∈ 𝑏 ∧ (π‘Ž ∩ 𝑏) = βˆ…))) β†’ 𝑔 ∈ (𝑅 Cn 𝑆))
6519ad2antrr 724 . . . . . . . . . . . . . . 15 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ π‘₯ ∈ βˆͺ 𝑅) ∧ ((π‘Ž ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((π‘“β€˜π‘₯) ∈ π‘Ž ∧ (π‘”β€˜π‘₯) ∈ 𝑏 ∧ (π‘Ž ∩ 𝑏) = βˆ…))) β†’ 𝑔 Fn βˆͺ 𝑅)
66 fnsnfv 6967 . . . . . . . . . . . . . . 15 ((𝑔 Fn βˆͺ 𝑅 ∧ π‘₯ ∈ βˆͺ 𝑅) β†’ {(π‘”β€˜π‘₯)} = (𝑔 β€œ {π‘₯}))
6765, 38, 66syl2anc 584 . . . . . . . . . . . . . 14 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ π‘₯ ∈ βˆͺ 𝑅) ∧ ((π‘Ž ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((π‘“β€˜π‘₯) ∈ π‘Ž ∧ (π‘”β€˜π‘₯) ∈ 𝑏 ∧ (π‘Ž ∩ 𝑏) = βˆ…))) β†’ {(π‘”β€˜π‘₯)} = (𝑔 β€œ {π‘₯}))
68 simprr2 1222 . . . . . . . . . . . . . . 15 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ π‘₯ ∈ βˆͺ 𝑅) ∧ ((π‘Ž ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((π‘“β€˜π‘₯) ∈ π‘Ž ∧ (π‘”β€˜π‘₯) ∈ 𝑏 ∧ (π‘Ž ∩ 𝑏) = βˆ…))) β†’ (π‘”β€˜π‘₯) ∈ 𝑏)
6968snssd 4811 . . . . . . . . . . . . . 14 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ π‘₯ ∈ βˆͺ 𝑅) ∧ ((π‘Ž ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((π‘“β€˜π‘₯) ∈ π‘Ž ∧ (π‘”β€˜π‘₯) ∈ 𝑏 ∧ (π‘Ž ∩ 𝑏) = βˆ…))) β†’ {(π‘”β€˜π‘₯)} βŠ† 𝑏)
7067, 69eqsstrrd 4020 . . . . . . . . . . . . 13 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ π‘₯ ∈ βˆͺ 𝑅) ∧ ((π‘Ž ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((π‘“β€˜π‘₯) ∈ π‘Ž ∧ (π‘”β€˜π‘₯) ∈ 𝑏 ∧ (π‘Ž ∩ 𝑏) = βˆ…))) β†’ (𝑔 β€œ {π‘₯}) βŠ† 𝑏)
7163, 64, 70elrabd 3684 . . . . . . . . . . . 12 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ π‘₯ ∈ βˆͺ 𝑅) ∧ ((π‘Ž ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((π‘“β€˜π‘₯) ∈ π‘Ž ∧ (π‘”β€˜π‘₯) ∈ 𝑏 ∧ (π‘Ž ∩ 𝑏) = βˆ…))) β†’ 𝑔 ∈ {β„Ž ∈ (𝑅 Cn 𝑆) ∣ (β„Ž β€œ {π‘₯}) βŠ† 𝑏})
72 inrab 4305 . . . . . . . . . . . . 13 ({β„Ž ∈ (𝑅 Cn 𝑆) ∣ (β„Ž β€œ {π‘₯}) βŠ† π‘Ž} ∩ {β„Ž ∈ (𝑅 Cn 𝑆) ∣ (β„Ž β€œ {π‘₯}) βŠ† 𝑏}) = {β„Ž ∈ (𝑅 Cn 𝑆) ∣ ((β„Ž β€œ {π‘₯}) βŠ† π‘Ž ∧ (β„Ž β€œ {π‘₯}) βŠ† 𝑏)}
73 simpllr 774 . . . . . . . . . . . . . . . . . 18 ((((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ π‘₯ ∈ βˆͺ 𝑅) ∧ ((π‘Ž ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((π‘“β€˜π‘₯) ∈ π‘Ž ∧ (π‘”β€˜π‘₯) ∈ 𝑏 ∧ (π‘Ž ∩ 𝑏) = βˆ…))) ∧ β„Ž ∈ (𝑅 Cn 𝑆)) β†’ π‘₯ ∈ βˆͺ 𝑅)
7411, 12cnf 22741 . . . . . . . . . . . . . . . . . . . 20 (β„Ž ∈ (𝑅 Cn 𝑆) β†’ β„Ž:βˆͺ π‘…βŸΆβˆͺ 𝑆)
7574fdmd 6725 . . . . . . . . . . . . . . . . . . 19 (β„Ž ∈ (𝑅 Cn 𝑆) β†’ dom β„Ž = βˆͺ 𝑅)
7675adantl 482 . . . . . . . . . . . . . . . . . 18 ((((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ π‘₯ ∈ βˆͺ 𝑅) ∧ ((π‘Ž ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((π‘“β€˜π‘₯) ∈ π‘Ž ∧ (π‘”β€˜π‘₯) ∈ 𝑏 ∧ (π‘Ž ∩ 𝑏) = βˆ…))) ∧ β„Ž ∈ (𝑅 Cn 𝑆)) β†’ dom β„Ž = βˆͺ 𝑅)
7773, 76eleqtrrd 2836 . . . . . . . . . . . . . . . . 17 ((((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ π‘₯ ∈ βˆͺ 𝑅) ∧ ((π‘Ž ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((π‘“β€˜π‘₯) ∈ π‘Ž ∧ (π‘”β€˜π‘₯) ∈ 𝑏 ∧ (π‘Ž ∩ 𝑏) = βˆ…))) ∧ β„Ž ∈ (𝑅 Cn 𝑆)) β†’ π‘₯ ∈ dom β„Ž)
78 simprr3 1223 . . . . . . . . . . . . . . . . . . . 20 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ π‘₯ ∈ βˆͺ 𝑅) ∧ ((π‘Ž ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((π‘“β€˜π‘₯) ∈ π‘Ž ∧ (π‘”β€˜π‘₯) ∈ 𝑏 ∧ (π‘Ž ∩ 𝑏) = βˆ…))) β†’ (π‘Ž ∩ 𝑏) = βˆ…)
7978adantr 481 . . . . . . . . . . . . . . . . . . 19 ((((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ π‘₯ ∈ βˆͺ 𝑅) ∧ ((π‘Ž ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((π‘“β€˜π‘₯) ∈ π‘Ž ∧ (π‘”β€˜π‘₯) ∈ 𝑏 ∧ (π‘Ž ∩ 𝑏) = βˆ…))) ∧ β„Ž ∈ (𝑅 Cn 𝑆)) β†’ (π‘Ž ∩ 𝑏) = βˆ…)
80 sseq0 4398 . . . . . . . . . . . . . . . . . . . 20 (((β„Ž β€œ {π‘₯}) βŠ† (π‘Ž ∩ 𝑏) ∧ (π‘Ž ∩ 𝑏) = βˆ…) β†’ (β„Ž β€œ {π‘₯}) = βˆ…)
8180expcom 414 . . . . . . . . . . . . . . . . . . 19 ((π‘Ž ∩ 𝑏) = βˆ… β†’ ((β„Ž β€œ {π‘₯}) βŠ† (π‘Ž ∩ 𝑏) β†’ (β„Ž β€œ {π‘₯}) = βˆ…))
8279, 81syl 17 . . . . . . . . . . . . . . . . . 18 ((((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ π‘₯ ∈ βˆͺ 𝑅) ∧ ((π‘Ž ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((π‘“β€˜π‘₯) ∈ π‘Ž ∧ (π‘”β€˜π‘₯) ∈ 𝑏 ∧ (π‘Ž ∩ 𝑏) = βˆ…))) ∧ β„Ž ∈ (𝑅 Cn 𝑆)) β†’ ((β„Ž β€œ {π‘₯}) βŠ† (π‘Ž ∩ 𝑏) β†’ (β„Ž β€œ {π‘₯}) = βˆ…))
83 imadisj 6076 . . . . . . . . . . . . . . . . . . 19 ((β„Ž β€œ {π‘₯}) = βˆ… ↔ (dom β„Ž ∩ {π‘₯}) = βˆ…)
84 disjsn 4714 . . . . . . . . . . . . . . . . . . 19 ((dom β„Ž ∩ {π‘₯}) = βˆ… ↔ Β¬ π‘₯ ∈ dom β„Ž)
8583, 84bitri 274 . . . . . . . . . . . . . . . . . 18 ((β„Ž β€œ {π‘₯}) = βˆ… ↔ Β¬ π‘₯ ∈ dom β„Ž)
8682, 85imbitrdi 250 . . . . . . . . . . . . . . . . 17 ((((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ π‘₯ ∈ βˆͺ 𝑅) ∧ ((π‘Ž ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((π‘“β€˜π‘₯) ∈ π‘Ž ∧ (π‘”β€˜π‘₯) ∈ 𝑏 ∧ (π‘Ž ∩ 𝑏) = βˆ…))) ∧ β„Ž ∈ (𝑅 Cn 𝑆)) β†’ ((β„Ž β€œ {π‘₯}) βŠ† (π‘Ž ∩ 𝑏) β†’ Β¬ π‘₯ ∈ dom β„Ž))
8777, 86mt2d 136 . . . . . . . . . . . . . . . 16 ((((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ π‘₯ ∈ βˆͺ 𝑅) ∧ ((π‘Ž ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((π‘“β€˜π‘₯) ∈ π‘Ž ∧ (π‘”β€˜π‘₯) ∈ 𝑏 ∧ (π‘Ž ∩ 𝑏) = βˆ…))) ∧ β„Ž ∈ (𝑅 Cn 𝑆)) β†’ Β¬ (β„Ž β€œ {π‘₯}) βŠ† (π‘Ž ∩ 𝑏))
88 ssin 4229 . . . . . . . . . . . . . . . 16 (((β„Ž β€œ {π‘₯}) βŠ† π‘Ž ∧ (β„Ž β€œ {π‘₯}) βŠ† 𝑏) ↔ (β„Ž β€œ {π‘₯}) βŠ† (π‘Ž ∩ 𝑏))
8987, 88sylnibr 328 . . . . . . . . . . . . . . 15 ((((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ π‘₯ ∈ βˆͺ 𝑅) ∧ ((π‘Ž ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((π‘“β€˜π‘₯) ∈ π‘Ž ∧ (π‘”β€˜π‘₯) ∈ 𝑏 ∧ (π‘Ž ∩ 𝑏) = βˆ…))) ∧ β„Ž ∈ (𝑅 Cn 𝑆)) β†’ Β¬ ((β„Ž β€œ {π‘₯}) βŠ† π‘Ž ∧ (β„Ž β€œ {π‘₯}) βŠ† 𝑏))
9089ralrimiva 3146 . . . . . . . . . . . . . 14 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ π‘₯ ∈ βˆͺ 𝑅) ∧ ((π‘Ž ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((π‘“β€˜π‘₯) ∈ π‘Ž ∧ (π‘”β€˜π‘₯) ∈ 𝑏 ∧ (π‘Ž ∩ 𝑏) = βˆ…))) β†’ βˆ€β„Ž ∈ (𝑅 Cn 𝑆) Β¬ ((β„Ž β€œ {π‘₯}) βŠ† π‘Ž ∧ (β„Ž β€œ {π‘₯}) βŠ† 𝑏))
91 rabeq0 4383 . . . . . . . . . . . . . 14 ({β„Ž ∈ (𝑅 Cn 𝑆) ∣ ((β„Ž β€œ {π‘₯}) βŠ† π‘Ž ∧ (β„Ž β€œ {π‘₯}) βŠ† 𝑏)} = βˆ… ↔ βˆ€β„Ž ∈ (𝑅 Cn 𝑆) Β¬ ((β„Ž β€œ {π‘₯}) βŠ† π‘Ž ∧ (β„Ž β€œ {π‘₯}) βŠ† 𝑏))
9290, 91sylibr 233 . . . . . . . . . . . . 13 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ π‘₯ ∈ βˆͺ 𝑅) ∧ ((π‘Ž ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((π‘“β€˜π‘₯) ∈ π‘Ž ∧ (π‘”β€˜π‘₯) ∈ 𝑏 ∧ (π‘Ž ∩ 𝑏) = βˆ…))) β†’ {β„Ž ∈ (𝑅 Cn 𝑆) ∣ ((β„Ž β€œ {π‘₯}) βŠ† π‘Ž ∧ (β„Ž β€œ {π‘₯}) βŠ† 𝑏)} = βˆ…)
9372, 92eqtrid 2784 . . . . . . . . . . . 12 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ π‘₯ ∈ βˆͺ 𝑅) ∧ ((π‘Ž ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((π‘“β€˜π‘₯) ∈ π‘Ž ∧ (π‘”β€˜π‘₯) ∈ 𝑏 ∧ (π‘Ž ∩ 𝑏) = βˆ…))) β†’ ({β„Ž ∈ (𝑅 Cn 𝑆) ∣ (β„Ž β€œ {π‘₯}) βŠ† π‘Ž} ∩ {β„Ž ∈ (𝑅 Cn 𝑆) ∣ (β„Ž β€œ {π‘₯}) βŠ† 𝑏}) = βˆ…)
94 eleq2 2822 . . . . . . . . . . . . . 14 (𝑒 = {β„Ž ∈ (𝑅 Cn 𝑆) ∣ (β„Ž β€œ {π‘₯}) βŠ† π‘Ž} β†’ (𝑓 ∈ 𝑒 ↔ 𝑓 ∈ {β„Ž ∈ (𝑅 Cn 𝑆) ∣ (β„Ž β€œ {π‘₯}) βŠ† π‘Ž}))
95 ineq1 4204 . . . . . . . . . . . . . . 15 (𝑒 = {β„Ž ∈ (𝑅 Cn 𝑆) ∣ (β„Ž β€œ {π‘₯}) βŠ† π‘Ž} β†’ (𝑒 ∩ 𝑣) = ({β„Ž ∈ (𝑅 Cn 𝑆) ∣ (β„Ž β€œ {π‘₯}) βŠ† π‘Ž} ∩ 𝑣))
9695eqeq1d 2734 . . . . . . . . . . . . . 14 (𝑒 = {β„Ž ∈ (𝑅 Cn 𝑆) ∣ (β„Ž β€œ {π‘₯}) βŠ† π‘Ž} β†’ ((𝑒 ∩ 𝑣) = βˆ… ↔ ({β„Ž ∈ (𝑅 Cn 𝑆) ∣ (β„Ž β€œ {π‘₯}) βŠ† π‘Ž} ∩ 𝑣) = βˆ…))
9794, 963anbi13d 1438 . . . . . . . . . . . . 13 (𝑒 = {β„Ž ∈ (𝑅 Cn 𝑆) ∣ (β„Ž β€œ {π‘₯}) βŠ† π‘Ž} β†’ ((𝑓 ∈ 𝑒 ∧ 𝑔 ∈ 𝑣 ∧ (𝑒 ∩ 𝑣) = βˆ…) ↔ (𝑓 ∈ {β„Ž ∈ (𝑅 Cn 𝑆) ∣ (β„Ž β€œ {π‘₯}) βŠ† π‘Ž} ∧ 𝑔 ∈ 𝑣 ∧ ({β„Ž ∈ (𝑅 Cn 𝑆) ∣ (β„Ž β€œ {π‘₯}) βŠ† π‘Ž} ∩ 𝑣) = βˆ…)))
98 eleq2 2822 . . . . . . . . . . . . . 14 (𝑣 = {β„Ž ∈ (𝑅 Cn 𝑆) ∣ (β„Ž β€œ {π‘₯}) βŠ† 𝑏} β†’ (𝑔 ∈ 𝑣 ↔ 𝑔 ∈ {β„Ž ∈ (𝑅 Cn 𝑆) ∣ (β„Ž β€œ {π‘₯}) βŠ† 𝑏}))
99 ineq2 4205 . . . . . . . . . . . . . . 15 (𝑣 = {β„Ž ∈ (𝑅 Cn 𝑆) ∣ (β„Ž β€œ {π‘₯}) βŠ† 𝑏} β†’ ({β„Ž ∈ (𝑅 Cn 𝑆) ∣ (β„Ž β€œ {π‘₯}) βŠ† π‘Ž} ∩ 𝑣) = ({β„Ž ∈ (𝑅 Cn 𝑆) ∣ (β„Ž β€œ {π‘₯}) βŠ† π‘Ž} ∩ {β„Ž ∈ (𝑅 Cn 𝑆) ∣ (β„Ž β€œ {π‘₯}) βŠ† 𝑏}))
10099eqeq1d 2734 . . . . . . . . . . . . . 14 (𝑣 = {β„Ž ∈ (𝑅 Cn 𝑆) ∣ (β„Ž β€œ {π‘₯}) βŠ† 𝑏} β†’ (({β„Ž ∈ (𝑅 Cn 𝑆) ∣ (β„Ž β€œ {π‘₯}) βŠ† π‘Ž} ∩ 𝑣) = βˆ… ↔ ({β„Ž ∈ (𝑅 Cn 𝑆) ∣ (β„Ž β€œ {π‘₯}) βŠ† π‘Ž} ∩ {β„Ž ∈ (𝑅 Cn 𝑆) ∣ (β„Ž β€œ {π‘₯}) βŠ† 𝑏}) = βˆ…))
10198, 1003anbi23d 1439 . . . . . . . . . . . . 13 (𝑣 = {β„Ž ∈ (𝑅 Cn 𝑆) ∣ (β„Ž β€œ {π‘₯}) βŠ† 𝑏} β†’ ((𝑓 ∈ {β„Ž ∈ (𝑅 Cn 𝑆) ∣ (β„Ž β€œ {π‘₯}) βŠ† π‘Ž} ∧ 𝑔 ∈ 𝑣 ∧ ({β„Ž ∈ (𝑅 Cn 𝑆) ∣ (β„Ž β€œ {π‘₯}) βŠ† π‘Ž} ∩ 𝑣) = βˆ…) ↔ (𝑓 ∈ {β„Ž ∈ (𝑅 Cn 𝑆) ∣ (β„Ž β€œ {π‘₯}) βŠ† π‘Ž} ∧ 𝑔 ∈ {β„Ž ∈ (𝑅 Cn 𝑆) ∣ (β„Ž β€œ {π‘₯}) βŠ† 𝑏} ∧ ({β„Ž ∈ (𝑅 Cn 𝑆) ∣ (β„Ž β€œ {π‘₯}) βŠ† π‘Ž} ∩ {β„Ž ∈ (𝑅 Cn 𝑆) ∣ (β„Ž β€œ {π‘₯}) βŠ† 𝑏}) = βˆ…)))
10297, 101rspc2ev 3623 . . . . . . . . . . . 12 (({β„Ž ∈ (𝑅 Cn 𝑆) ∣ (β„Ž β€œ {π‘₯}) βŠ† π‘Ž} ∈ (𝑆 ↑ko 𝑅) ∧ {β„Ž ∈ (𝑅 Cn 𝑆) ∣ (β„Ž β€œ {π‘₯}) βŠ† 𝑏} ∈ (𝑆 ↑ko 𝑅) ∧ (𝑓 ∈ {β„Ž ∈ (𝑅 Cn 𝑆) ∣ (β„Ž β€œ {π‘₯}) βŠ† π‘Ž} ∧ 𝑔 ∈ {β„Ž ∈ (𝑅 Cn 𝑆) ∣ (β„Ž β€œ {π‘₯}) βŠ† 𝑏} ∧ ({β„Ž ∈ (𝑅 Cn 𝑆) ∣ (β„Ž β€œ {π‘₯}) βŠ† π‘Ž} ∩ {β„Ž ∈ (𝑅 Cn 𝑆) ∣ (β„Ž β€œ {π‘₯}) βŠ† 𝑏}) = βˆ…)) β†’ βˆƒπ‘’ ∈ (𝑆 ↑ko 𝑅)βˆƒπ‘£ ∈ (𝑆 ↑ko 𝑅)(𝑓 ∈ 𝑒 ∧ 𝑔 ∈ 𝑣 ∧ (𝑒 ∩ 𝑣) = βˆ…))
10349, 51, 61, 71, 93, 102syl113anc 1382 . . . . . . . . . . 11 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ π‘₯ ∈ βˆͺ 𝑅) ∧ ((π‘Ž ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ ((π‘“β€˜π‘₯) ∈ π‘Ž ∧ (π‘”β€˜π‘₯) ∈ 𝑏 ∧ (π‘Ž ∩ 𝑏) = βˆ…))) β†’ βˆƒπ‘’ ∈ (𝑆 ↑ko 𝑅)βˆƒπ‘£ ∈ (𝑆 ↑ko 𝑅)(𝑓 ∈ 𝑒 ∧ 𝑔 ∈ 𝑣 ∧ (𝑒 ∩ 𝑣) = βˆ…))
104103expr 457 . . . . . . . . . 10 (((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ π‘₯ ∈ βˆͺ 𝑅) ∧ (π‘Ž ∈ 𝑆 ∧ 𝑏 ∈ 𝑆)) β†’ (((π‘“β€˜π‘₯) ∈ π‘Ž ∧ (π‘”β€˜π‘₯) ∈ 𝑏 ∧ (π‘Ž ∩ 𝑏) = βˆ…) β†’ βˆƒπ‘’ ∈ (𝑆 ↑ko 𝑅)βˆƒπ‘£ ∈ (𝑆 ↑ko 𝑅)(𝑓 ∈ 𝑒 ∧ 𝑔 ∈ 𝑣 ∧ (𝑒 ∩ 𝑣) = βˆ…)))
105104rexlimdvva 3211 . . . . . . . . 9 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ π‘₯ ∈ βˆͺ 𝑅) β†’ (βˆƒπ‘Ž ∈ 𝑆 βˆƒπ‘ ∈ 𝑆 ((π‘“β€˜π‘₯) ∈ π‘Ž ∧ (π‘”β€˜π‘₯) ∈ 𝑏 ∧ (π‘Ž ∩ 𝑏) = βˆ…) β†’ βˆƒπ‘’ ∈ (𝑆 ↑ko 𝑅)βˆƒπ‘£ ∈ (𝑆 ↑ko 𝑅)(𝑓 ∈ 𝑒 ∧ 𝑔 ∈ 𝑣 ∧ (𝑒 ∩ 𝑣) = βˆ…)))
10635, 105syld 47 . . . . . . . 8 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) ∧ π‘₯ ∈ βˆͺ 𝑅) β†’ (Β¬ (π‘“β€˜π‘₯) = (π‘”β€˜π‘₯) β†’ βˆƒπ‘’ ∈ (𝑆 ↑ko 𝑅)βˆƒπ‘£ ∈ (𝑆 ↑ko 𝑅)(𝑓 ∈ 𝑒 ∧ 𝑔 ∈ 𝑣 ∧ (𝑒 ∩ 𝑣) = βˆ…)))
107106rexlimdva 3155 . . . . . . 7 (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) β†’ (βˆƒπ‘₯ ∈ βˆͺ 𝑅 Β¬ (π‘“β€˜π‘₯) = (π‘”β€˜π‘₯) β†’ βˆƒπ‘’ ∈ (𝑆 ↑ko 𝑅)βˆƒπ‘£ ∈ (𝑆 ↑ko 𝑅)(𝑓 ∈ 𝑒 ∧ 𝑔 ∈ 𝑣 ∧ (𝑒 ∩ 𝑣) = βˆ…)))
10823, 107biimtrrid 242 . . . . . 6 (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) β†’ (Β¬ βˆ€π‘₯ ∈ βˆͺ 𝑅(π‘“β€˜π‘₯) = (π‘”β€˜π‘₯) β†’ βˆƒπ‘’ ∈ (𝑆 ↑ko 𝑅)βˆƒπ‘£ ∈ (𝑆 ↑ko 𝑅)(𝑓 ∈ 𝑒 ∧ 𝑔 ∈ 𝑣 ∧ (𝑒 ∩ 𝑣) = βˆ…)))
10922, 108sylbid 239 . . . . 5 (((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) ∧ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆))) β†’ (𝑓 β‰  𝑔 β†’ βˆƒπ‘’ ∈ (𝑆 ↑ko 𝑅)βˆƒπ‘£ ∈ (𝑆 ↑ko 𝑅)(𝑓 ∈ 𝑒 ∧ 𝑔 ∈ 𝑣 ∧ (𝑒 ∩ 𝑣) = βˆ…)))
110109ex 413 . . . 4 ((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) β†’ ((𝑓 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑅 Cn 𝑆)) β†’ (𝑓 β‰  𝑔 β†’ βˆƒπ‘’ ∈ (𝑆 ↑ko 𝑅)βˆƒπ‘£ ∈ (𝑆 ↑ko 𝑅)(𝑓 ∈ 𝑒 ∧ 𝑔 ∈ 𝑣 ∧ (𝑒 ∩ 𝑣) = βˆ…))))
1119, 110sylbird 259 . . 3 ((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) β†’ ((𝑓 ∈ βˆͺ (𝑆 ↑ko 𝑅) ∧ 𝑔 ∈ βˆͺ (𝑆 ↑ko 𝑅)) β†’ (𝑓 β‰  𝑔 β†’ βˆƒπ‘’ ∈ (𝑆 ↑ko 𝑅)βˆƒπ‘£ ∈ (𝑆 ↑ko 𝑅)(𝑓 ∈ 𝑒 ∧ 𝑔 ∈ 𝑣 ∧ (𝑒 ∩ 𝑣) = βˆ…))))
112111ralrimivv 3198 . 2 ((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) β†’ βˆ€π‘“ ∈ βˆͺ (𝑆 ↑ko 𝑅)βˆ€π‘” ∈ βˆͺ (𝑆 ↑ko 𝑅)(𝑓 β‰  𝑔 β†’ βˆƒπ‘’ ∈ (𝑆 ↑ko 𝑅)βˆƒπ‘£ ∈ (𝑆 ↑ko 𝑅)(𝑓 ∈ 𝑒 ∧ 𝑔 ∈ 𝑣 ∧ (𝑒 ∩ 𝑣) = βˆ…)))
113 eqid 2732 . . 3 βˆͺ (𝑆 ↑ko 𝑅) = βˆͺ (𝑆 ↑ko 𝑅)
114113ishaus 22817 . 2 ((𝑆 ↑ko 𝑅) ∈ Haus ↔ ((𝑆 ↑ko 𝑅) ∈ Top ∧ βˆ€π‘“ ∈ βˆͺ (𝑆 ↑ko 𝑅)βˆ€π‘” ∈ βˆͺ (𝑆 ↑ko 𝑅)(𝑓 β‰  𝑔 β†’ βˆƒπ‘’ ∈ (𝑆 ↑ko 𝑅)βˆƒπ‘£ ∈ (𝑆 ↑ko 𝑅)(𝑓 ∈ 𝑒 ∧ 𝑔 ∈ 𝑣 ∧ (𝑒 ∩ 𝑣) = βˆ…))))
1153, 112, 114sylanbrc 583 1 ((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) β†’ (𝑆 ↑ko 𝑅) ∈ Haus)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106   β‰  wne 2940  βˆ€wral 3061  βˆƒwrex 3070  {crab 3432   ∩ cin 3946   βŠ† wss 3947  βˆ…c0 4321  π’« cpw 4601  {csn 4627  βˆͺ cuni 4907  dom cdm 5675   β€œ cima 5678   Fn wfn 6535  βŸΆwf 6536  β€˜cfv 6540  (class class class)co 7405  Fincfn 8935   β†Ύt crest 17362  Topctop 22386  TopOnctopon 22403   Cn ccn 22719  Hauscha 22803  Compccmp 22881   ↑ko cxko 23056
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7852  df-1st 7971  df-2nd 7972  df-1o 8462  df-er 8699  df-map 8818  df-en 8936  df-fin 8939  df-fi 9402  df-rest 17364  df-topgen 17385  df-top 22387  df-topon 22404  df-bases 22440  df-cn 22722  df-haus 22810  df-cmp 22882  df-xko 23058
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator