Metamath Proof Explorer

Theorem ustval

Description: The class of all uniform structures for a base X . (Contributed by Thierry Arnoux, 15-Nov-2017) (Revised by AV, 17-Sep-2021)

Ref Expression
Assertion ustval 
|- ( X e. V -> ( UnifOn ` X ) = { 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 ) ) ) } )

Proof

Step Hyp Ref Expression
1 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 ) ) ) } )
2 id 
 |-  ( x = X -> x = X )
3 2 sqxpeqd 
 |-  ( x = X -> ( x X. x ) = ( X X. X ) )
4 3 pweqd 
 |-  ( x = X -> ~P ( x X. x ) = ~P ( X X. X ) )
5 4 sseq2d 
 |-  ( x = X -> ( u C_ ~P ( x X. x ) <-> u C_ ~P ( X X. X ) ) )
6 3 eleq1d 
 |-  ( x = X -> ( ( x X. x ) e. u <-> ( X X. X ) e. u ) )
7 4 raleqdv 
 |-  ( x = X -> ( A. w e. ~P ( x X. x ) ( v C_ w -> w e. u ) <-> A. w e. ~P ( X X. X ) ( v C_ w -> w e. u ) ) )
8 reseq2 
 |-  ( x = X -> ( _I |` x ) = ( _I |` X ) )
9 8 sseq1d 
 |-  ( x = X -> ( ( _I |` x ) C_ v <-> ( _I |` X ) C_ v ) )
10 9 3anbi1d 
 |-  ( x = X -> ( ( ( _I |` x ) C_ v /\ `' v e. u /\ E. w e. u ( w o. w ) C_ v ) <-> ( ( _I |` X ) C_ v /\ `' v e. u /\ E. w e. u ( w o. w ) C_ v ) ) )
11 7 10 3anbi13d 
 |-  ( x = X -> ( ( 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 ) /\ 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 ) ) ) )
12 11 ralbidv 
 |-  ( 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 ) ) <-> 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 ) ) ) )
13 5 6 12 3anbi123d 
 |-  ( 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 ) ) ) <-> ( 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 13 abbidv 
 |-  ( x = X -> { 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 ) ) ) } = { 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 ) ) ) } )
15 elex 
 |-  ( X e. V -> X e. _V )
16 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 ) )
17 16 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 ) }
18 df-pw 
 |-  ~P ~P ( X X. X ) = { u | u C_ ~P ( X X. X ) }
19 17 18 sseqtrri 
 |-  { 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_ ~P ~P ( X X. X )
20 sqxpexg 
 |-  ( X e. V -> ( X X. X ) e. _V )
21 pwexg 
 |-  ( ( X X. X ) e. _V -> ~P ( X X. X ) e. _V )
22 pwexg 
 |-  ( ~P ( X X. X ) e. _V -> ~P ~P ( X X. X ) e. _V )
23 20 21 22 3syl 
 |-  ( X e. V -> ~P ~P ( X X. X ) e. _V )
24 ssexg 
 |-  ( ( { 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_ ~P ~P ( X X. X ) /\ ~P ~P ( X X. 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 ) ) ) } e. _V )
25 19 23 24 sylancr 
 |-  ( 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 ) ) ) } e. _V )
26 1 14 15 25 fvmptd3 
 |-  ( X e. V -> ( UnifOn ` X ) = { 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 ) ) ) } )