Metamath Proof Explorer

Theorem ustex3sym

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

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

Proof

Step Hyp Ref Expression
1 ustex2sym 
 |-  ( ( U e. ( UnifOn ` X ) /\ v e. U ) -> E. w e. U ( `' w = w /\ ( w o. 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 o. 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 o. w ) C_ v ) ) -> `' w = w )
4 simp-5l 
 |-  ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ V e. U ) /\ v e. U ) /\ ( v o. v ) C_ V ) /\ w e. U ) /\ ( `' w = w /\ ( w o. w ) C_ v ) ) -> U e. ( UnifOn ` X ) )
5 simplr 
 |-  ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ V e. U ) /\ v e. U ) /\ ( v o. v ) C_ V ) /\ w e. U ) /\ ( `' w = w /\ ( w o. w ) C_ v ) ) -> w e. U )
6 ustssco 
 |-  ( ( U e. ( UnifOn ` X ) /\ w e. U ) -> w C_ ( w o. w ) )
7 4 5 6 syl2anc 
 |-  ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ V e. U ) /\ v e. U ) /\ ( v o. v ) C_ V ) /\ w e. U ) /\ ( `' w = w /\ ( w o. w ) C_ v ) ) -> w C_ ( w o. w ) )
8 simprr 
 |-  ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ V e. U ) /\ v e. U ) /\ ( v o. v ) C_ V ) /\ w e. U ) /\ ( `' w = w /\ ( w o. w ) C_ v ) ) -> ( w o. w ) C_ v )
9 coss2 
 |-  ( ( w o. w ) C_ v -> ( w o. ( w o. w ) ) C_ ( w o. v ) )
10 9 adantl 
 |-  ( ( w C_ ( w o. w ) /\ ( w o. w ) C_ v ) -> ( w o. ( w o. w ) ) C_ ( w o. v ) )
11 sstr 
 |-  ( ( w C_ ( w o. w ) /\ ( w o. w ) C_ v ) -> w C_ v )
12 coss1 
 |-  ( w C_ v -> ( w o. v ) C_ ( v o. v ) )
13 11 12 syl 
 |-  ( ( w C_ ( w o. w ) /\ ( w o. w ) C_ v ) -> ( w o. v ) C_ ( v o. v ) )
14 10 13 sstrd 
 |-  ( ( w C_ ( w o. w ) /\ ( w o. w ) C_ v ) -> ( w o. ( w o. w ) ) C_ ( v o. v ) )
15 7 8 14 syl2anc 
 |-  ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ V e. U ) /\ v e. U ) /\ ( v o. v ) C_ V ) /\ w e. U ) /\ ( `' w = w /\ ( w o. w ) C_ v ) ) -> ( w o. ( w o. w ) ) C_ ( v o. v ) )
16 simpllr 
 |-  ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ V e. U ) /\ v e. U ) /\ ( v o. v ) C_ V ) /\ w e. U ) /\ ( `' w = w /\ ( w o. w ) C_ v ) ) -> ( v o. v ) C_ V )
17 15 16 sstrd 
 |-  ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ V e. U ) /\ v e. U ) /\ ( v o. v ) C_ V ) /\ w e. U ) /\ ( `' w = w /\ ( w o. w ) C_ v ) ) -> ( w o. ( w o. w ) ) C_ V )
18 3 17 jca 
 |-  ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ V e. U ) /\ v e. U ) /\ ( v o. v ) C_ V ) /\ w e. U ) /\ ( `' w = w /\ ( w o. w ) C_ v ) ) -> ( `' w = w /\ ( w o. ( w o. w ) ) C_ V ) )
19 18 ex 
 |-  ( ( ( ( ( U e. ( UnifOn ` X ) /\ V e. U ) /\ v e. U ) /\ ( v o. v ) C_ V ) /\ w e. U ) -> ( ( `' w = w /\ ( w o. w ) C_ v ) -> ( `' w = w /\ ( w o. ( w o. w ) ) C_ V ) ) )
20 19 reximdva 
 |-  ( ( ( ( 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 ) -> E. w e. U ( `' w = w /\ ( w o. ( w o. w ) ) C_ V ) ) )
21 2 20 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 o. w ) ) C_ V ) )
22 ustexhalf 
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. U ) -> E. v e. U ( v o. v ) C_ V )
23 21 22 r19.29a 
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. U ) -> E. w e. U ( `' w = w /\ ( w o. ( w o. w ) ) C_ V ) )