This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ustssel

Description: A uniform structure is upward closed. Condition F_I of BourbakiTop1 p. I.36. (Contributed by Thierry Arnoux, 19-Nov-2017) (Proof shortened by AV, 17-Sep-2021)

Ref Expression
Assertion ustssel 
|- ( ( U e. ( UnifOn ` X ) /\ V e. U /\ W C_ ( X X. X ) ) -> ( V C_ W -> W e. U ) )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. U /\ W C_ ( X X. X ) ) -> U e. ( UnifOn ` X ) )
2 1 elfvexd 
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. U /\ W C_ ( X X. X ) ) -> X e. _V )
3 isust 
 |-  ( X e. _V -> ( U e. ( UnifOn ` X ) <-> ( 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 ) ) ) ) )
4 2 3 syl 
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. U /\ W C_ ( X X. X ) ) -> ( U e. ( UnifOn ` X ) <-> ( 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 ) ) ) ) )
5 1 4 mpbid 
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. U /\ W C_ ( X X. X ) ) -> ( 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 ) ) ) )
6 5 simp3d 
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. U /\ W C_ ( X X. X ) ) -> 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 ) ) )
7 simp1 
 |-  ( ( 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 ) ) -> A. w e. ~P ( X X. X ) ( v C_ w -> w e. U ) )
8 7 ralimi 
 |-  ( 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 ) ) -> A. v e. U A. w e. ~P ( X X. X ) ( v C_ w -> w e. U ) )
9 6 8 syl 
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. U /\ W C_ ( X X. X ) ) -> A. v e. U A. w e. ~P ( X X. X ) ( v C_ w -> w e. U ) )
10 simp2 
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. U /\ W C_ ( X X. X ) ) -> V e. U )
11 2 2 xpexd 
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. U /\ W C_ ( X X. X ) ) -> ( X X. X ) e. _V )
12 simp3 
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. U /\ W C_ ( X X. X ) ) -> W C_ ( X X. X ) )
13 11 12 sselpwd 
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. U /\ W C_ ( X X. X ) ) -> W e. ~P ( X X. X ) )
14 sseq1 
 |-  ( v = V -> ( v C_ w <-> V C_ w ) )
15 14 imbi1d 
 |-  ( v = V -> ( ( v C_ w -> w e. U ) <-> ( V C_ w -> w e. U ) ) )
16 sseq2 
 |-  ( w = W -> ( V C_ w <-> V C_ W ) )
17 eleq1 
 |-  ( w = W -> ( w e. U <-> W e. U ) )
18 16 17 imbi12d 
 |-  ( w = W -> ( ( V C_ w -> w e. U ) <-> ( V C_ W -> W e. U ) ) )
19 15 18 rspc2v 
 |-  ( ( V e. U /\ W e. ~P ( X X. X ) ) -> ( A. v e. U A. w e. ~P ( X X. X ) ( v C_ w -> w e. U ) -> ( V C_ W -> W e. U ) ) )
20 10 13 19 syl2anc 
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. U /\ W C_ ( X X. X ) ) -> ( A. v e. U A. w e. ~P ( X X. X ) ( v C_ w -> w e. U ) -> ( V C_ W -> W e. U ) ) )
21 9 20 mpd 
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. U /\ W C_ ( X X. X ) ) -> ( V C_ W -> W e. U ) )