Metamath Proof Explorer


Theorem fcoinvbr

Description: Binary relation for the equivalence relation from fcoinver . (Contributed by Thierry Arnoux, 3-Jan-2020)

Ref Expression
Hypothesis fcoinvbr.e
|- .~ = ( `' F o. F )
Assertion fcoinvbr
|- ( ( F Fn A /\ X e. A /\ Y e. A ) -> ( X .~ Y <-> ( F ` X ) = ( F ` Y ) ) )

Proof

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