Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fcoinver Structured version   Visualization version   GIF version

Theorem fcoinver 31528
Description: Build an equivalence relation from a function. Two values are equivalent if they have the same image by the function. See also fcoinvbr 31529. (Contributed by Thierry Arnoux, 3-Jan-2020.)
Assertion
Ref Expression
fcoinver (𝐹 Fn 𝑋 β†’ (◑𝐹 ∘ 𝐹) Er 𝑋)

Proof of Theorem fcoinver
StepHypRef Expression
1 relco 6061 . . 3 Rel (◑𝐹 ∘ 𝐹)
21a1i 11 . 2 (𝐹 Fn 𝑋 β†’ Rel (◑𝐹 ∘ 𝐹))
3 dmco 6207 . . 3 dom (◑𝐹 ∘ 𝐹) = (◑𝐹 β€œ dom ◑𝐹)
4 df-rn 5645 . . . . 5 ran 𝐹 = dom ◑𝐹
54imaeq2i 6012 . . . 4 (◑𝐹 β€œ ran 𝐹) = (◑𝐹 β€œ dom ◑𝐹)
6 cnvimarndm 6035 . . . . 5 (◑𝐹 β€œ ran 𝐹) = dom 𝐹
7 fndm 6606 . . . . 5 (𝐹 Fn 𝑋 β†’ dom 𝐹 = 𝑋)
86, 7eqtrid 2789 . . . 4 (𝐹 Fn 𝑋 β†’ (◑𝐹 β€œ ran 𝐹) = 𝑋)
95, 8eqtr3id 2791 . . 3 (𝐹 Fn 𝑋 β†’ (◑𝐹 β€œ dom ◑𝐹) = 𝑋)
103, 9eqtrid 2789 . 2 (𝐹 Fn 𝑋 β†’ dom (◑𝐹 ∘ 𝐹) = 𝑋)
11 cnvco 5842 . . . . 5 β—‘(◑𝐹 ∘ 𝐹) = (◑𝐹 ∘ ◑◑𝐹)
12 cnvcnvss 6147 . . . . . 6 ◑◑𝐹 βŠ† 𝐹
13 coss2 5813 . . . . . 6 (◑◑𝐹 βŠ† 𝐹 β†’ (◑𝐹 ∘ ◑◑𝐹) βŠ† (◑𝐹 ∘ 𝐹))
1412, 13ax-mp 5 . . . . 5 (◑𝐹 ∘ ◑◑𝐹) βŠ† (◑𝐹 ∘ 𝐹)
1511, 14eqsstri 3979 . . . 4 β—‘(◑𝐹 ∘ 𝐹) βŠ† (◑𝐹 ∘ 𝐹)
1615a1i 11 . . 3 (𝐹 Fn 𝑋 β†’ β—‘(◑𝐹 ∘ 𝐹) βŠ† (◑𝐹 ∘ 𝐹))
17 coass 6218 . . . . 5 ((◑𝐹 ∘ 𝐹) ∘ (◑𝐹 ∘ 𝐹)) = (◑𝐹 ∘ (𝐹 ∘ (◑𝐹 ∘ 𝐹)))
18 coass 6218 . . . . . . 7 ((𝐹 ∘ ◑𝐹) ∘ 𝐹) = (𝐹 ∘ (◑𝐹 ∘ 𝐹))
19 fnfun 6603 . . . . . . . . . 10 (𝐹 Fn 𝑋 β†’ Fun 𝐹)
20 funcocnv2 6810 . . . . . . . . . 10 (Fun 𝐹 β†’ (𝐹 ∘ ◑𝐹) = ( I β†Ύ ran 𝐹))
2119, 20syl 17 . . . . . . . . 9 (𝐹 Fn 𝑋 β†’ (𝐹 ∘ ◑𝐹) = ( I β†Ύ ran 𝐹))
2221coeq1d 5818 . . . . . . . 8 (𝐹 Fn 𝑋 β†’ ((𝐹 ∘ ◑𝐹) ∘ 𝐹) = (( I β†Ύ ran 𝐹) ∘ 𝐹))
23 dffn3 6682 . . . . . . . . 9 (𝐹 Fn 𝑋 ↔ 𝐹:π‘‹βŸΆran 𝐹)
24 fcoi2 6718 . . . . . . . . 9 (𝐹:π‘‹βŸΆran 𝐹 β†’ (( I β†Ύ ran 𝐹) ∘ 𝐹) = 𝐹)
2523, 24sylbi 216 . . . . . . . 8 (𝐹 Fn 𝑋 β†’ (( I β†Ύ ran 𝐹) ∘ 𝐹) = 𝐹)
2622, 25eqtrd 2777 . . . . . . 7 (𝐹 Fn 𝑋 β†’ ((𝐹 ∘ ◑𝐹) ∘ 𝐹) = 𝐹)
2718, 26eqtr3id 2791 . . . . . 6 (𝐹 Fn 𝑋 β†’ (𝐹 ∘ (◑𝐹 ∘ 𝐹)) = 𝐹)
2827coeq2d 5819 . . . . 5 (𝐹 Fn 𝑋 β†’ (◑𝐹 ∘ (𝐹 ∘ (◑𝐹 ∘ 𝐹))) = (◑𝐹 ∘ 𝐹))
2917, 28eqtrid 2789 . . . 4 (𝐹 Fn 𝑋 β†’ ((◑𝐹 ∘ 𝐹) ∘ (◑𝐹 ∘ 𝐹)) = (◑𝐹 ∘ 𝐹))
30 ssid 3967 . . . 4 (◑𝐹 ∘ 𝐹) βŠ† (◑𝐹 ∘ 𝐹)
3129, 30eqsstrdi 3999 . . 3 (𝐹 Fn 𝑋 β†’ ((◑𝐹 ∘ 𝐹) ∘ (◑𝐹 ∘ 𝐹)) βŠ† (◑𝐹 ∘ 𝐹))
3216, 31unssd 4147 . 2 (𝐹 Fn 𝑋 β†’ (β—‘(◑𝐹 ∘ 𝐹) βˆͺ ((◑𝐹 ∘ 𝐹) ∘ (◑𝐹 ∘ 𝐹))) βŠ† (◑𝐹 ∘ 𝐹))
33 df-er 8649 . 2 ((◑𝐹 ∘ 𝐹) Er 𝑋 ↔ (Rel (◑𝐹 ∘ 𝐹) ∧ dom (◑𝐹 ∘ 𝐹) = 𝑋 ∧ (β—‘(◑𝐹 ∘ 𝐹) βˆͺ ((◑𝐹 ∘ 𝐹) ∘ (◑𝐹 ∘ 𝐹))) βŠ† (◑𝐹 ∘ 𝐹)))
342, 10, 32, 33syl3anbrc 1344 1 (𝐹 Fn 𝑋 β†’ (◑𝐹 ∘ 𝐹) Er 𝑋)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   = wceq 1542   βˆͺ cun 3909   βŠ† wss 3911   I cid 5531  β—‘ccnv 5633  dom cdm 5634  ran crn 5635   β†Ύ cres 5636   β€œ cima 5637   ∘ ccom 5638  Rel wrel 5639  Fun wfun 6491   Fn wfn 6492  βŸΆwf 6493   Er wer 8646
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5257  ax-nul 5264  ax-pr 5385
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-ral 3066  df-rex 3075  df-rab 3409  df-v 3448  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-br 5107  df-opab 5169  df-id 5532  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-fun 6499  df-fn 6500  df-f 6501  df-er 8649
This theorem is referenced by:  qtophaus  32420
  Copyright terms: Public domain W3C validator