Step |
Hyp |
Ref |
Expression |
1 |
|
fvmptopab.1 |
|- ( ( ph /\ z = Z ) -> ( ch <-> ps ) ) |
2 |
|
fvmptopab.2 |
|- ( ph -> { <. x , y >. | x ( F ` Z ) y } e. _V ) |
3 |
|
fvmptopab.3 |
|- M = ( z e. _V |-> { <. x , y >. | ( x ( F ` z ) y /\ ch ) } ) |
4 |
|
fveq2 |
|- ( z = Z -> ( F ` z ) = ( F ` Z ) ) |
5 |
4
|
breqd |
|- ( z = Z -> ( x ( F ` z ) y <-> x ( F ` Z ) y ) ) |
6 |
5
|
adantl |
|- ( ( ( Z e. _V /\ ph ) /\ z = Z ) -> ( x ( F ` z ) y <-> x ( F ` Z ) y ) ) |
7 |
1
|
adantll |
|- ( ( ( Z e. _V /\ ph ) /\ z = Z ) -> ( ch <-> ps ) ) |
8 |
6 7
|
anbi12d |
|- ( ( ( Z e. _V /\ ph ) /\ z = Z ) -> ( ( x ( F ` z ) y /\ ch ) <-> ( x ( F ` Z ) y /\ ps ) ) ) |
9 |
8
|
opabbidv |
|- ( ( ( Z e. _V /\ ph ) /\ z = Z ) -> { <. x , y >. | ( x ( F ` z ) y /\ ch ) } = { <. x , y >. | ( x ( F ` Z ) y /\ ps ) } ) |
10 |
|
simpl |
|- ( ( Z e. _V /\ ph ) -> Z e. _V ) |
11 |
|
id |
|- ( x ( F ` Z ) y -> x ( F ` Z ) y ) |
12 |
11
|
gen2 |
|- A. x A. y ( x ( F ` Z ) y -> x ( F ` Z ) y ) |
13 |
2
|
adantl |
|- ( ( Z e. _V /\ ph ) -> { <. x , y >. | x ( F ` Z ) y } e. _V ) |
14 |
|
opabbrex |
|- ( ( A. x A. y ( x ( F ` Z ) y -> x ( F ` Z ) y ) /\ { <. x , y >. | x ( F ` Z ) y } e. _V ) -> { <. x , y >. | ( x ( F ` Z ) y /\ ps ) } e. _V ) |
15 |
12 13 14
|
sylancr |
|- ( ( Z e. _V /\ ph ) -> { <. x , y >. | ( x ( F ` Z ) y /\ ps ) } e. _V ) |
16 |
3 9 10 15
|
fvmptd2 |
|- ( ( Z e. _V /\ ph ) -> ( M ` Z ) = { <. x , y >. | ( x ( F ` Z ) y /\ ps ) } ) |
17 |
16
|
ex |
|- ( Z e. _V -> ( ph -> ( M ` Z ) = { <. x , y >. | ( x ( F ` Z ) y /\ ps ) } ) ) |
18 |
|
fvprc |
|- ( -. Z e. _V -> ( M ` Z ) = (/) ) |
19 |
|
br0 |
|- -. x (/) y |
20 |
|
fvprc |
|- ( -. Z e. _V -> ( F ` Z ) = (/) ) |
21 |
20
|
breqd |
|- ( -. Z e. _V -> ( x ( F ` Z ) y <-> x (/) y ) ) |
22 |
19 21
|
mtbiri |
|- ( -. Z e. _V -> -. x ( F ` Z ) y ) |
23 |
22
|
intnanrd |
|- ( -. Z e. _V -> -. ( x ( F ` Z ) y /\ ps ) ) |
24 |
23
|
alrimivv |
|- ( -. Z e. _V -> A. x A. y -. ( x ( F ` Z ) y /\ ps ) ) |
25 |
|
opab0 |
|- ( { <. x , y >. | ( x ( F ` Z ) y /\ ps ) } = (/) <-> A. x A. y -. ( x ( F ` Z ) y /\ ps ) ) |
26 |
24 25
|
sylibr |
|- ( -. Z e. _V -> { <. x , y >. | ( x ( F ` Z ) y /\ ps ) } = (/) ) |
27 |
18 26
|
eqtr4d |
|- ( -. Z e. _V -> ( M ` Z ) = { <. x , y >. | ( x ( F ` Z ) y /\ ps ) } ) |
28 |
27
|
a1d |
|- ( -. Z e. _V -> ( ph -> ( M ` Z ) = { <. x , y >. | ( x ( F ` Z ) y /\ ps ) } ) ) |
29 |
17 28
|
pm2.61i |
|- ( ph -> ( M ` Z ) = { <. x , y >. | ( x ( F ` Z ) y /\ ps ) } ) |