Metamath Proof Explorer

Theorem r0sep

Description: The separation property of an R_0 space. (Contributed by Mario Carneiro, 25-Aug-2015)

Ref Expression
Assertion r0sep 
|- ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre ) /\ ( A e. X /\ B e. X ) ) -> ( A. o e. J ( A e. o -> B e. o ) -> A. o e. J ( A e. o <-> B e. o ) ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( z e. X |-> { w e. J | z e. w } ) = ( z e. X |-> { w e. J | z e. w } )
2 1 isr0 
 |-  ( J e. ( TopOn ` X ) -> ( ( KQ ` J ) e. Fre <-> A. x e. X A. y e. X ( A. o e. J ( x e. o -> y e. o ) -> A. o e. J ( x e. o <-> y e. o ) ) ) )
3 2 biimpa 
 |-  ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre ) -> A. x e. X A. y e. X ( A. o e. J ( x e. o -> y e. o ) -> A. o e. J ( x e. o <-> y e. o ) ) )
4 eleq1 
 |-  ( x = A -> ( x e. o <-> A e. o ) )
5 4 imbi1d 
 |-  ( x = A -> ( ( x e. o -> y e. o ) <-> ( A e. o -> y e. o ) ) )
6 5 ralbidv 
 |-  ( x = A -> ( A. o e. J ( x e. o -> y e. o ) <-> A. o e. J ( A e. o -> y e. o ) ) )
7 4 bibi1d 
 |-  ( x = A -> ( ( x e. o <-> y e. o ) <-> ( A e. o <-> y e. o ) ) )
8 7 ralbidv 
 |-  ( x = A -> ( A. o e. J ( x e. o <-> y e. o ) <-> A. o e. J ( A e. o <-> y e. o ) ) )
9 6 8 imbi12d 
 |-  ( x = A -> ( ( A. o e. J ( x e. o -> y e. o ) -> A. o e. J ( x e. o <-> y e. o ) ) <-> ( A. o e. J ( A e. o -> y e. o ) -> A. o e. J ( A e. o <-> y e. o ) ) ) )
10 eleq1 
 |-  ( y = B -> ( y e. o <-> B e. o ) )
11 10 imbi2d 
 |-  ( y = B -> ( ( A e. o -> y e. o ) <-> ( A e. o -> B e. o ) ) )
12 11 ralbidv 
 |-  ( y = B -> ( A. o e. J ( A e. o -> y e. o ) <-> A. o e. J ( A e. o -> B e. o ) ) )
13 10 bibi2d 
 |-  ( y = B -> ( ( A e. o <-> y e. o ) <-> ( A e. o <-> B e. o ) ) )
14 13 ralbidv 
 |-  ( y = B -> ( A. o e. J ( A e. o <-> y e. o ) <-> A. o e. J ( A e. o <-> B e. o ) ) )
15 12 14 imbi12d 
 |-  ( y = B -> ( ( A. o e. J ( A e. o -> y e. o ) -> A. o e. J ( A e. o <-> y e. o ) ) <-> ( A. o e. J ( A e. o -> B e. o ) -> A. o e. J ( A e. o <-> B e. o ) ) ) )
16 9 15 rspc2v 
 |-  ( ( A e. X /\ B e. X ) -> ( A. x e. X A. y e. X ( A. o e. J ( x e. o -> y e. o ) -> A. o e. J ( x e. o <-> y e. o ) ) -> ( A. o e. J ( A e. o -> B e. o ) -> A. o e. J ( A e. o <-> B e. o ) ) ) )
17 3 16 mpan9 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre ) /\ ( A e. X /\ B e. X ) ) -> ( A. o e. J ( A e. o -> B e. o ) -> A. o e. J ( A e. o <-> B e. o ) ) )