Theorem nrmr0reg 19464

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 19082	. . 3 |- ( J e. Nrm -> J e. Top )
2	1	adantr 465	. 2 |- ( ( J e. Nrm /\ (KQ ` J ) e. Fre ) -> J e. Top )
3		simpll 753	. . . . 5 |- ( ( ( J e. Nrm /\ (KQ ` J ) e. Fre ) /\ ( x e. J /\ y e. x ) ) -> J e. Nrm )
4		simprl 755	. . . . 5 |- ( ( ( J e. Nrm /\ (KQ ` J ) e. Fre ) /\ ( x e. J /\ y e. x ) ) -> x e. J )
5	2	adantr 465	. . . . . . 7 |- ( ( ( J e. Nrm /\ (KQ ` J ) e. Fre ) /\ ( x e. J /\ y e. x ) ) -> J e. Top )
6		eqid 2454	. . . . . . . 8 |- U. J = U. J
7	6	toptopon 18680	. . . . . . 7 |- ( J e. Top <-> J e. (TopOn ` U. J ) )
8	5, 7	sylib 196	. . . . . 6 |- ( ( ( J e. Nrm /\ (KQ ` J ) e. Fre ) /\ ( x e. J /\ y e. x ) ) -> J e. (TopOn ` U. J ) )
9		simplr 754	. . . . . 6 |- ( ( ( J e. Nrm /\ (KQ ` J ) e. Fre ) /\ ( x e. J /\ y e. x ) ) -> (KQ ` J ) e. Fre )
10		simprr 756	. . . . . . 7 |- ( ( ( J e. Nrm /\ (KQ ` J ) e. Fre ) /\ ( x e. J /\ y e. x ) ) -> y e. x )
11		elunii 4207	. . . . . . 7 |- ( ( y e. x /\ x e. J ) -> y e. U. J )
12	10, 4, 11	syl2anc 661	. . . . . 6 |- ( ( ( J e. Nrm /\ (KQ ` J ) e. Fre ) /\ ( x e. J /\ y e. x ) ) -> y e. U. J )
13		eqid 2454	. . . . . . 7 |- ( z e. U. J |-> { w e. J | z e. w } ) = ( z e. U. J |-> { w e. J | z e. w } )
14	13	r0cld 19453	. . . . . 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 1219	. . . . 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 1054	. . . . . . 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 465	. . . . . . . . 9 |- ( ( ( ( J e. Nrm /\ (KQ ` J ) e. Fre ) /\ ( x e. J /\ y e. x ) ) /\ a e. U. J ) -> x e. J )
18		elequ2 1763	. . . . . . . . . . 11 |- ( b = x -> ( a e. b <-> a e. x ) )
19		elequ2 1763	. . . . . . . . . . 11 |- ( b = x -> ( y e. b <-> y e. x ) )
20	18, 19	bibi12d 321	. . . . . . . . . 10 |- ( b = x -> ( ( a e. b <-> y e. b ) <-> ( a e. x <-> y e. x ) ) )
21	20	rspcv 3175	. . . . . . . . 9 |- ( x e. J -> ( A. b e. J ( a e. b <-> y e. b ) -> ( a e. x <-> y e. x ) ) )
22	17, 21	syl 16	. . . . . . . 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 1185	. . . . . . 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 232	. . . . . 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 3543	. . . . 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 19101	. . . . 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 1221	. . . 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 237	. . . . . . . . 9 |- ( ( ( J e. Nrm /\ (KQ ` J ) e. Fre ) /\ ( x e. J /\ y e. x ) ) -> ( y e. b <-> y e. b ) )
29	28	ralrimivw 2831	. . . . . . . 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 1761	. . . . . . . . . . 11 |- ( a = y -> ( a e. b <-> y e. b ) )
31	30	bibi1d 319	. . . . . . . . . 10 |- ( a = y -> ( ( a e. b <-> y e. b ) <-> ( y e. b <-> y e. b ) ) )
32	31	ralbidv 2846	. . . . . . . . 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 3224	. . . . . . . 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 664	. . . . . . 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 3461	. . . . . . 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 30	. . . . . 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 564	. . . . 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 2933	. . . 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 2914	. 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 19078	. 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 664	1 |- ( ( J e. Nrm /\ (KQ ` J ) e. Fre ) -> J e. Reg )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   /\ w3a 965   e. wcel 1758   A.wral 2799   E.wrex 2800   {crab 2803   C_ wss 3439   U.cuni 4202   |-> cmpt 4461   ` cfv 5529   Topctop 18640  TopOnctopon 18641   Clsdccld 18762   clsccl 18764   Frect1 19053   Regcreg 19055   Nrmcnrm 19056  KQckq 19408

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-rep 4514  ax-sep 4524  ax-nul 4532  ax-pow 4581  ax-pr 4642  ax-un 6485

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-ral 2804  df-rex 2805  df-reu 2806  df-rab 2808  df-v 3080  df-sbc 3295  df-csb 3399  df-dif 3442  df-un 3444  df-in 3446  df-ss 3453  df-nul 3749  df-if 3903  df-pw 3973  df-sn 3989  df-pr 3991  df-op 3995  df-uni 4203  df-iun 4284  df-br 4404  df-opab 4462  df-mpt 4463  df-id 4747  df-xp 4957  df-rel 4958  df-cnv 4959  df-co 4960  df-dm 4961  df-rn 4962  df-res 4963  df-ima 4964  df-iota 5492  df-fun 5531  df-fn 5532  df-f 5533  df-f1 5534  df-fo 5535  df-f1o 5536  df-fv 5537  df-ov 6206  df-oprab 6207  df-mpt2 6208  df-map 7329  df-qtop 14568  df-top 18645  df-topon 18648  df-cld 18765  df-cn 18973  df-t1 19060  df-reg 19062  df-nrm 19063  df-kq 19409

This theorem is referenced by:  nrmreg  19539