Metamath Proof Explorer

Theorem nrmr0reg

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

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

Proof

Step Hyp Ref Expression
1 nrmtop 
 |-  ( J e. Nrm -> J e. Top )
2 1 adantr 
 |-  ( ( J e. Nrm /\ ( KQ ` J ) e. Fre ) -> J e. Top )
3 simpll 
 |-  ( ( ( J e. Nrm /\ ( KQ ` J ) e. Fre ) /\ ( x e. J /\ y e. x ) ) -> J e. Nrm )
4 simprl 
 |-  ( ( ( J e. Nrm /\ ( KQ ` J ) e. Fre ) /\ ( x e. J /\ y e. x ) ) -> x e. J )
5 2 adantr 
 |-  ( ( ( J e. Nrm /\ ( KQ ` J ) e. Fre ) /\ ( x e. J /\ y e. x ) ) -> J e. Top )
6 toptopon2 
 |-  ( J e. Top <-> J e. ( TopOn ` U. J ) )
7 5 6 sylib 
 |-  ( ( ( J e. Nrm /\ ( KQ ` J ) e. Fre ) /\ ( x e. J /\ y e. x ) ) -> J e. ( TopOn ` U. J ) )
8 simplr 
 |-  ( ( ( J e. Nrm /\ ( KQ ` J ) e. Fre ) /\ ( x e. J /\ y e. x ) ) -> ( KQ ` J ) e. Fre )
9 simprr 
 |-  ( ( ( J e. Nrm /\ ( KQ ` J ) e. Fre ) /\ ( x e. J /\ y e. x ) ) -> y e. x )
10 elunii 
 |-  ( ( y e. x /\ x e. J ) -> y e. U. J )
11 9 4 10 syl2anc 
 |-  ( ( ( J e. Nrm /\ ( KQ ` J ) e. Fre ) /\ ( x e. J /\ y e. x ) ) -> y e. U. J )
12 eqid 
 |-  ( z e. U. J |-> { w e. J | z e. w } ) = ( z e. U. J |-> { w e. J | z e. w } )
13 12 r0cld 
 |-  ( ( 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 ) )
14 7 8 11 13 syl3anc 
 |-  ( ( ( 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 ) )
15 simp1rr 
 |-  ( ( ( ( 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 )
16 4 adantr 
 |-  ( ( ( ( J e. Nrm /\ ( KQ ` J ) e. Fre ) /\ ( x e. J /\ y e. x ) ) /\ a e. U. J ) -> x e. J )
17 elequ2 
 |-  ( b = x -> ( a e. b <-> a e. x ) )
18 elequ2 
 |-  ( b = x -> ( y e. b <-> y e. x ) )
19 17 18 bibi12d 
 |-  ( b = x -> ( ( a e. b <-> y e. b ) <-> ( a e. x <-> y e. x ) ) )
20 19 rspcv 
 |-  ( x e. J -> ( A. b e. J ( a e. b <-> y e. b ) -> ( a e. x <-> y e. x ) ) )
21 16 20 syl 
 |-  ( ( ( ( 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 ) ) )
22 21 3impia 
 |-  ( ( ( ( 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 15 22 mpbird 
 |-  ( ( ( ( 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 )
24 23 rabssdv 
 |-  ( ( ( 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 )
25 nrmsep3 
 |-  ( ( 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 ) )
26 3 4 14 24 25 syl13anc 
 |-  ( ( ( 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 ) )
27 elequ1 
 |-  ( a = y -> ( a e. b <-> y e. b ) )
28 27 bibi1d 
 |-  ( a = y -> ( ( a e. b <-> y e. b ) <-> ( y e. b <-> y e. b ) ) )
29 28 ralbidv 
 |-  ( a = y -> ( A. b e. J ( a e. b <-> y e. b ) <-> A. b e. J ( y e. b <-> y e. b ) ) )
30 biidd 
 |-  ( ( ( J e. Nrm /\ ( KQ ` J ) e. Fre ) /\ ( x e. J /\ y e. x ) ) -> ( y e. b <-> y e. b ) )
31 30 ralrimivw 
 |-  ( ( ( J e. Nrm /\ ( KQ ` J ) e. Fre ) /\ ( x e. J /\ y e. x ) ) -> A. b e. J ( y e. b <-> y e. b ) )
32 29 11 31 elrabd 
 |-  ( ( ( 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 ) } )
33 ssel 
 |-  ( { 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 ) )
34 32 33 syl5com 
 |-  ( ( ( 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 ) )
35 34 anim1d 
 |-  ( ( ( 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 ) ) )
36 35 reximdv 
 |-  ( ( ( 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 ) ) )
37 26 36 mpd 
 |-  ( ( ( 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 ) )
38 37 ralrimivva 
 |-  ( ( 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 ) )
39 isreg 
 |-  ( 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 ) ) )
40 2 38 39 sylanbrc 
 |-  ( ( J e. Nrm /\ ( KQ ` J ) e. Fre ) -> J e. Reg )