Metamath Proof Explorer

Theorem isust

Description: The predicate " U is a uniform structure with base X ". (Contributed by Thierry Arnoux, 15-Nov-2017) (Revised by AV, 17-Sep-2021)

Ref Expression
Assertion 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 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 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 ) ) ) } )
2 1 eleq2d 
 |-  ( X e. V -> ( U e. ( UnifOn ` X ) <-> U e. { 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 ) ) ) } ) )
3 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 ) )
4 sqxpexg 
 |-  ( X e. V -> ( X X. X ) e. _V )
5 4 pwexd 
 |-  ( X e. V -> ~P ( X X. X ) e. _V )
6 5 adantr 
 |-  ( ( X e. V /\ U C_ ~P ( X X. X ) ) -> ~P ( X X. X ) e. _V )
7 simpr 
 |-  ( ( X e. V /\ U C_ ~P ( X X. X ) ) -> U C_ ~P ( X X. X ) )
8 6 7 ssexd 
 |-  ( ( X e. V /\ U C_ ~P ( X X. X ) ) -> U e. _V )
9 8 ex 
 |-  ( X e. V -> ( U C_ ~P ( X X. X ) -> U e. _V ) )
10 3 9 syl5 
 |-  ( X e. 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 ) ) ) -> U e. _V ) )
11 sseq1 
 |-  ( u = U -> ( u C_ ~P ( X X. X ) <-> U C_ ~P ( X X. X ) ) )
12 eleq2 
 |-  ( u = U -> ( ( X X. X ) e. u <-> ( X X. X ) e. U ) )
13 eleq2 
 |-  ( u = U -> ( w e. u <-> w e. U ) )
14 13 imbi2d 
 |-  ( u = U -> ( ( v C_ w -> w e. u ) <-> ( v C_ w -> w e. U ) ) )
15 14 ralbidv 
 |-  ( u = U -> ( 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 ) ) )
16 eleq2 
 |-  ( u = U -> ( ( v i^i w ) e. u <-> ( v i^i w ) e. U ) )
17 16 raleqbi1dv 
 |-  ( u = U -> ( A. w e. u ( v i^i w ) e. u <-> A. w e. U ( v i^i w ) e. U ) )
18 eleq2 
 |-  ( u = U -> ( `' v e. u <-> `' v e. U ) )
19 rexeq 
 |-  ( u = U -> ( E. w e. u ( w o. w ) C_ v <-> E. w e. U ( w o. w ) C_ v ) )
20 18 19 3anbi23d 
 |-  ( u = U -> ( ( ( _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 ) ) )
21 15 17 20 3anbi123d 
 |-  ( u = 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. 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 ) ) ) )
22 21 raleqbi1dv 
 |-  ( u = 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 ) ) <-> 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 ) ) ) )
23 11 12 22 3anbi123d 
 |-  ( u = 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 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 ) ) ) ) )
24 23 elab3g 
 |-  ( ( ( 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 e. _V ) -> ( U e. { 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 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 ) ) ) ) )
25 10 24 syl 
 |-  ( X e. V -> ( U e. { 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 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 ) ) ) ) )
26 2 25 bitrd 
 |-  ( 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 ) ) ) ) )