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 ( ( 𝐴 ∈ 𝑉 ∧ 𝑅 Er 𝐴 ) → ∃ 𝑓 ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ↔ ( 𝑓 ‘ 𝑥 ) = ( 𝑓 ‘ 𝑦 ) ) ) )

Proof

Step Hyp Ref Expression
1 erex ⊢ ( 𝑅 Er 𝐴 → ( 𝐴 ∈ 𝑉 → 𝑅 ∈ V ) )
2 1 impcom ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑅 Er 𝐴 ) → 𝑅 ∈ V )
3 ecexg ⊢ ( 𝑅 ∈ V → [ 𝑢 ] 𝑅 ∈ V )
4 2 3 syl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑅 Er 𝐴 ) → [ 𝑢 ] 𝑅 ∈ V )
5 4 adantr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑅 Er 𝐴 ) ∧ 𝑢 ∈ 𝐴 ) → [ 𝑢 ] 𝑅 ∈ V )
6 5 ralrimiva ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑅 Er 𝐴 ) → ∀ 𝑢 ∈ 𝐴 [ 𝑢 ] 𝑅 ∈ V )
7 eqid ⊢ ( 𝑢 ∈ 𝐴 ↦ [ 𝑢 ] 𝑅 ) = ( 𝑢 ∈ 𝐴 ↦ [ 𝑢 ] 𝑅 )
8 7 fnmpt ⊢ ( ∀ 𝑢 ∈ 𝐴 [ 𝑢 ] 𝑅 ∈ V → ( 𝑢 ∈ 𝐴 ↦ [ 𝑢 ] 𝑅 ) Fn 𝐴 )
9 6 8 syl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑅 Er 𝐴 ) → ( 𝑢 ∈ 𝐴 ↦ [ 𝑢 ] 𝑅 ) Fn 𝐴 )
10 simpllr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑅 Er 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → 𝑅 Er 𝐴 )
11 simpr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑅 Er 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
12 11 adantr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑅 Er 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
13 10 12 erth ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑅 Er 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 𝑅 𝑦 ↔ [ 𝑥 ] 𝑅 = [ 𝑦 ] 𝑅 ) )
14 eceq1 ⊢ ( 𝑢 = 𝑥 → [ 𝑢 ] 𝑅 = [ 𝑥 ] 𝑅 )
15 ecelqsg ⊢ ( ( 𝑅 ∈ V ∧ 𝑥 ∈ 𝐴 ) → [ 𝑥 ] 𝑅 ∈ ( 𝐴 / 𝑅 ) )
16 2 15 sylan ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑅 Er 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) → [ 𝑥 ] 𝑅 ∈ ( 𝐴 / 𝑅 ) )
17 7 14 11 16 fvmptd3 ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑅 Er 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑢 ∈ 𝐴 ↦ [ 𝑢 ] 𝑅 ) ‘ 𝑥 ) = [ 𝑥 ] 𝑅 )
18 17 adantr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑅 Er 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝑢 ∈ 𝐴 ↦ [ 𝑢 ] 𝑅 ) ‘ 𝑥 ) = [ 𝑥 ] 𝑅 )
19 eceq1 ⊢ ( 𝑢 = 𝑦 → [ 𝑢 ] 𝑅 = [ 𝑦 ] 𝑅 )
20 simpr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑅 Er 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ 𝐴 )
21 ecelqsg ⊢ ( ( 𝑅 ∈ V ∧ 𝑦 ∈ 𝐴 ) → [ 𝑦 ] 𝑅 ∈ ( 𝐴 / 𝑅 ) )
22 2 21 sylan ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑅 Er 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → [ 𝑦 ] 𝑅 ∈ ( 𝐴 / 𝑅 ) )
23 7 19 20 22 fvmptd3 ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑅 Er 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝑢 ∈ 𝐴 ↦ [ 𝑢 ] 𝑅 ) ‘ 𝑦 ) = [ 𝑦 ] 𝑅 )
24 23 adantlr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑅 Er 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝑢 ∈ 𝐴 ↦ [ 𝑢 ] 𝑅 ) ‘ 𝑦 ) = [ 𝑦 ] 𝑅 )
25 18 24 eqeq12d ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑅 Er 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ( ( ( 𝑢 ∈ 𝐴 ↦ [ 𝑢 ] 𝑅 ) ‘ 𝑥 ) = ( ( 𝑢 ∈ 𝐴 ↦ [ 𝑢 ] 𝑅 ) ‘ 𝑦 ) ↔ [ 𝑥 ] 𝑅 = [ 𝑦 ] 𝑅 ) )
26 13 25 bitr4d ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑅 Er 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 𝑅 𝑦 ↔ ( ( 𝑢 ∈ 𝐴 ↦ [ 𝑢 ] 𝑅 ) ‘ 𝑥 ) = ( ( 𝑢 ∈ 𝐴 ↦ [ 𝑢 ] 𝑅 ) ‘ 𝑦 ) ) )
27 26 ralrimiva ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑅 Er 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) → ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ↔ ( ( 𝑢 ∈ 𝐴 ↦ [ 𝑢 ] 𝑅 ) ‘ 𝑥 ) = ( ( 𝑢 ∈ 𝐴 ↦ [ 𝑢 ] 𝑅 ) ‘ 𝑦 ) ) )
28 27 ralrimiva ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑅 Er 𝐴 ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ↔ ( ( 𝑢 ∈ 𝐴 ↦ [ 𝑢 ] 𝑅 ) ‘ 𝑥 ) = ( ( 𝑢 ∈ 𝐴 ↦ [ 𝑢 ] 𝑅 ) ‘ 𝑦 ) ) )
29 mptexg ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑢 ∈ 𝐴 ↦ [ 𝑢 ] 𝑅 ) ∈ V )
30 29 adantr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑅 Er 𝐴 ) → ( 𝑢 ∈ 𝐴 ↦ [ 𝑢 ] 𝑅 ) ∈ V )
31 fneq1 ⊢ ( 𝑓 = ( 𝑢 ∈ 𝐴 ↦ [ 𝑢 ] 𝑅 ) → ( 𝑓 Fn 𝐴 ↔ ( 𝑢 ∈ 𝐴 ↦ [ 𝑢 ] 𝑅 ) Fn 𝐴 ) )
32 simpl ⊢ ( ( 𝑓 = ( 𝑢 ∈ 𝐴 ↦ [ 𝑢 ] 𝑅 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → 𝑓 = ( 𝑢 ∈ 𝐴 ↦ [ 𝑢 ] 𝑅 ) )
33 32 fveq1d ⊢ ( ( 𝑓 = ( 𝑢 ∈ 𝐴 ↦ [ 𝑢 ] 𝑅 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝑓 ‘ 𝑥 ) = ( ( 𝑢 ∈ 𝐴 ↦ [ 𝑢 ] 𝑅 ) ‘ 𝑥 ) )
34 32 fveq1d ⊢ ( ( 𝑓 = ( 𝑢 ∈ 𝐴 ↦ [ 𝑢 ] 𝑅 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝑓 ‘ 𝑦 ) = ( ( 𝑢 ∈ 𝐴 ↦ [ 𝑢 ] 𝑅 ) ‘ 𝑦 ) )
35 33 34 eqeq12d ⊢ ( ( 𝑓 = ( 𝑢 ∈ 𝐴 ↦ [ 𝑢 ] 𝑅 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( 𝑓 ‘ 𝑥 ) = ( 𝑓 ‘ 𝑦 ) ↔ ( ( 𝑢 ∈ 𝐴 ↦ [ 𝑢 ] 𝑅 ) ‘ 𝑥 ) = ( ( 𝑢 ∈ 𝐴 ↦ [ 𝑢 ] 𝑅 ) ‘ 𝑦 ) ) )
36 35 bibi2d ⊢ ( ( 𝑓 = ( 𝑢 ∈ 𝐴 ↦ [ 𝑢 ] 𝑅 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( 𝑥 𝑅 𝑦 ↔ ( 𝑓 ‘ 𝑥 ) = ( 𝑓 ‘ 𝑦 ) ) ↔ ( 𝑥 𝑅 𝑦 ↔ ( ( 𝑢 ∈ 𝐴 ↦ [ 𝑢 ] 𝑅 ) ‘ 𝑥 ) = ( ( 𝑢 ∈ 𝐴 ↦ [ 𝑢 ] 𝑅 ) ‘ 𝑦 ) ) ) )
37 36 2ralbidva ⊢ ( 𝑓 = ( 𝑢 ∈ 𝐴 ↦ [ 𝑢 ] 𝑅 ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ↔ ( 𝑓 ‘ 𝑥 ) = ( 𝑓 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ↔ ( ( 𝑢 ∈ 𝐴 ↦ [ 𝑢 ] 𝑅 ) ‘ 𝑥 ) = ( ( 𝑢 ∈ 𝐴 ↦ [ 𝑢 ] 𝑅 ) ‘ 𝑦 ) ) ) )
38 31 37 anbi12d ⊢ ( 𝑓 = ( 𝑢 ∈ 𝐴 ↦ [ 𝑢 ] 𝑅 ) → ( ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ↔ ( 𝑓 ‘ 𝑥 ) = ( 𝑓 ‘ 𝑦 ) ) ) ↔ ( ( 𝑢 ∈ 𝐴 ↦ [ 𝑢 ] 𝑅 ) Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ↔ ( ( 𝑢 ∈ 𝐴 ↦ [ 𝑢 ] 𝑅 ) ‘ 𝑥 ) = ( ( 𝑢 ∈ 𝐴 ↦ [ 𝑢 ] 𝑅 ) ‘ 𝑦 ) ) ) ) )
39 38 spcegv ⊢ ( ( 𝑢 ∈ 𝐴 ↦ [ 𝑢 ] 𝑅 ) ∈ V → ( ( ( 𝑢 ∈ 𝐴 ↦ [ 𝑢 ] 𝑅 ) Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ↔ ( ( 𝑢 ∈ 𝐴 ↦ [ 𝑢 ] 𝑅 ) ‘ 𝑥 ) = ( ( 𝑢 ∈ 𝐴 ↦ [ 𝑢 ] 𝑅 ) ‘ 𝑦 ) ) ) → ∃ 𝑓 ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ↔ ( 𝑓 ‘ 𝑥 ) = ( 𝑓 ‘ 𝑦 ) ) ) ) )
40 30 39 syl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑅 Er 𝐴 ) → ( ( ( 𝑢 ∈ 𝐴 ↦ [ 𝑢 ] 𝑅 ) Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ↔ ( ( 𝑢 ∈ 𝐴 ↦ [ 𝑢 ] 𝑅 ) ‘ 𝑥 ) = ( ( 𝑢 ∈ 𝐴 ↦ [ 𝑢 ] 𝑅 ) ‘ 𝑦 ) ) ) → ∃ 𝑓 ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ↔ ( 𝑓 ‘ 𝑥 ) = ( 𝑓 ‘ 𝑦 ) ) ) ) )
41 9 28 40 mp2and ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑅 Er 𝐴 ) → ∃ 𝑓 ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ↔ ( 𝑓 ‘ 𝑥 ) = ( 𝑓 ‘ 𝑦 ) ) ) )