Step |
Hyp |
Ref |
Expression |
1 |
|
brfvopabrbr.1 |
|- ( A ` Z ) = { <. x , y >. | ( x ( B ` Z ) y /\ ph ) } |
2 |
|
brfvopabrbr.2 |
|- ( ( x = X /\ y = Y ) -> ( ph <-> ps ) ) |
3 |
|
brfvopabrbr.3 |
|- Rel ( B ` Z ) |
4 |
|
brne0 |
|- ( X ( A ` Z ) Y -> ( A ` Z ) =/= (/) ) |
5 |
|
fvprc |
|- ( -. Z e. _V -> ( A ` Z ) = (/) ) |
6 |
5
|
necon1ai |
|- ( ( A ` Z ) =/= (/) -> Z e. _V ) |
7 |
4 6
|
syl |
|- ( X ( A ` Z ) Y -> Z e. _V ) |
8 |
1
|
relopabiv |
|- Rel ( A ` Z ) |
9 |
8
|
brrelex1i |
|- ( X ( A ` Z ) Y -> X e. _V ) |
10 |
8
|
brrelex2i |
|- ( X ( A ` Z ) Y -> Y e. _V ) |
11 |
7 9 10
|
3jca |
|- ( X ( A ` Z ) Y -> ( Z e. _V /\ X e. _V /\ Y e. _V ) ) |
12 |
|
brne0 |
|- ( X ( B ` Z ) Y -> ( B ` Z ) =/= (/) ) |
13 |
|
fvprc |
|- ( -. Z e. _V -> ( B ` Z ) = (/) ) |
14 |
13
|
necon1ai |
|- ( ( B ` Z ) =/= (/) -> Z e. _V ) |
15 |
12 14
|
syl |
|- ( X ( B ` Z ) Y -> Z e. _V ) |
16 |
3
|
brrelex1i |
|- ( X ( B ` Z ) Y -> X e. _V ) |
17 |
3
|
brrelex2i |
|- ( X ( B ` Z ) Y -> Y e. _V ) |
18 |
15 16 17
|
3jca |
|- ( X ( B ` Z ) Y -> ( Z e. _V /\ X e. _V /\ Y e. _V ) ) |
19 |
18
|
adantr |
|- ( ( X ( B ` Z ) Y /\ ps ) -> ( Z e. _V /\ X e. _V /\ Y e. _V ) ) |
20 |
1
|
a1i |
|- ( Z e. _V -> ( A ` Z ) = { <. x , y >. | ( x ( B ` Z ) y /\ ph ) } ) |
21 |
20 2
|
rbropap |
|- ( ( Z e. _V /\ X e. _V /\ Y e. _V ) -> ( X ( A ` Z ) Y <-> ( X ( B ` Z ) Y /\ ps ) ) ) |
22 |
11 19 21
|
pm5.21nii |
|- ( X ( A ` Z ) Y <-> ( X ( B ` Z ) Y /\ ps ) ) |