Metamath Proof Explorer

Theorem ntreq0

Description: Two ways to say that a subset has an empty interior. (Contributed by NM, 3-Oct-2007) (Revised by Mario Carneiro, 11-Nov-2013)

Ref Expression
Hypothesis clscld.1 
|- X = U. J
Assertion ntreq0 
|- ( ( J e. Top /\ S C_ X ) -> ( ( ( int ` J ) ` S ) = (/) <-> A. x e. J ( x C_ S -> x = (/) ) ) )

Proof

Step Hyp Ref Expression
1 clscld.1 
 |-  X = U. J
2 1 ntrval 
 |-  ( ( J e. Top /\ S C_ X ) -> ( ( int ` J ) ` S ) = U. ( J i^i ~P S ) )
3 2 eqeq1d 
 |-  ( ( J e. Top /\ S C_ X ) -> ( ( ( int ` J ) ` S ) = (/) <-> U. ( J i^i ~P S ) = (/) ) )
4 neq0 
 |-  ( -. U. ( J i^i ~P S ) = (/) <-> E. y y e. U. ( J i^i ~P S ) )
5 4 con1bii 
 |-  ( -. E. y y e. U. ( J i^i ~P S ) <-> U. ( J i^i ~P S ) = (/) )
6 ancom 
 |-  ( ( y e. x /\ x e. ( J i^i ~P S ) ) <-> ( x e. ( J i^i ~P S ) /\ y e. x ) )
7 elin 
 |-  ( x e. ( J i^i ~P S ) <-> ( x e. J /\ x e. ~P S ) )
8 7 anbi1i 
 |-  ( ( x e. ( J i^i ~P S ) /\ y e. x ) <-> ( ( x e. J /\ x e. ~P S ) /\ y e. x ) )
9 anass 
 |-  ( ( ( x e. J /\ x e. ~P S ) /\ y e. x ) <-> ( x e. J /\ ( x e. ~P S /\ y e. x ) ) )
10 6 8 9 3bitri 
 |-  ( ( y e. x /\ x e. ( J i^i ~P S ) ) <-> ( x e. J /\ ( x e. ~P S /\ y e. x ) ) )
11 10 exbii 
 |-  ( E. x ( y e. x /\ x e. ( J i^i ~P S ) ) <-> E. x ( x e. J /\ ( x e. ~P S /\ y e. x ) ) )
12 eluni 
 |-  ( y e. U. ( J i^i ~P S ) <-> E. x ( y e. x /\ x e. ( J i^i ~P S ) ) )
13 df-rex 
 |-  ( E. x e. J ( x e. ~P S /\ y e. x ) <-> E. x ( x e. J /\ ( x e. ~P S /\ y e. x ) ) )
14 11 12 13 3bitr4i 
 |-  ( y e. U. ( J i^i ~P S ) <-> E. x e. J ( x e. ~P S /\ y e. x ) )
15 14 exbii 
 |-  ( E. y y e. U. ( J i^i ~P S ) <-> E. y E. x e. J ( x e. ~P S /\ y e. x ) )
16 rexcom4 
 |-  ( E. x e. J E. y ( x e. ~P S /\ y e. x ) <-> E. y E. x e. J ( x e. ~P S /\ y e. x ) )
17 19.42v 
 |-  ( E. y ( x e. ~P S /\ y e. x ) <-> ( x e. ~P S /\ E. y y e. x ) )
18 17 rexbii 
 |-  ( E. x e. J E. y ( x e. ~P S /\ y e. x ) <-> E. x e. J ( x e. ~P S /\ E. y y e. x ) )
19 15 16 18 3bitr2i 
 |-  ( E. y y e. U. ( J i^i ~P S ) <-> E. x e. J ( x e. ~P S /\ E. y y e. x ) )
20 19 notbii 
 |-  ( -. E. y y e. U. ( J i^i ~P S ) <-> -. E. x e. J ( x e. ~P S /\ E. y y e. x ) )
21 5 20 bitr3i 
 |-  ( U. ( J i^i ~P S ) = (/) <-> -. E. x e. J ( x e. ~P S /\ E. y y e. x ) )
22 ralinexa 
 |-  ( A. x e. J ( x e. ~P S -> -. E. y y e. x ) <-> -. E. x e. J ( x e. ~P S /\ E. y y e. x ) )
23 velpw 
 |-  ( x e. ~P S <-> x C_ S )
24 neq0 
 |-  ( -. x = (/) <-> E. y y e. x )
25 24 con1bii 
 |-  ( -. E. y y e. x <-> x = (/) )
26 23 25 imbi12i 
 |-  ( ( x e. ~P S -> -. E. y y e. x ) <-> ( x C_ S -> x = (/) ) )
27 26 ralbii 
 |-  ( A. x e. J ( x e. ~P S -> -. E. y y e. x ) <-> A. x e. J ( x C_ S -> x = (/) ) )
28 21 22 27 3bitr2i 
 |-  ( U. ( J i^i ~P S ) = (/) <-> A. x e. J ( x C_ S -> x = (/) ) )
29 3 28 bitrdi 
 |-  ( ( J e. Top /\ S C_ X ) -> ( ( ( int ` J ) ` S ) = (/) <-> A. x e. J ( x C_ S -> x = (/) ) ) )