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