Metamath Proof Explorer

Theorem tgjustf

Description: Given any function F , equality of the image by F is an equivalence relation. (Contributed by Thierry Arnoux, 25-Jan-2023)

Ref Expression
Assertion tgjustf 
|- ( A e. V -> E. r ( r Er A /\ A. x e. A A. y e. A ( x r y <-> ( F ` x ) = ( F ` y ) ) ) )

Proof

Step Hyp Ref Expression
1 relopabv 
 |-  Rel { <. u , v >. | ( ( u e. A /\ v e. A ) /\ ( F ` u ) = ( F ` v ) ) }
2 ancom 
 |-  ( ( x e. A /\ y e. A ) <-> ( y e. A /\ x e. A ) )
3 eqcom 
 |-  ( ( F ` x ) = ( F ` y ) <-> ( F ` y ) = ( F ` x ) )
4 2 3 anbi12i 
 |-  ( ( ( x e. A /\ y e. A ) /\ ( F ` x ) = ( F ` y ) ) <-> ( ( y e. A /\ x e. A ) /\ ( F ` y ) = ( F ` x ) ) )
5 simpl 
 |-  ( ( u = x /\ v = y ) -> u = x )
6 5 fveq2d 
 |-  ( ( u = x /\ v = y ) -> ( F ` u ) = ( F ` x ) )
7 simpr 
 |-  ( ( u = x /\ v = y ) -> v = y )
8 7 fveq2d 
 |-  ( ( u = x /\ v = y ) -> ( F ` v ) = ( F ` y ) )
9 6 8 eqeq12d 
 |-  ( ( u = x /\ v = y ) -> ( ( F ` u ) = ( F ` v ) <-> ( F ` x ) = ( F ` y ) ) )
10 eqid 
 |-  { <. u , v >. | ( ( u e. A /\ v e. A ) /\ ( F ` u ) = ( F ` v ) ) } = { <. u , v >. | ( ( u e. A /\ v e. A ) /\ ( F ` u ) = ( F ` v ) ) }
11 9 10 brab2a 
 |-  ( x { <. u , v >. | ( ( u e. A /\ v e. A ) /\ ( F ` u ) = ( F ` v ) ) } y <-> ( ( x e. A /\ y e. A ) /\ ( F ` x ) = ( F ` y ) ) )
12 simpl 
 |-  ( ( u = y /\ v = x ) -> u = y )
13 12 fveq2d 
 |-  ( ( u = y /\ v = x ) -> ( F ` u ) = ( F ` y ) )
14 simpr 
 |-  ( ( u = y /\ v = x ) -> v = x )
15 14 fveq2d 
 |-  ( ( u = y /\ v = x ) -> ( F ` v ) = ( F ` x ) )
16 13 15 eqeq12d 
 |-  ( ( u = y /\ v = x ) -> ( ( F ` u ) = ( F ` v ) <-> ( F ` y ) = ( F ` x ) ) )
17 16 10 brab2a 
 |-  ( y { <. u , v >. | ( ( u e. A /\ v e. A ) /\ ( F ` u ) = ( F ` v ) ) } x <-> ( ( y e. A /\ x e. A ) /\ ( F ` y ) = ( F ` x ) ) )
18 4 11 17 3bitr4i 
 |-  ( x { <. u , v >. | ( ( u e. A /\ v e. A ) /\ ( F ` u ) = ( F ` v ) ) } y <-> y { <. u , v >. | ( ( u e. A /\ v e. A ) /\ ( F ` u ) = ( F ` v ) ) } x )
19 18 biimpi 
 |-  ( x { <. u , v >. | ( ( u e. A /\ v e. A ) /\ ( F ` u ) = ( F ` v ) ) } y -> y { <. u , v >. | ( ( u e. A /\ v e. A ) /\ ( F ` u ) = ( F ` v ) ) } x )
