Metamath Proof Explorer

Theorem ustex2sym

Description: In an uniform structure, for any entourage V , there exists a symmetrical entourage smaller than half V . (Contributed by Thierry Arnoux, 16-Jan-2018)

Ref Expression
Assertion ustex2sym 
|- ( ( U e. ( UnifOn ` X ) /\ V e. U ) -> E. w e. U ( `' w = w /\ ( w o. w ) C_ V ) )

Proof

Step Hyp Ref Expression
1 ustexsym 
 |-  ( ( U e. ( UnifOn ` X ) /\ v e. U ) -> E. w e. U ( `' w = w /\ w C_ v ) )
2 1 ad4ant13 
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ V e. U ) /\ v e. U ) /\ ( v o. v ) C_ V ) -> E. w e. U ( `' w = w /\ w C_ v ) )
3 simprl 
 |-  ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ V e. U ) /\ v e. U ) /\ ( v o. v ) C_ V ) /\ w e. U ) /\ ( `' w = w /\ w C_ v ) ) -> `' w = w )
4 coss1 
 |-  ( w C_ v -> ( w o. w ) C_ ( v o. w ) )
5 coss2 
 |-  ( w C_ v -> ( v o. w ) C_ ( v o. v ) )
6 4 5 sstrd 
 |-  ( w C_ v -> ( w o. w ) C_ ( v o. v ) )
7 6 ad2antll 
 |-  ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ V e. U ) /\ v e. U ) /\ ( v o. v ) C_ V ) /\ w e. U ) /\ ( `' w = w /\ w C_ v ) ) -> ( w o. w ) C_ ( v o. v ) )
8 simpllr 
 |-  ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ V e. U ) /\ v e. U ) /\ ( v o. v ) C_ V ) /\ w e. U ) /\ ( `' w = w /\ w C_ v ) ) -> ( v o. v ) C_ V )
9 7 8 sstrd 
 |-  ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ V e. U ) /\ v e. U ) /\ ( v o. v ) C_ V ) /\ w e. U ) /\ ( `' w = w /\ w C_ v ) ) -> ( w o. w ) C_ V )
10 3 9 jca 
 |-  ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ V e. U ) /\ v e. U ) /\ ( v o. v ) C_ V ) /\ w e. U ) /\ ( `' w = w /\ w C_ v ) ) -> ( `' w = w /\ ( w o. w ) C_ V ) )
11 10 ex 
 |-  ( ( ( ( ( U e. ( UnifOn ` X ) /\ V e. U ) /\ v e. U ) /\ ( v o. v ) C_ V ) /\ w e. U ) -> ( ( `' w = w /\ w C_ v ) -> ( `' w = w /\ ( w o. w ) C_ V ) ) )
12 11 reximdva 
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ V e. U ) /\ v e. U ) /\ ( v o. v ) C_ V ) -> ( E. w e. U ( `' w = w /\ w C_ v ) -> E. w e. U ( `' w = w /\ ( w o. w ) C_ V ) ) )
13 2 12 mpd 
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ V e. U ) /\ v e. U ) /\ ( v o. v ) C_ V ) -> E. w e. U ( `' w = w /\ ( w o. w ) C_ V ) )
14 ustexhalf 
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. U ) -> E. v e. U ( v o. v ) C_ V )
15 13 14 r19.29a 
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. U ) -> E. w e. U ( `' w = w /\ ( w o. w ) C_ V ) )