Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  tgjustr Structured version   Visualization version   GIF version

Theorem tgjustr 25825
 Description: Given any equivalence relation 𝑅, one can define a function 𝑓 such that all elements of an equivalence classe of 𝑅 have the same image by 𝑓. (Contributed by Thierry Arnoux, 25-Jan-2023.)
Assertion
Ref Expression
tgjustr ((𝐴𝑉𝑅 Er 𝐴) → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝑓𝑥) = (𝑓𝑦))))
Distinct variable groups:   𝐴,𝑓,𝑥,𝑦   𝑅,𝑓,𝑥,𝑦   𝑥,𝑉,𝑦
Allowed substitution hint:   𝑉(𝑓)

Proof of Theorem tgjustr
Dummy variable 𝑢 is distinct from all other variables.
StepHypRef Expression
1 erex 8050 . . . . . . 7 (𝑅 Er 𝐴 → (𝐴𝑉𝑅 ∈ V))
21impcom 398 . . . . . 6 ((𝐴𝑉𝑅 Er 𝐴) → 𝑅 ∈ V)
3 ecexg 8030 . . . . . 6 (𝑅 ∈ V → [𝑢]𝑅 ∈ V)
42, 3syl 17 . . . . 5 ((𝐴𝑉𝑅 Er 𝐴) → [𝑢]𝑅 ∈ V)
54adantr 474 . . . 4 (((𝐴𝑉𝑅 Er 𝐴) ∧ 𝑢𝐴) → [𝑢]𝑅 ∈ V)
65ralrimiva 3148 . . 3 ((𝐴𝑉𝑅 Er 𝐴) → ∀𝑢𝐴 [𝑢]𝑅 ∈ V)
7 eqid 2778 . . . 4 (𝑢𝐴 ↦ [𝑢]𝑅) = (𝑢𝐴 ↦ [𝑢]𝑅)
87fnmpt 6266 . . 3 (∀𝑢𝐴 [𝑢]𝑅 ∈ V → (𝑢𝐴 ↦ [𝑢]𝑅) Fn 𝐴)
96, 8syl 17 . 2 ((𝐴𝑉𝑅 Er 𝐴) → (𝑢𝐴 ↦ [𝑢]𝑅) Fn 𝐴)
10 simpllr 766 . . . . . 6 ((((𝐴𝑉𝑅 Er 𝐴) ∧ 𝑥𝐴) ∧ 𝑦𝐴) → 𝑅 Er 𝐴)
11 simpr 479 . . . . . . 7 (((𝐴𝑉𝑅 Er 𝐴) ∧ 𝑥𝐴) → 𝑥𝐴)
1211adantr 474 . . . . . 6 ((((𝐴𝑉𝑅 Er 𝐴) ∧ 𝑥𝐴) ∧ 𝑦𝐴) → 𝑥𝐴)
1310, 12erth 8073 . . . . 5 ((((𝐴𝑉𝑅 Er 𝐴) ∧ 𝑥𝐴) ∧ 𝑦𝐴) → (𝑥𝑅𝑦 ↔ [𝑥]𝑅 = [𝑦]𝑅))
14 eceq1 8064 . . . . . . . 8 (𝑢 = 𝑥 → [𝑢]𝑅 = [𝑥]𝑅)
152adantr 474 . . . . . . . . 9 (((𝐴𝑉𝑅 Er 𝐴) ∧ 𝑥𝐴) → 𝑅 ∈ V)
16 ecelqsg 8085 . . . . . . . . 9 ((𝑅 ∈ V ∧ 𝑥𝐴) → [𝑥]𝑅 ∈ (𝐴 / 𝑅))
1715, 11, 16syl2anc 579 . . . . . . . 8 (((𝐴𝑉𝑅 Er 𝐴) ∧ 𝑥𝐴) → [𝑥]𝑅 ∈ (𝐴 / 𝑅))
187, 14, 11, 17fvmptd3 6564 . . . . . . 7 (((𝐴𝑉𝑅 Er 𝐴) ∧ 𝑥𝐴) → ((𝑢𝐴 ↦ [𝑢]𝑅)‘𝑥) = [𝑥]𝑅)
1918adantr 474 . . . . . 6 ((((𝐴𝑉𝑅 Er 𝐴) ∧ 𝑥𝐴) ∧ 𝑦𝐴) → ((𝑢𝐴 ↦ [𝑢]𝑅)‘𝑥) = [𝑥]𝑅)
20 eceq1 8064 . . . . . . . 8 (𝑢 = 𝑦 → [𝑢]𝑅 = [𝑦]𝑅)
21 simpr 479 . . . . . . . 8 (((𝐴𝑉𝑅 Er 𝐴) ∧ 𝑦𝐴) → 𝑦𝐴)
222adantr 474 . . . . . . . . 9 (((𝐴𝑉𝑅 Er 𝐴) ∧ 𝑦𝐴) → 𝑅 ∈ V)
23 ecelqsg 8085 . . . . . . . . 9 ((𝑅 ∈ V ∧ 𝑦𝐴) → [𝑦]𝑅 ∈ (𝐴 / 𝑅))
2422, 21, 23syl2anc 579 . . . . . . . 8 (((𝐴𝑉𝑅 Er 𝐴) ∧ 𝑦𝐴) → [𝑦]𝑅 ∈ (𝐴 / 𝑅))
257, 20, 21, 24fvmptd3 6564 . . . . . . 7 (((𝐴𝑉𝑅 Er 𝐴) ∧ 𝑦𝐴) → ((𝑢𝐴 ↦ [𝑢]𝑅)‘𝑦) = [𝑦]𝑅)
2625adantlr 705 . . . . . 6 ((((𝐴𝑉𝑅 Er 𝐴) ∧ 𝑥𝐴) ∧ 𝑦𝐴) → ((𝑢𝐴 ↦ [𝑢]𝑅)‘𝑦) = [𝑦]𝑅)
2719, 26eqeq12d 2793 . . . . 5 ((((𝐴𝑉𝑅 Er 𝐴) ∧ 𝑥𝐴) ∧ 𝑦𝐴) → (((𝑢𝐴 ↦ [𝑢]𝑅)‘𝑥) = ((𝑢𝐴 ↦ [𝑢]𝑅)‘𝑦) ↔ [𝑥]𝑅 = [𝑦]𝑅))
2813, 27bitr4d 274 . . . 4 ((((𝐴𝑉𝑅 Er 𝐴) ∧ 𝑥𝐴) ∧ 𝑦𝐴) → (𝑥𝑅𝑦 ↔ ((𝑢𝐴 ↦ [𝑢]𝑅)‘𝑥) = ((𝑢𝐴 ↦ [𝑢]𝑅)‘𝑦)))
2928ralrimiva 3148 . . 3 (((𝐴𝑉𝑅 Er 𝐴) ∧ 𝑥𝐴) → ∀𝑦𝐴 (𝑥𝑅𝑦 ↔ ((𝑢𝐴 ↦ [𝑢]𝑅)‘𝑥) = ((𝑢𝐴 ↦ [𝑢]𝑅)‘𝑦)))
3029ralrimiva 3148 . 2 ((𝐴𝑉𝑅 Er 𝐴) → ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ ((𝑢𝐴 ↦ [𝑢]𝑅)‘𝑥) = ((𝑢𝐴 ↦ [𝑢]𝑅)‘𝑦)))
31 mptexg 6756 . . . 4 (𝐴𝑉 → (𝑢𝐴 ↦ [𝑢]𝑅) ∈ V)
3231adantr 474 . . 3 ((𝐴𝑉𝑅 Er 𝐴) → (𝑢𝐴 ↦ [𝑢]𝑅) ∈ V)
33 fneq1 6224 . . . . 5 (𝑓 = (𝑢𝐴 ↦ [𝑢]𝑅) → (𝑓 Fn 𝐴 ↔ (𝑢𝐴 ↦ [𝑢]𝑅) Fn 𝐴))
34 simpl 476 . . . . . . . . 9 ((𝑓 = (𝑢𝐴 ↦ [𝑢]𝑅) ∧ (𝑥𝐴𝑦𝐴)) → 𝑓 = (𝑢𝐴 ↦ [𝑢]𝑅))
35 eqidd 2779 . . . . . . . . 9 ((𝑓 = (𝑢𝐴 ↦ [𝑢]𝑅) ∧ (𝑥𝐴𝑦𝐴)) → 𝑥 = 𝑥)
3634, 35fveq12d 6453 . . . . . . . 8 ((𝑓 = (𝑢𝐴 ↦ [𝑢]𝑅) ∧ (𝑥𝐴𝑦𝐴)) → (𝑓𝑥) = ((𝑢𝐴 ↦ [𝑢]𝑅)‘𝑥))
37 eqidd 2779 . . . . . . . . 9 ((𝑓 = (𝑢𝐴 ↦ [𝑢]𝑅) ∧ (𝑥𝐴𝑦𝐴)) → 𝑦 = 𝑦)
3834, 37fveq12d 6453 . . . . . . . 8 ((𝑓 = (𝑢𝐴 ↦ [𝑢]𝑅) ∧ (𝑥𝐴𝑦𝐴)) → (𝑓𝑦) = ((𝑢𝐴 ↦ [𝑢]𝑅)‘𝑦))
3936, 38eqeq12d 2793 . . . . . . 7 ((𝑓 = (𝑢𝐴 ↦ [𝑢]𝑅) ∧ (𝑥𝐴𝑦𝐴)) → ((𝑓𝑥) = (𝑓𝑦) ↔ ((𝑢𝐴 ↦ [𝑢]𝑅)‘𝑥) = ((𝑢𝐴 ↦ [𝑢]𝑅)‘𝑦)))
4039bibi2d 334 . . . . . 6 ((𝑓 = (𝑢𝐴 ↦ [𝑢]𝑅) ∧ (𝑥𝐴𝑦𝐴)) → ((𝑥𝑅𝑦 ↔ (𝑓𝑥) = (𝑓𝑦)) ↔ (𝑥𝑅𝑦 ↔ ((𝑢𝐴 ↦ [𝑢]𝑅)‘𝑥) = ((𝑢𝐴 ↦ [𝑢]𝑅)‘𝑦))))
41402ralbidva 3170 . . . . 5 (𝑓 = (𝑢𝐴 ↦ [𝑢]𝑅) → (∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝑓𝑥) = (𝑓𝑦)) ↔ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ ((𝑢𝐴 ↦ [𝑢]𝑅)‘𝑥) = ((𝑢𝐴 ↦ [𝑢]𝑅)‘𝑦))))
4233, 41anbi12d 624 . . . 4 (𝑓 = (𝑢𝐴 ↦ [𝑢]𝑅) → ((𝑓 Fn 𝐴 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝑓𝑥) = (𝑓𝑦))) ↔ ((𝑢𝐴 ↦ [𝑢]𝑅) Fn 𝐴 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ ((𝑢𝐴 ↦ [𝑢]𝑅)‘𝑥) = ((𝑢𝐴 ↦ [𝑢]𝑅)‘𝑦)))))
4342spcegv 3496 . . 3 ((𝑢𝐴 ↦ [𝑢]𝑅) ∈ V → (((𝑢𝐴 ↦ [𝑢]𝑅) Fn 𝐴 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ ((𝑢𝐴 ↦ [𝑢]𝑅)‘𝑥) = ((𝑢𝐴 ↦ [𝑢]𝑅)‘𝑦))) → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝑓𝑥) = (𝑓𝑦)))))
4432, 43syl 17 . 2 ((𝐴𝑉𝑅 Er 𝐴) → (((𝑢𝐴 ↦ [𝑢]𝑅) Fn 𝐴 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ ((𝑢𝐴 ↦ [𝑢]𝑅)‘𝑥) = ((𝑢𝐴 ↦ [𝑢]𝑅)‘𝑦))) → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝑓𝑥) = (𝑓𝑦)))))
459, 30, 44mp2and 689 1 ((𝐴𝑉𝑅 Er 𝐴) → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝑓𝑥) = (𝑓𝑦))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386   = wceq 1601  ∃wex 1823   ∈ wcel 2107  ∀wral 3090  Vcvv 3398   class class class wbr 4886   ↦ cmpt 4965   Fn wfn 6130  ‘cfv 6135   Er wer 8023  [cec 8024   / cqs 8025 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-rep 5006  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226 This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-ral 3095  df-rex 3096  df-reu 3097  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4672  df-iun 4755  df-br 4887  df-opab 4949  df-mpt 4966  df-id 5261  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-er 8026  df-ec 8028  df-qs 8032 This theorem is referenced by:  tgjustc2  25827
 Copyright terms: Public domain W3C validator