20 simplll 
 |-  ( ( ( ( x e. A /\ y e. A ) /\ ( F ` x ) = ( F ` y ) ) /\ ( ( y e. A /\ z e. A ) /\ ( F ` y ) = ( F ` z ) ) ) -> x e. A )
21 simprlr 
 |-  ( ( ( ( x e. A /\ y e. A ) /\ ( F ` x ) = ( F ` y ) ) /\ ( ( y e. A /\ z e. A ) /\ ( F ` y ) = ( F ` z ) ) ) -> z e. A )
22 simplr 
 |-  ( ( ( ( x e. A /\ y e. A ) /\ ( F ` x ) = ( F ` y ) ) /\ ( ( y e. A /\ z e. A ) /\ ( F ` y ) = ( F ` z ) ) ) -> ( F ` x ) = ( F ` y ) )
23 simprr 
 |-  ( ( ( ( x e. A /\ y e. A ) /\ ( F ` x ) = ( F ` y ) ) /\ ( ( y e. A /\ z e. A ) /\ ( F ` y ) = ( F ` z ) ) ) -> ( F ` y ) = ( F ` z ) )
24 22 23 eqtrd 
 |-  ( ( ( ( x e. A /\ y e. A ) /\ ( F ` x ) = ( F ` y ) ) /\ ( ( y e. A /\ z e. A ) /\ ( F ` y ) = ( F ` z ) ) ) -> ( F ` x ) = ( F ` z ) )
25 20 21 24 jca31 
 |-  ( ( ( ( x e. A /\ y e. A ) /\ ( F ` x ) = ( F ` y ) ) /\ ( ( y e. A /\ z e. A ) /\ ( F ` y ) = ( F ` z ) ) ) -> ( ( x e. A /\ z e. A ) /\ ( F ` x ) = ( F ` z ) ) )
26 simpl 
 |-  ( ( u = y /\ v = z ) -> u = y )
27 26 fveq2d 
 |-  ( ( u = y /\ v = z ) -> ( F ` u ) = ( F ` y ) )
28 simpr 
 |-  ( ( u = y /\ v = z ) -> v = z )
29 28 fveq2d 
 |-  ( ( u = y /\ v = z ) -> ( F ` v ) = ( F ` z ) )
30 27 29 eqeq12d 
 |-  ( ( u = y /\ v = z ) -> ( ( F ` u ) = ( F ` v ) <-> ( F ` y ) = ( F ` z ) ) )
31 30 10 brab2a 
 |-  ( y { <. u , v >. | ( ( u e. A /\ v e. A ) /\ ( F ` u ) = ( F ` v ) ) } z <-> ( ( y e. A /\ z e. A ) /\ ( F ` y ) = ( F ` z ) ) )
32 11 31 anbi12i 
 |-  ( ( x { <. u , v >. | ( ( u e. A /\ v e. A ) /\ ( F ` u ) = ( F ` v ) ) } y /\ y { <. u , v >. | ( ( u e. A /\ v e. A ) /\ ( F ` u ) = ( F ` v ) ) } z ) <-> ( ( ( x e. A /\ y e. A ) /\ ( F ` x ) = ( F ` y ) ) /\ ( ( y e. A /\ z e. A ) /\ ( F ` y ) = ( F ` z ) ) ) )
33 simpl 
 |-  ( ( u = x /\ v = z ) -> u = x )
34 33 fveq2d 
 |-  ( ( u = x /\ v = z ) -> ( F ` u ) = ( F ` x ) )
35 simpr 
 |-  ( ( u = x /\ v = z ) -> v = z )
36 35 fveq2d 
 |-  ( ( u = x /\ v = z ) -> ( F ` v ) = ( F ` z ) )
37 34 36 eqeq12d 
 |-  ( ( u = x /\ v = z ) -> ( ( F ` u ) = ( F ` v ) <-> ( F ` x ) = ( F ` z ) ) )
