Theorem nrmr0reg 20813

Description: A normal R₀ space is also regular. These spaces are usually referred to as normal regular spaces. (Contributed by Mario Carneiro, 25-Aug-2015.)

Assertion

Ref	Expression
nrmr0reg	|- ( ( J e. Nrm /\ (KQ ` J ) e. Fre ) -> J e. Reg )

Proof of Theorem nrmr0reg

Dummy variables x y a b w z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nrmtop 20401	. . 3 |- ( J e. Nrm -> J e. Top )
2	1	adantr 471	. 2 |- ( ( J e. Nrm /\ (KQ ` J ) e. Fre ) -> J e. Top )
3		simpll 765	. . . . 5 |- ( ( ( J e. Nrm /\ (KQ ` J ) e. Fre ) /\ ( x e. J /\ y e. x ) ) -> J e. Nrm )
4		simprl 769	. . . . 5 |- ( ( ( J e. Nrm /\ (KQ ` J ) e. Fre ) /\ ( x e. J /\ y e. x ) ) -> x e. J )
5	2	adantr 471	. . . . . . 7 |- ( ( ( J e. Nrm /\ (KQ ` J ) e. Fre ) /\ ( x e. J /\ y e. x ) ) -> J e. Top )
6		eqid 2462	. . . . . . . 8 |- U. J = U. J
7	6	toptopon 19997	. . . . . . 7 |- ( J e. Top <-> J e. (TopOn ` U. J ) )
8	5, 7	sylib 201	. . . . . 6 |- ( ( ( J e. Nrm /\ (KQ ` J ) e. Fre ) /\ ( x e. J /\ y e. x ) ) -> J e. (TopOn ` U. J ) )
9		simplr 767	. . . . . 6 |- ( ( ( J e. Nrm /\ (KQ ` J ) e. Fre ) /\ ( x e. J /\ y e. x ) ) -> (KQ ` J ) e. Fre )
10		simprr 771	. . . . . . 7 |- ( ( ( J e. Nrm /\ (KQ ` J ) e. Fre ) /\ ( x e. J /\ y e. x ) ) -> y e. x )
11		elunii 4217	. . . . . . 7 |- ( ( y e. x /\ x e. J ) -> y e. U. J )
12	10, 4, 11	syl2anc 671	. . . . . 6 |- ( ( ( J e. Nrm /\ (KQ ` J ) e. Fre ) /\ ( x e. J /\ y e. x ) ) -> y e. U. J )
13		eqid 2462	. . . . . . 7 |- ( z e. U. J |-> { w e. J | z e. w } ) = ( z e. U. J |-> { w e. J | z e. w } )
14	13	r0cld 20802	. . . . . 6 |- ( ( J e. (TopOn ` U. J ) /\ (KQ ` J ) e. Fre /\ y e. U. J ) -> { a e. U. J | A. b e. J ( a e. b <-> y e. b ) } e. ( Clsd ` J ) )
15	8, 9, 12, 14	syl3anc 1276	. . . . 5 |- ( ( ( J e. Nrm /\ (KQ ` J ) e. Fre ) /\ ( x e. J /\ y e. x ) ) -> { a e. U. J | A. b e. J ( a e. b <-> y e. b ) } e. ( Clsd ` J ) )
16		simp1rr 1080	. . . . . . 7 |- ( ( ( ( J e. Nrm /\ (KQ ` J ) e. Fre ) /\ ( x e. J /\ y e. x ) ) /\ a e. U. J /\ A. b e. J ( a e. b <-> y e. b ) ) -> y e. x )
17	4	adantr 471	. . . . . . . . 9 |- ( ( ( ( J e. Nrm /\ (KQ ` J ) e. Fre ) /\ ( x e. J /\ y e. x ) ) /\ a e. U. J ) -> x e. J )
18		elequ2 1912	. . . . . . . . . . 11 |- ( b = x -> ( a e. b <-> a e. x ) )
19		elequ2 1912	. . . . . . . . . . 11 |- ( b = x -> ( y e. b <-> y e. x ) )
20	18, 19	bibi12d 327	. . . . . . . . . 10 |- ( b = x -> ( ( a e. b <-> y e. b ) <-> ( a e. x <-> y e. x ) ) )
21	20	rspcv 3158	. . . . . . . . 9 |- ( x e. J -> ( A. b e. J ( a e. b <-> y e. b ) -> ( a e. x <-> y e. x ) ) )
22	17, 21	syl 17	. . . . . . . 8 |- ( ( ( ( J e. Nrm /\ (KQ ` J ) e. Fre ) /\ ( x e. J /\ y e. x ) ) /\ a e. U. J ) -> ( A. b e. J ( a e. b <-> y e. b ) -> ( a e. x <-> y e. x ) ) )
23	22	3impia 1212	. . . . . . 7 |- ( ( ( ( J e. Nrm /\ (KQ ` J ) e. Fre ) /\ ( x e. J /\ y e. x ) ) /\ a e. U. J /\ A. b e. J ( a e. b <-> y e. b ) ) -> ( a e. x <-> y e. x ) )
24	16, 23	mpbird 240	. . . . . 6 |- ( ( ( ( J e. Nrm /\ (KQ ` J ) e. Fre ) /\ ( x e. J /\ y e. x ) ) /\ a e. U. J /\ A. b e. J ( a e. b <-> y e. b ) ) -> a e. x )
25	24	rabssdv 3521	. . . . 5 |- ( ( ( J e. Nrm /\ (KQ ` J ) e. Fre ) /\ ( x e. J /\ y e. x ) ) -> { a e. U. J | A. b e. J ( a e. b <-> y e. b ) } C_ x )
26		nrmsep3 20420	. . . . 5 |- ( ( J e. Nrm /\ ( x e. J /\ { a e. U. J | A. b e. J ( a e. b <-> y e. b ) } e. ( Clsd ` J ) /\ { a e. U. J | A. b e. J ( a e. b <-> y e. b ) } C_ x ) ) -> E. z e. J ( { a e. U. J | A. b e. J ( a e. b <-> y e. b ) } C_ z /\ ( ( cls ` J ) ` z ) C_ x ) )
27	3, 4, 15, 25, 26	syl13anc 1278	. . . 4 |- ( ( ( J e. Nrm /\ (KQ ` J ) e. Fre ) /\ ( x e. J /\ y e. x ) ) -> E. z e. J ( { a e. U. J | A. b e. J ( a e. b <-> y e. b ) } C_ z /\ ( ( cls ` J ) ` z ) C_ x ) )
28		biidd 245	. . . . . . . . 9 |- ( ( ( J e. Nrm /\ (KQ ` J ) e. Fre ) /\ ( x e. J /\ y e. x ) ) -> ( y e. b <-> y e. b ) )
29	28	ralrimivw 2815	. . . . . . . 8 |- ( ( ( J e. Nrm /\ (KQ ` J ) e. Fre ) /\ ( x e. J /\ y e. x ) ) -> A. b e. J ( y e. b <-> y e. b ) )
30		elequ1 1905	. . . . . . . . . . 11 |- ( a = y -> ( a e. b <-> y e. b ) )
31	30	bibi1d 325	. . . . . . . . . 10 |- ( a = y -> ( ( a e. b <-> y e. b ) <-> ( y e. b <-> y e. b ) ) )
32	31	ralbidv 2839	. . . . . . . . 9 |- ( a = y -> ( A. b e. J ( a e. b <-> y e. b ) <-> A. b e. J ( y e. b <-> y e. b ) ) )
33	32	elrab 3208	. . . . . . . 8 |- ( y e. { a e. U. J | A. b e. J ( a e. b <-> y e. b ) } <-> ( y e. U. J /\ A. b e. J ( y e. b <-> y e. b ) ) )
34	12, 29, 33	sylanbrc 675	. . . . . . 7 |- ( ( ( J e. Nrm /\ (KQ ` J ) e. Fre ) /\ ( x e. J /\ y e. x ) ) -> y e. { a e. U. J | A. b e. J ( a e. b <-> y e. b ) } )
35		ssel 3438	. . . . . . 7 |- ( { a e. U. J | A. b e. J ( a e. b <-> y e. b ) } C_ z -> ( y e. { a e. U. J | A. b e. J ( a e. b <-> y e. b ) } -> y e. z ) )
36	34, 35	syl5com 31	. . . . . 6 |- ( ( ( J e. Nrm /\ (KQ ` J ) e. Fre ) /\ ( x e. J /\ y e. x ) ) -> ( { a e. U. J | A. b e. J ( a e. b <-> y e. b ) } C_ z -> y e. z ) )
37	36	anim1d 572	. . . . 5 |- ( ( ( J e. Nrm /\ (KQ ` J ) e. Fre ) /\ ( x e. J /\ y e. x ) ) -> ( ( { a e. U. J | A. b e. J ( a e. b <-> y e. b ) } C_ z /\ ( ( cls ` J ) ` z ) C_ x ) -> ( y e. z /\ ( ( cls ` J ) ` z ) C_ x ) ) )
38	37	reximdv 2873	. . . 4 |- ( ( ( J e. Nrm /\ (KQ ` J ) e. Fre ) /\ ( x e. J /\ y e. x ) ) -> ( E. z e. J ( { a e. U. J | A. b e. J ( a e. b <-> y e. b ) } C_ z /\ ( ( cls ` J ) ` z ) C_ x ) -> E. z e. J ( y e. z /\ ( ( cls ` J ) ` z ) C_ x ) ) )
39	27, 38	mpd 15	. . 3 |- ( ( ( J e. Nrm /\ (KQ ` J ) e. Fre ) /\ ( x e. J /\ y e. x ) ) -> E. z e. J ( y e. z /\ ( ( cls ` J ) ` z ) C_ x ) )
40	39	ralrimivva 2821	. 2 |- ( ( J e. Nrm /\ (KQ ` J ) e. Fre ) -> A. x e. J A. y e. x E. z e. J ( y e. z /\ ( ( cls ` J ) ` z ) C_ x ) )
41		isreg 20397	. 2 |- ( J e. Reg <-> ( J e. Top /\ A. x e. J A. y e. x E. z e. J ( y e. z /\ ( ( cls ` J ) ` z ) C_ x ) ) )
42	2, 40, 41	sylanbrc 675	1 |- ( ( J e. Nrm /\ (KQ ` J ) e. Fre ) -> J e. Reg )

Syntax hints:   -> wi 4   <-> wb 189   /\ wa 375   /\ w3a 991   e. wcel 1898   A.wral 2749   E.wrex 2750   {crab 2753   C_ wss 3416   U.cuni 4212   |-> cmpt 4475   ` cfv 5601   Topctop 19966  TopOnctopon 19967   Clsdccld 20080   clsccl 20082   Frect1 20372   Regcreg 20374   Nrmcnrm 20375  KQckq 20757

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-rep 4529  ax-sep 4539  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6610

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-reu 2756  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-iun 4294  df-br 4417  df-opab 4476  df-mpt 4477  df-id 4768  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-ov 6318  df-oprab 6319  df-mpt2 6320  df-map 7500  df-qtop 15455  df-top 19970  df-topon 19972  df-cld 20083  df-cn 20292  df-t1 20379  df-reg 20381  df-nrm 20382  df-kq 20758

This theorem is referenced by:  nrmreg  20888