Metamath Proof Explorer

Theorem tgjustr

Description: Given any equivalence relation R , one can define a function f such that all elements of an equivalence classe of R have the same image by f . (Contributed by Thierry Arnoux, 25-Jan-2023)

Ref Expression
Assertion tgjustr 
|- ( ( A e. V /\ R Er A ) -> E. f ( f Fn A /\ A. x e. A A. y e. A ( x R y <-> ( f ` x ) = ( f ` y ) ) ) )

Proof

Step Hyp Ref Expression
1 erex 
 |-  ( R Er A -> ( A e. V -> R e. _V ) )
2 1 impcom 
 |-  ( ( A e. V /\ R Er A ) -> R e. _V )
3 ecexg 
 |-  ( R e. _V -> [ u ] R e. _V )
4 2 3 syl 
 |-  ( ( A e. V /\ R Er A ) -> [ u ] R e. _V )
5 4 adantr 
 |-  ( ( ( A e. V /\ R Er A ) /\ u e. A ) -> [ u ] R e. _V )
6 5 ralrimiva 
 |-  ( ( A e. V /\ R Er A ) -> A. u e. A [ u ] R e. _V )
7 eqid 
 |-  ( u e. A |-> [ u ] R ) = ( u e. A |-> [ u ] R )
8 7 fnmpt 
 |-  ( A. u e. A [ u ] R e. _V -> ( u e. A |-> [ u ] R ) Fn A )
9 6 8 syl 
 |-  ( ( A e. V /\ R Er A ) -> ( u e. A |-> [ u ] R ) Fn A )
10 simpllr 
 |-  ( ( ( ( A e. V /\ R Er A ) /\ x e. A ) /\ y e. A ) -> R Er A )
11 simpr 
 |-  ( ( ( A e. V /\ R Er A ) /\ x e. A ) -> x e. A )
12 11 adantr 
 |-  ( ( ( ( A e. V /\ R Er A ) /\ x e. A ) /\ y e. A ) -> x e. A )
13 10 12 erth 
 |-  ( ( ( ( A e. V /\ R Er A ) /\ x e. A ) /\ y e. A ) -> ( x R y <-> [ x ] R = [ y ] R ) )
14 eceq1 
 |-  ( u = x -> [ u ] R = [ x ] R )
15 ecelqsg 
 |-  ( ( R e. _V /\ x e. A ) -> [ x ] R e. ( A /. R ) )
16 2 15 sylan 
 |-  ( ( ( A e. V /\ R Er A ) /\ x e. A ) -> [ x ] R e. ( A /. R ) )
17 7 14 11 16 fvmptd3 
 |-  ( ( ( A e. V /\ R Er A ) /\ x e. A ) -> ( ( u e. A |-> [ u ] R ) ` x ) = [ x ] R )
18 17 adantr 
 |-  ( ( ( ( A e. V /\ R Er A ) /\ x e. A ) /\ y e. A ) -> ( ( u e. A |-> [ u ] R ) ` x ) = [ x ] R )
19 eceq1 
 |-  ( u = y -> [ u ] R = [ y ] R )
20 simpr 
 |-  ( ( ( A e. V /\ R Er A ) /\ y e. A ) -> y e. A )
21 ecelqsg 
 |-  ( ( R e. _V /\ y e. A ) -> [ y ] R e. ( A /. R ) )
22 2 21 sylan 
 |-  ( ( ( A e. V /\ R Er A ) /\ y e. A ) -> [ y ] R e. ( A /. R ) )
23 7 19 20 22 fvmptd3 
 |-  ( ( ( A e. V /\ R Er A ) /\ y e. A ) -> ( ( u e. A |-> [ u ] R ) ` y ) = [ y ] R )
24 23 adantlr 
 |-  ( ( ( ( A e. V /\ R Er A ) /\ x e. A ) /\ y e. A ) -> ( ( u e. A |-> [ u ] R ) ` y ) = [ y ] R )
25 18 24 eqeq12d 
 |-  ( ( ( ( A e. V /\ R Er A ) /\ x e. A ) /\ y e. A ) -> ( ( ( u e. A |-> [ u ] R ) ` x ) = ( ( u e. A |-> [ u ] R ) ` y ) <-> [ x ] R = [ y ] R ) )
26 13 25 bitr4d 
 |-  ( ( ( ( A e. V /\ R Er A ) /\ x e. A ) /\ y e. A ) -> ( x R y <-> ( ( u e. A |-> [ u ] R ) ` x ) = ( ( u e. A |-> [ u ] R ) ` y ) ) )