38 37 10 brab2a 
 |-  ( x { <. u , v >. | ( ( u e. A /\ v e. A ) /\ ( F ` u ) = ( F ` v ) ) } z <-> ( ( x e. A /\ z e. A ) /\ ( F ` x ) = ( F ` z ) ) )
39 25 32 38 3imtr4i 
 |-  ( ( x { <. u , v >. | ( ( u e. A /\ v e. A ) /\ ( F ` u ) = ( F ` v ) ) } y /\ y { <. u , v >. | ( ( u e. A /\ v e. A ) /\ ( F ` u ) = ( F ` v ) ) } z ) -> x { <. u , v >. | ( ( u e. A /\ v e. A ) /\ ( F ` u ) = ( F ` v ) ) } z )
40 eqid 
 |-  ( F ` x ) = ( F ` x )
41 40 biantru 
 |-  ( ( x e. A /\ x e. A ) <-> ( ( x e. A /\ x e. A ) /\ ( F ` x ) = ( F ` x ) ) )
42 pm4.24 
 |-  ( x e. A <-> ( x e. A /\ x e. A ) )
43 simpl 
 |-  ( ( u = x /\ v = x ) -> u = x )
44 43 fveq2d 
 |-  ( ( u = x /\ v = x ) -> ( F ` u ) = ( F ` x ) )
45 simpr 
 |-  ( ( u = x /\ v = x ) -> v = x )
46 45 fveq2d 
 |-  ( ( u = x /\ v = x ) -> ( F ` v ) = ( F ` x ) )
47 44 46 eqeq12d 
 |-  ( ( u = x /\ v = x ) -> ( ( F ` u ) = ( F ` v ) <-> ( F ` x ) = ( F ` x ) ) )
48 47 10 brab2a 
 |-  ( x { <. u , v >. | ( ( u e. A /\ v e. A ) /\ ( F ` u ) = ( F ` v ) ) } x <-> ( ( x e. A /\ x e. A ) /\ ( F ` x ) = ( F ` x ) ) )
49 41 42 48 3bitr4i 
 |-  ( x e. A <-> x { <. u , v >. | ( ( u e. A /\ v e. A ) /\ ( F ` u ) = ( F ` v ) ) } x )
50 1 19 39 49 iseri 
 |-  { <. u , v >. | ( ( u e. A /\ v e. A ) /\ ( F ` u ) = ( F ` v ) ) } Er A
51 11 baib 
 |-  ( ( x e. A /\ y e. A ) -> ( x { <. u , v >. | ( ( u e. A /\ v e. A ) /\ ( F ` u ) = ( F ` v ) ) } y <-> ( F ` x ) = ( F ` y ) ) )
52 51 rgen2 
 |-  A. x e. A A. y e. A ( x { <. u , v >. | ( ( u e. A /\ v e. A ) /\ ( F ` u ) = ( F ` v ) ) } y <-> ( F ` x ) = ( F ` y ) )
53 id 
 |-  ( A e. V -> A e. V )
54 simprll 
 |-  ( ( A e. V /\ ( ( u e. A /\ v e. A ) /\ ( F ` u ) = ( F ` v ) ) ) -> u e. A )
55 simprlr 
 |-  ( ( A e. V /\ ( ( u e. A /\ v e. A ) /\ ( F ` u ) = ( F ` v ) ) ) -> v e. A )
56 53 53 54 55 opabex2 
 |-  ( A e. V -> { <. u , v >. | ( ( u e. A /\ v e. A ) /\ ( F ` u ) = ( F ` v ) ) } e. _V )
57 ereq1 
 |-  ( r = { <. u , v >. | ( ( u e. A /\ v e. A ) /\ ( F ` u ) = ( F ` v ) ) } -> ( r Er A <-> { <. u , v >. | ( ( u e. A /\ v e. A ) /\ ( F ` u ) = ( F ` v ) ) } Er A ) )
