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