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 ) ) ) ) ) |