Metamath Proof Explorer

Theorem ustexsym

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

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

Proof

Step Hyp Ref Expression
1 simplll 
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ V e. U ) /\ x e. U ) /\ ( x o. x ) C_ V ) -> U e. ( UnifOn ` X ) )
2 ustinvel 
 |-  ( ( U e. ( UnifOn ` X ) /\ x e. U ) -> `' x e. U )
3 2 ad4ant13 
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ V e. U ) /\ x e. U ) /\ ( x o. x ) C_ V ) -> `' x e. U )
4 simplr 
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ V e. U ) /\ x e. U ) /\ ( x o. x ) C_ V ) -> x e. U )
5 ustincl 
 |-  ( ( U e. ( UnifOn ` X ) /\ `' x e. U /\ x e. U ) -> ( `' x i^i x ) e. U )
6 1 3 4 5 syl3anc 
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ V e. U ) /\ x e. U ) /\ ( x o. x ) C_ V ) -> ( `' x i^i x ) e. U )
7 ustrel 
 |-  ( ( U e. ( UnifOn ` X ) /\ x e. U ) -> Rel x )
8 dfrel2 
 |-  ( Rel x <-> `' `' x = x )
9 7 8 sylib 
 |-  ( ( U e. ( UnifOn ` X ) /\ x e. U ) -> `' `' x = x )
10 9 ineq1d 
 |-  ( ( U e. ( UnifOn ` X ) /\ x e. U ) -> ( `' `' x i^i `' x ) = ( x i^i `' x ) )
11 cnvin 
 |-  `' ( `' x i^i x ) = ( `' `' x i^i `' x )
12 incom 
 |-  ( `' x i^i x ) = ( x i^i `' x )
13 10 11 12 3eqtr4g 
 |-  ( ( U e. ( UnifOn ` X ) /\ x e. U ) -> `' ( `' x i^i x ) = ( `' x i^i x ) )
14 13 ad4ant13 
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ V e. U ) /\ x e. U ) /\ ( x o. x ) C_ V ) -> `' ( `' x i^i x ) = ( `' x i^i x ) )
15 inss2 
 |-  ( `' x i^i x ) C_ x
16 ustssco 
 |-  ( ( U e. ( UnifOn ` X ) /\ x e. U ) -> x C_ ( x o. x ) )
17 16 ad4ant13 
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ V e. U ) /\ x e. U ) /\ ( x o. x ) C_ V ) -> x C_ ( x o. x ) )
18 simpr 
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ V e. U ) /\ x e. U ) /\ ( x o. x ) C_ V ) -> ( x o. x ) C_ V )
19 17 18 sstrd 
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ V e. U ) /\ x e. U ) /\ ( x o. x ) C_ V ) -> x C_ V )
20 15 19 sstrid 
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ V e. U ) /\ x e. U ) /\ ( x o. x ) C_ V ) -> ( `' x i^i x ) C_ V )
21 cnveq 
 |-  ( w = ( `' x i^i x ) -> `' w = `' ( `' x i^i x ) )
22 id 
 |-  ( w = ( `' x i^i x ) -> w = ( `' x i^i x ) )
23 21 22 eqeq12d 
 |-  ( w = ( `' x i^i x ) -> ( `' w = w <-> `' ( `' x i^i x ) = ( `' x i^i x ) ) )
24 sseq1 
 |-  ( w = ( `' x i^i x ) -> ( w C_ V <-> ( `' x i^i x ) C_ V ) )
25 23 24 anbi12d 
 |-  ( w = ( `' x i^i x ) -> ( ( `' w = w /\ w C_ V ) <-> ( `' ( `' x i^i x ) = ( `' x i^i x ) /\ ( `' x i^i x ) C_ V ) ) )
26 25 rspcev 
 |-  ( ( ( `' x i^i x ) e. U /\ ( `' ( `' x i^i x ) = ( `' x i^i x ) /\ ( `' x i^i x ) C_ V ) ) -> E. w e. U ( `' w = w /\ w C_ V ) )
27 6 14 20 26 syl12anc 
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ V e. U ) /\ x e. U ) /\ ( x o. x ) C_ V ) -> E. w e. U ( `' w = w /\ w C_ V ) )
28 ustexhalf 
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. U ) -> E. x e. U ( x o. x ) C_ V )
29 27 28 r19.29a 
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. U ) -> E. w e. U ( `' w = w /\ w C_ V ) )