Step |
Hyp |
Ref |
Expression |
1 |
|
fcoinvbr.e |
|- .~ = ( `' F o. F ) |
2 |
1
|
breqi |
|- ( X .~ Y <-> X ( `' F o. F ) Y ) |
3 |
|
brcog |
|- ( ( X e. A /\ Y e. A ) -> ( X ( `' F o. F ) Y <-> E. z ( X F z /\ z `' F Y ) ) ) |
4 |
2 3
|
syl5bb |
|- ( ( X e. A /\ Y e. A ) -> ( X .~ Y <-> E. z ( X F z /\ z `' F Y ) ) ) |
5 |
4
|
3adant1 |
|- ( ( F Fn A /\ X e. A /\ Y e. A ) -> ( X .~ Y <-> E. z ( X F z /\ z `' F Y ) ) ) |
6 |
|
fvex |
|- ( F ` X ) e. _V |
7 |
6
|
eqvinc |
|- ( ( F ` X ) = ( F ` Y ) <-> E. z ( z = ( F ` X ) /\ z = ( F ` Y ) ) ) |
8 |
|
eqcom |
|- ( z = ( F ` X ) <-> ( F ` X ) = z ) |
9 |
|
eqcom |
|- ( z = ( F ` Y ) <-> ( F ` Y ) = z ) |
10 |
8 9
|
anbi12i |
|- ( ( z = ( F ` X ) /\ z = ( F ` Y ) ) <-> ( ( F ` X ) = z /\ ( F ` Y ) = z ) ) |
11 |
10
|
exbii |
|- ( E. z ( z = ( F ` X ) /\ z = ( F ` Y ) ) <-> E. z ( ( F ` X ) = z /\ ( F ` Y ) = z ) ) |
12 |
7 11
|
bitri |
|- ( ( F ` X ) = ( F ` Y ) <-> E. z ( ( F ` X ) = z /\ ( F ` Y ) = z ) ) |
13 |
|
fnbrfvb |
|- ( ( F Fn A /\ X e. A ) -> ( ( F ` X ) = z <-> X F z ) ) |
14 |
13
|
3adant3 |
|- ( ( F Fn A /\ X e. A /\ Y e. A ) -> ( ( F ` X ) = z <-> X F z ) ) |
15 |
|
fnbrfvb |
|- ( ( F Fn A /\ Y e. A ) -> ( ( F ` Y ) = z <-> Y F z ) ) |
16 |
15
|
3adant2 |
|- ( ( F Fn A /\ X e. A /\ Y e. A ) -> ( ( F ` Y ) = z <-> Y F z ) ) |
17 |
14 16
|
anbi12d |
|- ( ( F Fn A /\ X e. A /\ Y e. A ) -> ( ( ( F ` X ) = z /\ ( F ` Y ) = z ) <-> ( X F z /\ Y F z ) ) ) |
18 |
|
vex |
|- z e. _V |
19 |
|
brcnvg |
|- ( ( z e. _V /\ Y e. A ) -> ( z `' F Y <-> Y F z ) ) |
20 |
18 19
|
mpan |
|- ( Y e. A -> ( z `' F Y <-> Y F z ) ) |
21 |
20
|
3ad2ant3 |
|- ( ( F Fn A /\ X e. A /\ Y e. A ) -> ( z `' F Y <-> Y F z ) ) |
22 |
21
|
anbi2d |
|- ( ( F Fn A /\ X e. A /\ Y e. A ) -> ( ( X F z /\ z `' F Y ) <-> ( X F z /\ Y F z ) ) ) |
23 |
17 22
|
bitr4d |
|- ( ( F Fn A /\ X e. A /\ Y e. A ) -> ( ( ( F ` X ) = z /\ ( F ` Y ) = z ) <-> ( X F z /\ z `' F Y ) ) ) |
24 |
23
|
exbidv |
|- ( ( F Fn A /\ X e. A /\ Y e. A ) -> ( E. z ( ( F ` X ) = z /\ ( F ` Y ) = z ) <-> E. z ( X F z /\ z `' F Y ) ) ) |
25 |
12 24
|
syl5bb |
|- ( ( F Fn A /\ X e. A /\ Y e. A ) -> ( ( F ` X ) = ( F ` Y ) <-> E. z ( X F z /\ z `' F Y ) ) ) |
26 |
5 25
|
bitr4d |
|- ( ( F Fn A /\ X e. A /\ Y e. A ) -> ( X .~ Y <-> ( F ` X ) = ( F ` Y ) ) ) |