nrmhmph - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > nrmhmph		Structured version Visualization version GIF version

Theorem nrmhmph 23737

Description: Normality is a topological property. (Contributed by Mario Carneiro, 25-Aug-2015.)

**Assertion**
Ref	Expression
nrmhmph	⊢ (𝐽 ≃ 𝐾 → (𝐽 ∈ Nrm → 𝐾 ∈ Nrm))

Proof of Theorem nrmhmph Dummy variables 𝑤 𝑓 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		hmph 23719	. 2 ⊢ (𝐽 ≃ 𝐾 ↔ (𝐽Homeo𝐾) ≠ ∅)
2		n0 4333	. . 3 ⊢ ((𝐽Homeo𝐾) ≠ ∅ ↔ ∃𝑓 𝑓 ∈ (𝐽Homeo𝐾))
3		hmeocn 23703	. . . . . . . 8 ⊢ (𝑓 ∈ (𝐽Homeo𝐾) → 𝑓 ∈ (𝐽 Cn 𝐾))
4	3	adantl 481	. . . . . . 7 ⊢ ((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) → 𝑓 ∈ (𝐽 Cn 𝐾))
5		cntop2 23184	. . . . . . 7 ⊢ (𝑓 ∈ (𝐽 Cn 𝐾) → 𝐾 ∈ Top)
6	4, 5	syl 17	. . . . . 6 ⊢ ((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) → 𝐾 ∈ Top)
7		simpll 766	. . . . . . . . 9 ⊢ (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → 𝐽 ∈ Nrm)
8	4	adantr 480	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → 𝑓 ∈ (𝐽 Cn 𝐾))
9		simprl 770	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → 𝑥 ∈ 𝐾)
10		cnima 23208	. . . . . . . . . 10 ⊢ ((𝑓 ∈ (𝐽 Cn 𝐾) ∧ 𝑥 ∈ 𝐾) → (^◡𝑓 “ 𝑥) ∈ 𝐽)
11	8, 9, 10	syl2anc 584	. . . . . . . . 9 ⊢ (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → (^◡𝑓 “ 𝑥) ∈ 𝐽)
12		simprr 772	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))
13	12	elin1d 4184	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → 𝑦 ∈ (Clsd‘𝐾))
14		cnclima 23211	. . . . . . . . . 10 ⊢ ((𝑓 ∈ (𝐽 Cn 𝐾) ∧ 𝑦 ∈ (Clsd‘𝐾)) → (^◡𝑓 “ 𝑦) ∈ (Clsd‘𝐽))
15	8, 13, 14	syl2anc 584	. . . . . . . . 9 ⊢ (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → (^◡𝑓 “ 𝑦) ∈ (Clsd‘𝐽))
16	12	elin2d 4185	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → 𝑦 ∈ 𝒫 𝑥)
17	16	elpwid 4589	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → 𝑦 ⊆ 𝑥)
18		imass2 6094	. . . . . . . . . 10 ⊢ (𝑦 ⊆ 𝑥 → (^◡𝑓 “ 𝑦) ⊆ (^◡𝑓 “ 𝑥))
19	17, 18	syl 17	. . . . . . . . 9 ⊢ (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → (^◡𝑓 “ 𝑦) ⊆ (^◡𝑓 “ 𝑥))
20		nrmsep3 23298	. . . . . . . . 9 ⊢ ((𝐽 ∈ Nrm ∧ ((^◡𝑓 “ 𝑥) ∈ 𝐽 ∧ (^◡𝑓 “ 𝑦) ∈ (Clsd‘𝐽) ∧ (^◡𝑓 “ 𝑦) ⊆ (^◡𝑓 “ 𝑥))) → ∃𝑤 ∈ 𝐽 ((^◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝑓 “ 𝑥)))
21	7, 11, 15, 19, 20	syl13anc 1374	. . . . . . . 8 ⊢ (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → ∃𝑤 ∈ 𝐽 ((^◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝑓 “ 𝑥)))
22		simpllr 775	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((^◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝑓 “ 𝑥)))) → 𝑓 ∈ (𝐽Homeo𝐾))
23		simprl 770	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((^◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝑓 “ 𝑥)))) → 𝑤 ∈ 𝐽)
24		hmeoima 23708	. . . . . . . . . 10 ⊢ ((𝑓 ∈ (𝐽Homeo𝐾) ∧ 𝑤 ∈ 𝐽) → (𝑓 “ 𝑤) ∈ 𝐾)
25	22, 23, 24	syl2anc 584	. . . . . . . . 9 ⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((^◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝑓 “ 𝑥)))) → (𝑓 “ 𝑤) ∈ 𝐾)
26		simprrl 780	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((^◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝑓 “ 𝑥)))) → (^◡𝑓 “ 𝑦) ⊆ 𝑤)
27		eqid 2736	. . . . . . . . . . . . . 14 ⊢ ∪ 𝐽 = ∪ 𝐽
28		eqid 2736	. . . . . . . . . . . . . 14 ⊢ ∪ 𝐾 = ∪ 𝐾
29	27, 28	hmeof1o 23707	. . . . . . . . . . . . 13 ⊢ (𝑓 ∈ (𝐽Homeo𝐾) → 𝑓:∪ 𝐽–1-1-onto→∪ 𝐾)
30	22, 29	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((^◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝑓 “ 𝑥)))) → 𝑓:∪ 𝐽–1-1-onto→∪ 𝐾)
31		f1ofun 6825	. . . . . . . . . . . 12 ⊢ (𝑓:∪ 𝐽–1-1-onto→∪ 𝐾 → Fun 𝑓)
32	30, 31	syl 17	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((^◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝑓 “ 𝑥)))) → Fun 𝑓)
33	13	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((^◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝑓 “ 𝑥)))) → 𝑦 ∈ (Clsd‘𝐾))
34	28	cldss 22972	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ (Clsd‘𝐾) → 𝑦 ⊆ ∪ 𝐾)
35	33, 34	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((^◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝑓 “ 𝑥)))) → 𝑦 ⊆ ∪ 𝐾)
36		f1ofo 6830	. . . . . . . . . . . . 13 ⊢ (𝑓:∪ 𝐽–1-1-onto→∪ 𝐾 → 𝑓:∪ 𝐽–onto→∪ 𝐾)
37		forn 6798	. . . . . . . . . . . . 13 ⊢ (𝑓:∪ 𝐽–onto→∪ 𝐾 → ran 𝑓 = ∪ 𝐾)
38	30, 36, 37	3syl 18	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((^◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝑓 “ 𝑥)))) → ran 𝑓 = ∪ 𝐾)
39	35, 38	sseqtrrd 4001	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((^◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝑓 “ 𝑥)))) → 𝑦 ⊆ ran 𝑓)
40		funimass1 6623	. . . . . . . . . . 11 ⊢ ((Fun 𝑓 ∧ 𝑦 ⊆ ran 𝑓) → ((^◡𝑓 “ 𝑦) ⊆ 𝑤 → 𝑦 ⊆ (𝑓 “ 𝑤)))
41	32, 39, 40	syl2anc 584	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((^◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝑓 “ 𝑥)))) → ((^◡𝑓 “ 𝑦) ⊆ 𝑤 → 𝑦 ⊆ (𝑓 “ 𝑤)))
42	26, 41	mpd 15	. . . . . . . . 9 ⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((^◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝑓 “ 𝑥)))) → 𝑦 ⊆ (𝑓 “ 𝑤))
43		elssuni 4918	. . . . . . . . . . . 12 ⊢ (𝑤 ∈ 𝐽 → 𝑤 ⊆ ∪ 𝐽)
44	43	ad2antrl 728	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((^◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝑓 “ 𝑥)))) → 𝑤 ⊆ ∪ 𝐽)
45	27	hmeocls 23711	. . . . . . . . . . 11 ⊢ ((𝑓 ∈ (𝐽Homeo𝐾) ∧ 𝑤 ⊆ ∪ 𝐽) → ((cls‘𝐾)‘(𝑓 “ 𝑤)) = (𝑓 “ ((cls‘𝐽)‘𝑤)))
46	22, 44, 45	syl2anc 584	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((^◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝑓 “ 𝑥)))) → ((cls‘𝐾)‘(𝑓 “ 𝑤)) = (𝑓 “ ((cls‘𝐽)‘𝑤)))
47		simprrr 781	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((^◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝑓 “ 𝑥)))) → ((cls‘𝐽)‘𝑤) ⊆ (^◡𝑓 “ 𝑥))
48		nrmtop 23279	. . . . . . . . . . . . . . 15 ⊢ (𝐽 ∈ Nrm → 𝐽 ∈ Top)
49	48	ad3antrrr 730	. . . . . . . . . . . . . 14 ⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((^◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝑓 “ 𝑥)))) → 𝐽 ∈ Top)
50	27	clsss3 23002	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ Top ∧ 𝑤 ⊆ ∪ 𝐽) → ((cls‘𝐽)‘𝑤) ⊆ ∪ 𝐽)
51	49, 44, 50	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((^◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝑓 “ 𝑥)))) → ((cls‘𝐽)‘𝑤) ⊆ ∪ 𝐽)
52		f1odm 6827	. . . . . . . . . . . . . 14 ⊢ (𝑓:∪ 𝐽–1-1-onto→∪ 𝐾 → dom 𝑓 = ∪ 𝐽)
53	30, 52	syl 17	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((^◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝑓 “ 𝑥)))) → dom 𝑓 = ∪ 𝐽)
54	51, 53	sseqtrrd 4001	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((^◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝑓 “ 𝑥)))) → ((cls‘𝐽)‘𝑤) ⊆ dom 𝑓)
55		funimass3 7049	. . . . . . . . . . . 12 ⊢ ((Fun 𝑓 ∧ ((cls‘𝐽)‘𝑤) ⊆ dom 𝑓) → ((𝑓 “ ((cls‘𝐽)‘𝑤)) ⊆ 𝑥 ↔ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝑓 “ 𝑥)))
56	32, 54, 55	syl2anc 584	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((^◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝑓 “ 𝑥)))) → ((𝑓 “ ((cls‘𝐽)‘𝑤)) ⊆ 𝑥 ↔ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝑓 “ 𝑥)))
57	47, 56	mpbird 257	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((^◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝑓 “ 𝑥)))) → (𝑓 “ ((cls‘𝐽)‘𝑤)) ⊆ 𝑥)
58	46, 57	eqsstrd 3998	. . . . . . . . 9 ⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((^◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝑓 “ 𝑥)))) → ((cls‘𝐾)‘(𝑓 “ 𝑤)) ⊆ 𝑥)
59		sseq2 3990	. . . . . . . . . . 11 ⊢ (𝑧 = (𝑓 “ 𝑤) → (𝑦 ⊆ 𝑧 ↔ 𝑦 ⊆ (𝑓 “ 𝑤)))
60		fveq2 6881	. . . . . . . . . . . 12 ⊢ (𝑧 = (𝑓 “ 𝑤) → ((cls‘𝐾)‘𝑧) = ((cls‘𝐾)‘(𝑓 “ 𝑤)))
61	60	sseq1d 3995	. . . . . . . . . . 11 ⊢ (𝑧 = (𝑓 “ 𝑤) → (((cls‘𝐾)‘𝑧) ⊆ 𝑥 ↔ ((cls‘𝐾)‘(𝑓 “ 𝑤)) ⊆ 𝑥))
62	59, 61	anbi12d 632	. . . . . . . . . 10 ⊢ (𝑧 = (𝑓 “ 𝑤) → ((𝑦 ⊆ 𝑧 ∧ ((cls‘𝐾)‘𝑧) ⊆ 𝑥) ↔ (𝑦 ⊆ (𝑓 “ 𝑤) ∧ ((cls‘𝐾)‘(𝑓 “ 𝑤)) ⊆ 𝑥)))
63	62	rspcev 3606	. . . . . . . . 9 ⊢ (((𝑓 “ 𝑤) ∈ 𝐾 ∧ (𝑦 ⊆ (𝑓 “ 𝑤) ∧ ((cls‘𝐾)‘(𝑓 “ 𝑤)) ⊆ 𝑥)) → ∃𝑧 ∈ 𝐾 (𝑦 ⊆ 𝑧 ∧ ((cls‘𝐾)‘𝑧) ⊆ 𝑥))
64	25, 42, 58, 63	syl12anc 836	. . . . . . . 8 ⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((^◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (^◡𝑓 “ 𝑥)))) → ∃𝑧 ∈ 𝐾 (𝑦 ⊆ 𝑧 ∧ ((cls‘𝐾)‘𝑧) ⊆ 𝑥))
65	21, 64	rexlimddv 3148	. . . . . . 7 ⊢ (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → ∃𝑧 ∈ 𝐾 (𝑦 ⊆ 𝑧 ∧ ((cls‘𝐾)‘𝑧) ⊆ 𝑥))
66	65	ralrimivva 3188	. . . . . 6 ⊢ ((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) → ∀𝑥 ∈ 𝐾 ∀𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥)∃𝑧 ∈ 𝐾 (𝑦 ⊆ 𝑧 ∧ ((cls‘𝐾)‘𝑧) ⊆ 𝑥))
67		isnrm 23278	. . . . . 6 ⊢ (𝐾 ∈ Nrm ↔ (𝐾 ∈ Top ∧ ∀𝑥 ∈ 𝐾 ∀𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥)∃𝑧 ∈ 𝐾 (𝑦 ⊆ 𝑧 ∧ ((cls‘𝐾)‘𝑧) ⊆ 𝑥)))
68	6, 66, 67	sylanbrc 583	. . . . 5 ⊢ ((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) → 𝐾 ∈ Nrm)
69	68	expcom 413	. . . 4 ⊢ (𝑓 ∈ (𝐽Homeo𝐾) → (𝐽 ∈ Nrm → 𝐾 ∈ Nrm))
70	69	exlimiv 1930	. . 3 ⊢ (∃𝑓 𝑓 ∈ (𝐽Homeo𝐾) → (𝐽 ∈ Nrm → 𝐾 ∈ Nrm))
71	2, 70	sylbi 217	. 2 ⊢ ((𝐽Homeo𝐾) ≠ ∅ → (𝐽 ∈ Nrm → 𝐾 ∈ Nrm))
72	1, 71	sylbi 217	1 ⊢ (𝐽 ≃ 𝐾 → (𝐽 ∈ Nrm → 𝐾 ∈ Nrm))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1540 ∃wex 1779 ∈ wcel 2109 ≠ wne 2933 ∀wral 3052 ∃wrex 3061 ∩ cin 3930 ⊆ wss 3931 ∅c0 4313 𝒫 cpw 4580 ∪ cuni 4888 class class class wbr 5124 ^◡ccnv 5658 dom cdm 5659 ran crn 5660 “ cima 5662 Fun wfun 6530 –onto→wfo 6534 –1-1-onto→wf1o 6535 ‘cfv 6536 (class class class)co 7410 Topctop 22836 Clsdccld 22959 clsccl 22961 Cn ccn 23167 Nrmcnrm 23253 Homeochmeo 23696 ≃ chmph 23697

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2708 ax-rep 5254 ax-sep 5271 ax-nul 5281 ax-pow 5340 ax-pr 5407 ax-un 7734

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2810 df-nfc 2886 df-ne 2934 df-ral 3053 df-rex 3062 df-reu 3365 df-rab 3421 df-v 3466 df-sbc 3771 df-csb 3880 df-dif 3934 df-un 3936 df-in 3938 df-ss 3948 df-nul 4314 df-if 4506 df-pw 4582 df-sn 4607 df-pr 4609 df-op 4613 df-uni 4889 df-int 4928 df-iun 4974 df-iin 4975 df-br 5125 df-opab 5187 df-mpt 5207 df-id 5553 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-suc 6363 df-iota 6489 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-ov 7413 df-oprab 7414 df-mpo 7415 df-1st 7993 df-2nd 7994 df-1o 8485 df-map 8847 df-top 22837 df-topon 22854 df-cld 22962 df-cls 22964 df-cn 23170 df-nrm 23260 df-hmeo 23698 df-hmph 23699

This theorem is referenced by: (None)

W3C validator