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

Metamath Proof Explorer

Theorem ustfn

Description: The defined uniform structure as a function. (Contributed by Thierry Arnoux, 15-Nov-2017)

Ref Expression
Assertion ustfn 
|- UnifOn Fn _V

Proof

Step Hyp Ref Expression
1 velpw 
 |-  ( u e. ~P ~P ( x X. x ) <-> u C_ ~P ( x X. x ) )
2 1 abbii 
 |-  { u | u e. ~P ~P ( x X. x ) } = { u | u C_ ~P ( x X. x ) }
3 abid2 
 |-  { u | u e. ~P ~P ( x X. x ) } = ~P ~P ( x X. x )
4 vex 
 |-  x e. _V
5 4 4 xpex 
 |-  ( x X. x ) e. _V
6 5 pwex 
 |-  ~P ( x X. x ) e. _V
7 6 pwex 
 |-  ~P ~P ( x X. x ) e. _V
8 3 7 eqeltri 
 |-  { u | u e. ~P ~P ( x X. x ) } e. _V
9 2 8 eqeltrri 
 |-  { u | u C_ ~P ( x X. x ) } e. _V
10 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 ) )
11 10 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 ) }
12 9 11 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
13 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 ) ) ) } )
14 12 13 fnmpti 
 |-  UnifOn Fn _V