Metamath Proof Explorer

Theorem dissnref

Description: The set of singletons is a refinement of any open covering of the discrete topology. (Contributed by Thierry Arnoux, 9-Jan-2020)

Ref Expression
Hypothesis dissnref.c 
|- C = { u | E. x e. X u = { x } }
Assertion dissnref 
|- ( ( X e. V /\ U. Y = X ) -> C Ref Y )

Proof

Step Hyp Ref Expression
1 dissnref.c 
 |-  C = { u | E. x e. X u = { x } }
2 simpr 
 |-  ( ( X e. V /\ U. Y = X ) -> U. Y = X )
3 1 unisngl 
 |-  X = U. C
4 2 3 eqtrdi 
 |-  ( ( X e. V /\ U. Y = X ) -> U. Y = U. C )
5 simplr 
 |-  ( ( ( ( ( ( X e. V /\ U. Y = X ) /\ u e. C ) /\ x e. X ) /\ u = { x } ) /\ ( y e. Y /\ x e. y ) ) -> u = { x } )
6 simprr 
 |-  ( ( ( ( ( ( X e. V /\ U. Y = X ) /\ u e. C ) /\ x e. X ) /\ u = { x } ) /\ ( y e. Y /\ x e. y ) ) -> x e. y )
7 6 snssd 
 |-  ( ( ( ( ( ( X e. V /\ U. Y = X ) /\ u e. C ) /\ x e. X ) /\ u = { x } ) /\ ( y e. Y /\ x e. y ) ) -> { x } C_ y )
8 5 7 eqsstrd 
 |-  ( ( ( ( ( ( X e. V /\ U. Y = X ) /\ u e. C ) /\ x e. X ) /\ u = { x } ) /\ ( y e. Y /\ x e. y ) ) -> u C_ y )
9 simplr 
 |-  ( ( ( ( ( X e. V /\ U. Y = X ) /\ u e. C ) /\ x e. X ) /\ u = { x } ) -> x e. X )
10 simp-4r 
 |-  ( ( ( ( ( X e. V /\ U. Y = X ) /\ u e. C ) /\ x e. X ) /\ u = { x } ) -> U. Y = X )
11 9 10 eleqtrrd 
 |-  ( ( ( ( ( X e. V /\ U. Y = X ) /\ u e. C ) /\ x e. X ) /\ u = { x } ) -> x e. U. Y )
12 eluni2 
 |-  ( x e. U. Y <-> E. y e. Y x e. y )
13 11 12 sylib 
 |-  ( ( ( ( ( X e. V /\ U. Y = X ) /\ u e. C ) /\ x e. X ) /\ u = { x } ) -> E. y e. Y x e. y )
14 8 13 reximddv 
 |-  ( ( ( ( ( X e. V /\ U. Y = X ) /\ u e. C ) /\ x e. X ) /\ u = { x } ) -> E. y e. Y u C_ y )
15 1 abeq2i 
 |-  ( u e. C <-> E. x e. X u = { x } )
16 15 biimpi 
 |-  ( u e. C -> E. x e. X u = { x } )
17 16 adantl 
 |-  ( ( ( X e. V /\ U. Y = X ) /\ u e. C ) -> E. x e. X u = { x } )
18 14 17 r19.29a 
 |-  ( ( ( X e. V /\ U. Y = X ) /\ u e. C ) -> E. y e. Y u C_ y )
19 18 ralrimiva 
 |-  ( ( X e. V /\ U. Y = X ) -> A. u e. C E. y e. Y u C_ y )
20 pwexg 
 |-  ( X e. V -> ~P X e. _V )
21 simpr 
 |-  ( ( ( u e. C /\ x e. X ) /\ u = { x } ) -> u = { x } )
22 snelpwi 
 |-  ( x e. X -> { x } e. ~P X )
23 22 ad2antlr 
 |-  ( ( ( u e. C /\ x e. X ) /\ u = { x } ) -> { x } e. ~P X )
24 21 23 eqeltrd 
 |-  ( ( ( u e. C /\ x e. X ) /\ u = { x } ) -> u e. ~P X )
25 24 16 r19.29a 
 |-  ( u e. C -> u e. ~P X )
26 25 ssriv 
 |-  C C_ ~P X
27 26 a1i 
 |-  ( X e. V -> C C_ ~P X )
28 20 27 ssexd 
 |-  ( X e. V -> C e. _V )
29 28 adantr 
 |-  ( ( X e. V /\ U. Y = X ) -> C e. _V )
30 eqid 
 |-  U. C = U. C
31 eqid 
 |-  U. Y = U. Y
32 30 31 isref 
 |-  ( C e. _V -> ( C Ref Y <-> ( U. Y = U. C /\ A. u e. C E. y e. Y u C_ y ) ) )
33 29 32 syl 
 |-  ( ( X e. V /\ U. Y = X ) -> ( C Ref Y <-> ( U. Y = U. C /\ A. u e. C E. y e. Y u C_ y ) ) )
34 4 19 33 mpbir2and 
 |-  ( ( X e. V /\ U. Y = X ) -> C Ref Y )