27 26 ralrimiva 
 |-  ( ( ( A e. V /\ R Er A ) /\ x e. A ) -> A. y e. A ( x R y <-> ( ( u e. A |-> [ u ] R ) ` x ) = ( ( u e. A |-> [ u ] R ) ` y ) ) )
28 27 ralrimiva 
 |-  ( ( A e. V /\ R Er A ) -> A. x e. A A. y e. A ( x R y <-> ( ( u e. A |-> [ u ] R ) ` x ) = ( ( u e. A |-> [ u ] R ) ` y ) ) )
29 mptexg 
 |-  ( A e. V -> ( u e. A |-> [ u ] R ) e. _V )
30 29 adantr 
 |-  ( ( A e. V /\ R Er A ) -> ( u e. A |-> [ u ] R ) e. _V )
31 fneq1 
 |-  ( f = ( u e. A |-> [ u ] R ) -> ( f Fn A <-> ( u e. A |-> [ u ] R ) Fn A ) )
32 simpl 
 |-  ( ( f = ( u e. A |-> [ u ] R ) /\ ( x e. A /\ y e. A ) ) -> f = ( u e. A |-> [ u ] R ) )
33 32 fveq1d 
 |-  ( ( f = ( u e. A |-> [ u ] R ) /\ ( x e. A /\ y e. A ) ) -> ( f ` x ) = ( ( u e. A |-> [ u ] R ) ` x ) )
34 32 fveq1d 
 |-  ( ( f = ( u e. A |-> [ u ] R ) /\ ( x e. A /\ y e. A ) ) -> ( f ` y ) = ( ( u e. A |-> [ u ] R ) ` y ) )
35 33 34 eqeq12d 
 |-  ( ( f = ( u e. A |-> [ u ] R ) /\ ( x e. A /\ y e. A ) ) -> ( ( f ` x ) = ( f ` y ) <-> ( ( u e. A |-> [ u ] R ) ` x ) = ( ( u e. A |-> [ u ] R ) ` y ) ) )
36 35 bibi2d 
 |-  ( ( f = ( u e. A |-> [ u ] R ) /\ ( x e. A /\ y e. A ) ) -> ( ( x R y <-> ( f ` x ) = ( f ` y ) ) <-> ( x R y <-> ( ( u e. A |-> [ u ] R ) ` x ) = ( ( u e. A |-> [ u ] R ) ` y ) ) ) )
37 36 2ralbidva 
 |-  ( f = ( u e. A |-> [ u ] R ) -> ( A. x e. A A. y e. A ( x R y <-> ( f ` x ) = ( f ` y ) ) <-> A. x e. A A. y e. A ( x R y <-> ( ( u e. A |-> [ u ] R ) ` x ) = ( ( u e. A |-> [ u ] R ) ` y ) ) ) )
38 31 37 anbi12d 
 |-  ( f = ( u e. A |-> [ u ] R ) -> ( ( f Fn A /\ A. x e. A A. y e. A ( x R y <-> ( f ` x ) = ( f ` y ) ) ) <-> ( ( u e. A |-> [ u ] R ) Fn A /\ A. x e. A A. y e. A ( x R y <-> ( ( u e. A |-> [ u ] R ) ` x ) = ( ( u e. A |-> [ u ] R ) ` y ) ) ) ) )
39 38 spcegv 
 |-  ( ( u e. A |-> [ u ] R ) e. _V -> ( ( ( u e. A |-> [ u ] R ) Fn A /\ A. x e. A A. y e. A ( x R y <-> ( ( u e. A |-> [ u ] R ) ` x ) = ( ( u e. A |-> [ u ] R ) ` y ) ) ) -> E. f ( f Fn A /\ A. x e. A A. y e. A ( x R y <-> ( f ` x ) = ( f ` y ) ) ) ) )
40 30 39 syl 
 |-  ( ( A e. V /\ R Er A ) -> ( ( ( u e. A |-> [ u ] R ) Fn A /\ A. x e. A A. y e. A ( x R y <-> ( ( u e. A |-> [ u ] R ) ` x ) = ( ( u e. A |-> [ u ] R ) ` y ) ) ) -> E. f ( f Fn A /\ A. x e. A A. y e. A ( x R y <-> ( f ` x ) = ( f ` y ) ) ) ) )
41 9 28 40 mp2and 
 |-  ( ( A e. V /\ R Er A ) -> E. f ( f Fn A /\ A. x e. A A. y e. A ( x R y <-> ( f ` x ) = ( f ` y ) ) ) )