58 simpl 
 |-  ( ( r = { <. u , v >. | ( ( u e. A /\ v e. A ) /\ ( F ` u ) = ( F ` v ) ) } /\ ( x e. A /\ y e. A ) ) -> r = { <. u , v >. | ( ( u e. A /\ v e. A ) /\ ( F ` u ) = ( F ` v ) ) } )
59 58 breqd 
 |-  ( ( r = { <. u , v >. | ( ( u e. A /\ v e. A ) /\ ( F ` u ) = ( F ` v ) ) } /\ ( x e. A /\ y e. A ) ) -> ( x r y <-> x { <. u , v >. | ( ( u e. A /\ v e. A ) /\ ( F ` u ) = ( F ` v ) ) } y ) )
60 59 bibi1d 
 |-  ( ( r = { <. u , v >. | ( ( u e. A /\ v e. A ) /\ ( F ` u ) = ( F ` v ) ) } /\ ( x e. A /\ y e. A ) ) -> ( ( x r y <-> ( F ` x ) = ( F ` y ) ) <-> ( x { <. u , v >. | ( ( u e. A /\ v e. A ) /\ ( F ` u ) = ( F ` v ) ) } y <-> ( F ` x ) = ( F ` y ) ) ) )
61 60 2ralbidva 
 |-  ( r = { <. u , v >. | ( ( u e. A /\ v e. A ) /\ ( F ` u ) = ( F ` v ) ) } -> ( A. x e. A A. y e. A ( x r y <-> ( F ` x ) = ( F ` y ) ) <-> A. x e. A A. y e. A ( x { <. u , v >. | ( ( u e. A /\ v e. A ) /\ ( F ` u ) = ( F ` v ) ) } y <-> ( F ` x ) = ( F ` y ) ) ) )
62 57 61 anbi12d 
 |-  ( r = { <. u , v >. | ( ( u e. A /\ v e. A ) /\ ( F ` u ) = ( F ` v ) ) } -> ( ( r Er A /\ A. x e. A A. y e. A ( x r y <-> ( F ` x ) = ( F ` y ) ) ) <-> ( { <. u , v >. | ( ( u e. A /\ v e. A ) /\ ( F ` u ) = ( F ` v ) ) } Er A /\ A. x e. A A. y e. A ( x { <. u , v >. | ( ( u e. A /\ v e. A ) /\ ( F ` u ) = ( F ` v ) ) } y <-> ( F ` x ) = ( F ` y ) ) ) ) )
63 62 spcegv 
 |-  ( { <. u , v >. | ( ( u e. A /\ v e. A ) /\ ( F ` u ) = ( F ` v ) ) } e. _V -> ( ( { <. u , v >. | ( ( u e. A /\ v e. A ) /\ ( F ` u ) = ( F ` v ) ) } Er A /\ A. x e. A A. y e. A ( x { <. u , v >. | ( ( u e. A /\ v e. A ) /\ ( F ` u ) = ( F ` v ) ) } y <-> ( F ` x ) = ( F ` y ) ) ) -> E. r ( r Er A /\ A. x e. A A. y e. A ( x r y <-> ( F ` x ) = ( F ` y ) ) ) ) )
64 56 63 syl 
 |-  ( A e. V -> ( ( { <. u , v >. | ( ( u e. A /\ v e. A ) /\ ( F ` u ) = ( F ` v ) ) } Er A /\ A. x e. A A. y e. A ( x { <. u , v >. | ( ( u e. A /\ v e. A ) /\ ( F ` u ) = ( F ` v ) ) } y <-> ( F ` x ) = ( F ` y ) ) ) -> E. r ( r Er A /\ A. x e. A A. y e. A ( x r y <-> ( F ` x ) = ( F ` y ) ) ) ) )
65 50 52 64 mp2ani 
 |-  ( A e. V -> E. r ( r Er A /\ A. x e. A A. y e. A ( x r y <-> ( F ` x ) = ( F ` y ) ) ) )