hausgraph - Mathbox for Stefan O'Rear

	Mathbox for Stefan O'Rear		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > hausgraph		Structured version Visualization version GIF version

Theorem hausgraph 37790

Description: The graph of a continuous function into a Hausdorff space is closed. (Contributed by Stefan O'Rear, 25-Jan-2015.)

**Assertion**
Ref	Expression
hausgraph	⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹 ∈ (Clsd‘(𝐽 ×_t 𝐾)))

Proof of Theorem hausgraph Dummy variable 𝑎 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		f1stres 7190	. . . . . . . . 9 ⊢ (1^st ↾ (∪ 𝐽 × ∪ 𝐾)):(∪ 𝐽 × ∪ 𝐾)⟶∪ 𝐽
2		ffn 6045	. . . . . . . . 9 ⊢ ((1^st ↾ (∪ 𝐽 × ∪ 𝐾)):(∪ 𝐽 × ∪ 𝐾)⟶∪ 𝐽 → (1^st ↾ (∪ 𝐽 × ∪ 𝐾)) Fn (∪ 𝐽 × ∪ 𝐾))
3	1, 2	ax-mp 5	. . . . . . . 8 ⊢ (1^st ↾ (∪ 𝐽 × ∪ 𝐾)) Fn (∪ 𝐽 × ∪ 𝐾)
4		fvco2 6273	. . . . . . . 8 ⊢ (((1^st ↾ (∪ 𝐽 × ∪ 𝐾)) Fn (∪ 𝐽 × ∪ 𝐾) ∧ 𝑎 ∈ (∪ 𝐽 × ∪ 𝐾)) → ((𝐹 ∘ (1^st ↾ (∪ 𝐽 × ∪ 𝐾)))‘𝑎) = (𝐹‘((1^st ↾ (∪ 𝐽 × ∪ 𝐾))‘𝑎)))
5	3, 4	mpan 706	. . . . . . 7 ⊢ (𝑎 ∈ (∪ 𝐽 × ∪ 𝐾) → ((𝐹 ∘ (1^st ↾ (∪ 𝐽 × ∪ 𝐾)))‘𝑎) = (𝐹‘((1^st ↾ (∪ 𝐽 × ∪ 𝐾))‘𝑎)))
6	5	adantl 482	. . . . . 6 ⊢ (((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑎 ∈ (∪ 𝐽 × ∪ 𝐾)) → ((𝐹 ∘ (1^st ↾ (∪ 𝐽 × ∪ 𝐾)))‘𝑎) = (𝐹‘((1^st ↾ (∪ 𝐽 × ∪ 𝐾))‘𝑎)))
7		fvres 6207	. . . . . . . 8 ⊢ (𝑎 ∈ (∪ 𝐽 × ∪ 𝐾) → ((1^st ↾ (∪ 𝐽 × ∪ 𝐾))‘𝑎) = (1^st ‘𝑎))
8	7	fveq2d 6195	. . . . . . 7 ⊢ (𝑎 ∈ (∪ 𝐽 × ∪ 𝐾) → (𝐹‘((1^st ↾ (∪ 𝐽 × ∪ 𝐾))‘𝑎)) = (𝐹‘(1^st ‘𝑎)))
9	8	adantl 482	. . . . . 6 ⊢ (((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑎 ∈ (∪ 𝐽 × ∪ 𝐾)) → (𝐹‘((1^st ↾ (∪ 𝐽 × ∪ 𝐾))‘𝑎)) = (𝐹‘(1^st ‘𝑎)))
10	6, 9	eqtrd 2656	. . . . 5 ⊢ (((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑎 ∈ (∪ 𝐽 × ∪ 𝐾)) → ((𝐹 ∘ (1^st ↾ (∪ 𝐽 × ∪ 𝐾)))‘𝑎) = (𝐹‘(1^st ‘𝑎)))
11		fvres 6207	. . . . . 6 ⊢ (𝑎 ∈ (∪ 𝐽 × ∪ 𝐾) → ((2^nd ↾ (∪ 𝐽 × ∪ 𝐾))‘𝑎) = (2^nd ‘𝑎))
12	11	adantl 482	. . . . 5 ⊢ (((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑎 ∈ (∪ 𝐽 × ∪ 𝐾)) → ((2^nd ↾ (∪ 𝐽 × ∪ 𝐾))‘𝑎) = (2^nd ‘𝑎))
13	10, 12	eqeq12d 2637	. . . 4 ⊢ (((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑎 ∈ (∪ 𝐽 × ∪ 𝐾)) → (((𝐹 ∘ (1^st ↾ (∪ 𝐽 × ∪ 𝐾)))‘𝑎) = ((2^nd ↾ (∪ 𝐽 × ∪ 𝐾))‘𝑎) ↔ (𝐹‘(1^st ‘𝑎)) = (2^nd ‘𝑎)))
14	13	rabbidva 3188	. . 3 ⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → {𝑎 ∈ (∪ 𝐽 × ∪ 𝐾) ∣ ((𝐹 ∘ (1^st ↾ (∪ 𝐽 × ∪ 𝐾)))‘𝑎) = ((2^nd ↾ (∪ 𝐽 × ∪ 𝐾))‘𝑎)} = {𝑎 ∈ (∪ 𝐽 × ∪ 𝐾) ∣ (𝐹‘(1^st ‘𝑎)) = (2^nd ‘𝑎)})
15		eqid 2622	. . . . . . . 8 ⊢ ∪ 𝐽 = ∪ 𝐽
16		eqid 2622	. . . . . . . 8 ⊢ ∪ 𝐾 = ∪ 𝐾
17	15, 16	cnf 21050	. . . . . . 7 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹:∪ 𝐽⟶∪ 𝐾)
18	17	adantl 482	. . . . . 6 ⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹:∪ 𝐽⟶∪ 𝐾)
19		fco 6058	. . . . . 6 ⊢ ((𝐹:∪ 𝐽⟶∪ 𝐾 ∧ (1^st ↾ (∪ 𝐽 × ∪ 𝐾)):(∪ 𝐽 × ∪ 𝐾)⟶∪ 𝐽) → (𝐹 ∘ (1^st ↾ (∪ 𝐽 × ∪ 𝐾))):(∪ 𝐽 × ∪ 𝐾)⟶∪ 𝐾)
20	18, 1, 19	sylancl 694	. . . . 5 ⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (𝐹 ∘ (1^st ↾ (∪ 𝐽 × ∪ 𝐾))):(∪ 𝐽 × ∪ 𝐾)⟶∪ 𝐾)
21		ffn 6045	. . . . 5 ⊢ ((𝐹 ∘ (1^st ↾ (∪ 𝐽 × ∪ 𝐾))):(∪ 𝐽 × ∪ 𝐾)⟶∪ 𝐾 → (𝐹 ∘ (1^st ↾ (∪ 𝐽 × ∪ 𝐾))) Fn (∪ 𝐽 × ∪ 𝐾))
22	20, 21	syl 17	. . . 4 ⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (𝐹 ∘ (1^st ↾ (∪ 𝐽 × ∪ 𝐾))) Fn (∪ 𝐽 × ∪ 𝐾))
23		f2ndres 7191	. . . . 5 ⊢ (2^nd ↾ (∪ 𝐽 × ∪ 𝐾)):(∪ 𝐽 × ∪ 𝐾)⟶∪ 𝐾
24		ffn 6045	. . . . 5 ⊢ ((2^nd ↾ (∪ 𝐽 × ∪ 𝐾)):(∪ 𝐽 × ∪ 𝐾)⟶∪ 𝐾 → (2^nd ↾ (∪ 𝐽 × ∪ 𝐾)) Fn (∪ 𝐽 × ∪ 𝐾))
25	23, 24	ax-mp 5	. . . 4 ⊢ (2^nd ↾ (∪ 𝐽 × ∪ 𝐾)) Fn (∪ 𝐽 × ∪ 𝐾)
26		fndmin 6324	. . . 4 ⊢ (((𝐹 ∘ (1^st ↾ (∪ 𝐽 × ∪ 𝐾))) Fn (∪ 𝐽 × ∪ 𝐾) ∧ (2^nd ↾ (∪ 𝐽 × ∪ 𝐾)) Fn (∪ 𝐽 × ∪ 𝐾)) → dom ((𝐹 ∘ (1^st ↾ (∪ 𝐽 × ∪ 𝐾))) ∩ (2^nd ↾ (∪ 𝐽 × ∪ 𝐾))) = {𝑎 ∈ (∪ 𝐽 × ∪ 𝐾) ∣ ((𝐹 ∘ (1^st ↾ (∪ 𝐽 × ∪ 𝐾)))‘𝑎) = ((2^nd ↾ (∪ 𝐽 × ∪ 𝐾))‘𝑎)})
27	22, 25, 26	sylancl 694	. . 3 ⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → dom ((𝐹 ∘ (1^st ↾ (∪ 𝐽 × ∪ 𝐾))) ∩ (2^nd ↾ (∪ 𝐽 × ∪ 𝐾))) = {𝑎 ∈ (∪ 𝐽 × ∪ 𝐾) ∣ ((𝐹 ∘ (1^st ↾ (∪ 𝐽 × ∪ 𝐾)))‘𝑎) = ((2^nd ↾ (∪ 𝐽 × ∪ 𝐾))‘𝑎)})
28		fgraphxp 37789	. . . 4 ⊢ (𝐹:∪ 𝐽⟶∪ 𝐾 → 𝐹 = {𝑎 ∈ (∪ 𝐽 × ∪ 𝐾) ∣ (𝐹‘(1^st ‘𝑎)) = (2^nd ‘𝑎)})
29	18, 28	syl 17	. . 3 ⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹 = {𝑎 ∈ (∪ 𝐽 × ∪ 𝐾) ∣ (𝐹‘(1^st ‘𝑎)) = (2^nd ‘𝑎)})
30	14, 27, 29	3eqtr4rd 2667	. 2 ⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹 = dom ((𝐹 ∘ (1^st ↾ (∪ 𝐽 × ∪ 𝐾))) ∩ (2^nd ↾ (∪ 𝐽 × ∪ 𝐾))))
31		simpl 473	. . 3 ⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐾 ∈ Haus)
32		cntop1 21044	. . . . . . 7 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐽 ∈ Top)
33	32	adantl 482	. . . . . 6 ⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐽 ∈ Top)
34	15	toptopon 20722	. . . . . 6 ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘∪ 𝐽))
35	33, 34	sylib 208	. . . . 5 ⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐽 ∈ (TopOn‘∪ 𝐽))
36		haustop 21135	. . . . . . 7 ⊢ (𝐾 ∈ Haus → 𝐾 ∈ Top)
37	31, 36	syl 17	. . . . . 6 ⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐾 ∈ Top)
38	16	toptopon 20722	. . . . . 6 ⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘∪ 𝐾))
39	37, 38	sylib 208	. . . . 5 ⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐾 ∈ (TopOn‘∪ 𝐾))
40		tx1cn 21412	. . . . 5 ⊢ ((𝐽 ∈ (TopOn‘∪ 𝐽) ∧ 𝐾 ∈ (TopOn‘∪ 𝐾)) → (1^st ↾ (∪ 𝐽 × ∪ 𝐾)) ∈ ((𝐽 ×_t 𝐾) Cn 𝐽))
41	35, 39, 40	syl2anc 693	. . . 4 ⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (1^st ↾ (∪ 𝐽 × ∪ 𝐾)) ∈ ((𝐽 ×_t 𝐾) Cn 𝐽))
42		cnco 21070	. . . 4 ⊢ (((1^st ↾ (∪ 𝐽 × ∪ 𝐾)) ∈ ((𝐽 ×_t 𝐾) Cn 𝐽) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (𝐹 ∘ (1^st ↾ (∪ 𝐽 × ∪ 𝐾))) ∈ ((𝐽 ×_t 𝐾) Cn 𝐾))
43	41, 42	sylancom 701	. . 3 ⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (𝐹 ∘ (1^st ↾ (∪ 𝐽 × ∪ 𝐾))) ∈ ((𝐽 ×_t 𝐾) Cn 𝐾))
44		tx2cn 21413	. . . 4 ⊢ ((𝐽 ∈ (TopOn‘∪ 𝐽) ∧ 𝐾 ∈ (TopOn‘∪ 𝐾)) → (2^nd ↾ (∪ 𝐽 × ∪ 𝐾)) ∈ ((𝐽 ×_t 𝐾) Cn 𝐾))
45	35, 39, 44	syl2anc 693	. . 3 ⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (2^nd ↾ (∪ 𝐽 × ∪ 𝐾)) ∈ ((𝐽 ×_t 𝐾) Cn 𝐾))
46	31, 43, 45	hauseqlcld 21449	. 2 ⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → dom ((𝐹 ∘ (1^st ↾ (∪ 𝐽 × ∪ 𝐾))) ∩ (2^nd ↾ (∪ 𝐽 × ∪ 𝐾))) ∈ (Clsd‘(𝐽 ×_t 𝐾)))
47	30, 46	eqeltrd 2701	1 ⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹 ∈ (Clsd‘(𝐽 ×_t 𝐾)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 384 = wceq 1483 ∈ wcel 1990 {crab 2916 ∩ cin 3573 ∪ cuni 4436 × cxp 5112 dom cdm 5114 ↾ cres 5116 ∘ ccom 5118 Fn wfn 5883 ⟶wf 5884 ‘cfv 5888 (class class class)co 6650 1^st c1st 7166 2^nd c2nd 7167 Topctop 20698 TopOnctopon 20715 Clsdccld 20820 Cn ccn 21028 Hauscha 21112 ×_t ctx 21363

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-ral 2917 df-rex 2918 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-op 4184 df-uni 4437 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-id 5024 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-1st 7168 df-2nd 7169 df-map 7859 df-topgen 16104 df-top 20699 df-topon 20716 df-bases 20750 df-cld 20823 df-cn 21031 df-haus 21119 df-tx 21365

This theorem is referenced by: (None)

W3C validator