Metamath Proof Explorer

Theorem ustn0

Description: The empty set is not an uniform structure. (Contributed by Thierry Arnoux, 3-Dec-2017)

Ref Expression
Assertion ustn0 
|- -. (/) e. U. ran UnifOn

Proof

Step Hyp Ref Expression
1 noel 
 |-  -. ( x X. x ) e. (/)
2 0ex 
 |-  (/) e. _V
3 eleq2 
 |-  ( u = (/) -> ( ( x X. x ) e. u <-> ( x X. x ) e. (/) ) )
4 2 3 elab 
 |-  ( (/) e. { u | ( x X. x ) e. u } <-> ( x X. x ) e. (/) )
5 1 4 mtbir 
 |-  -. (/) e. { u | ( x X. x ) e. u }
6 vex 
 |-  x e. _V
7 velpw 
 |-  ( u e. ~P ~P ( x X. x ) <-> u C_ ~P ( x X. x ) )
8 7 abbii 
 |-  { u | u e. ~P ~P ( x X. x ) } = { u | u C_ ~P ( x X. x ) }
9 abid2 
 |-  { u | u e. ~P ~P ( x X. x ) } = ~P ~P ( x X. x )
10 6 6 xpex 
 |-  ( x X. x ) e. _V
11 10 pwex 
 |-  ~P ( x X. x ) e. _V
12 11 pwex 
 |-  ~P ~P ( x X. x ) e. _V
13 9 12 eqeltri 
 |-  { u | u e. ~P ~P ( x X. x ) } e. _V
14 8 13 eqeltrri 
 |-  { u | u C_ ~P ( x X. x ) } e. _V
15 simp1 
 |-  ( ( u C_ ~P ( x X. x ) /\ ( x X. x ) e. u /\ A. v e. u ( A. w e. ~P ( x X. x ) ( v C_ w -> w e. u ) /\ A. w e. u ( v i^i w ) e. u /\ ( ( _I |` x ) C_ v /\ `' v e. u /\ E. w e. u ( w o. w ) C_ v ) ) ) -> u C_ ~P ( x X. x ) )
16 15 ss2abi 
 |-  { u | ( u C_ ~P ( x X. x ) /\ ( x X. x ) e. u /\ A. v e. u ( A. w e. ~P ( x X. x ) ( v C_ w -> w e. u ) /\ A. w e. u ( v i^i w ) e. u /\ ( ( _I |` x ) C_ v /\ `' v e. u /\ E. w e. u ( w o. w ) C_ v ) ) ) } C_ { u | u C_ ~P ( x X. x ) }
17 14 16 ssexi 
 |-  { u | ( u C_ ~P ( x X. x ) /\ ( x X. x ) e. u /\ A. v e. u ( A. w e. ~P ( x X. x ) ( v C_ w -> w e. u ) /\ A. w e. u ( v i^i w ) e. u /\ ( ( _I |` x ) C_ v /\ `' v e. u /\ E. w e. u ( w o. w ) C_ v ) ) ) } e. _V
18 df-ust 
 |-  UnifOn = ( x e. _V |-> { u | ( u C_ ~P ( x X. x ) /\ ( x X. x ) e. u /\ A. v e. u ( A. w e. ~P ( x X. x ) ( v C_ w -> w e. u ) /\ A. w e. u ( v i^i w ) e. u /\ ( ( _I |` x ) C_ v /\ `' v e. u /\ E. w e. u ( w o. w ) C_ v ) ) ) } )
19 18 fvmpt2 
 |-  ( ( x e. _V /\ { u | ( u C_ ~P ( x X. x ) /\ ( x X. x ) e. u /\ A. v e. u ( A. w e. ~P ( x X. x ) ( v C_ w -> w e. u ) /\ A. w e. u ( v i^i w ) e. u /\ ( ( _I |` x ) C_ v /\ `' v e. u /\ E. w e. u ( w o. w ) C_ v ) ) ) } e. _V ) -> ( UnifOn ` x ) = { u | ( u C_ ~P ( x X. x ) /\ ( x X. x ) e. u /\ A. v e. u ( A. w e. ~P ( x X. x ) ( v C_ w -> w e. u ) /\ A. w e. u ( v i^i w ) e. u /\ ( ( _I |` x ) C_ v /\ `' v e. u /\ E. w e. u ( w o. w ) C_ v ) ) ) } )
20 6 17 19 mp2an 
 |-  ( UnifOn ` x ) = { u | ( u C_ ~P ( x X. x ) /\ ( x X. x ) e. u /\ A. v e. u ( A. w e. ~P ( x X. x ) ( v C_ w -> w e. u ) /\ A. w e. u ( v i^i w ) e. u /\ ( ( _I |` x ) C_ v /\ `' v e. u /\ E. w e. u ( w o. w ) C_ v ) ) ) }
21 simp2 
 |-  ( ( u C_ ~P ( x X. x ) /\ ( x X. x ) e. u /\ A. v e. u ( A. w e. ~P ( x X. x ) ( v C_ w -> w e. u ) /\ A. w e. u ( v i^i w ) e. u /\ ( ( _I |` x ) C_ v /\ `' v e. u /\ E. w e. u ( w o. w ) C_ v ) ) ) -> ( x X. x ) e. u )
22 21 ss2abi 
 |-  { u | ( u C_ ~P ( x X. x ) /\ ( x X. x ) e. u /\ A. v e. u ( A. w e. ~P ( x X. x ) ( v C_ w -> w e. u ) /\ A. w e. u ( v i^i w ) e. u /\ ( ( _I |` x ) C_ v /\ `' v e. u /\ E. w e. u ( w o. w ) C_ v ) ) ) } C_ { u | ( x X. x ) e. u }
23 20 22 eqsstri 
 |-  ( UnifOn ` x ) C_ { u | ( x X. x ) e. u }
24 23 sseli 
 |-  ( (/) e. ( UnifOn ` x ) -> (/) e. { u | ( x X. x ) e. u } )
25 5 24 mto 
 |-  -. (/) e. ( UnifOn ` x )
26 25 nex 
 |-  -. E. x (/) e. ( UnifOn ` x )
27 18 funmpt2 
 |-  Fun UnifOn
28 elunirn 
 |-  ( Fun UnifOn -> ( (/) e. U. ran UnifOn <-> E. x e. dom UnifOn (/) e. ( UnifOn ` x ) ) )
29 27 28 ax-mp 
 |-  ( (/) e. U. ran UnifOn <-> E. x e. dom UnifOn (/) e. ( UnifOn ` x ) )
30 ustfn 
 |-  UnifOn Fn _V
31 fndm 
 |-  ( UnifOn Fn _V -> dom UnifOn = _V )
32 30 31 ax-mp 
 |-  dom UnifOn = _V
33 32 rexeqi 
 |-  ( E. x e. dom UnifOn (/) e. ( UnifOn ` x ) <-> E. x e. _V (/) e. ( UnifOn ` x ) )
34 rexv 
 |-  ( E. x e. _V (/) e. ( UnifOn ` x ) <-> E. x (/) e. ( UnifOn ` x ) )
35 29 33 34 3bitri 
 |-  ( (/) e. U. ran UnifOn <-> E. x (/) e. ( UnifOn ` x ) )
36 26 35 mtbir 
 |-  -. (/) e. U. ran UnifOn