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

Theorem coprprop 31715
Description: Composition of two pairs of ordered pairs with matching domain and range. (Contributed by Thierry Arnoux, 24-Sep-2023.)
Hypotheses
Ref Expression
brprop.a (𝜑𝐴𝑉)
brprop.b (𝜑𝐵𝑊)
brprop.c (𝜑𝐶𝑉)
brprop.d (𝜑𝐷𝑊)
mptprop.1 (𝜑𝐴𝐶)
coprprop.e (𝜑𝐸𝑋)
coprprop.f (𝜑𝐹𝑋)
coprprop.1 (𝜑𝐸𝐹)
Assertion
Ref Expression
coprprop (𝜑 → ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} ∘ {⟨𝐸, 𝐴⟩, ⟨𝐹, 𝐶⟩}) = {⟨𝐸, 𝐵⟩, ⟨𝐹, 𝐷⟩})

Proof of Theorem coprprop
StepHypRef Expression
1 coundir 6220 . . . 4 (({⟨𝐴, 𝐵⟩} ∪ {⟨𝐶, 𝐷⟩}) ∘ {⟨𝐸, 𝐴⟩}) = (({⟨𝐴, 𝐵⟩} ∘ {⟨𝐸, 𝐴⟩}) ∪ ({⟨𝐶, 𝐷⟩} ∘ {⟨𝐸, 𝐴⟩}))
2 brprop.a . . . . . . 7 (𝜑𝐴𝑉)
3 brprop.b . . . . . . 7 (𝜑𝐵𝑊)
4 coprprop.e . . . . . . 7 (𝜑𝐸𝑋)
52, 3, 4cosnop 31711 . . . . . 6 (𝜑 → ({⟨𝐴, 𝐵⟩} ∘ {⟨𝐸, 𝐴⟩}) = {⟨𝐸, 𝐵⟩})
6 brprop.d . . . . . . 7 (𝜑𝐷𝑊)
7 mptprop.1 . . . . . . . 8 (𝜑𝐴𝐶)
87necomd 2995 . . . . . . 7 (𝜑𝐶𝐴)
96, 4, 8cosnopne 31710 . . . . . 6 (𝜑 → ({⟨𝐶, 𝐷⟩} ∘ {⟨𝐸, 𝐴⟩}) = ∅)
105, 9uneq12d 4144 . . . . 5 (𝜑 → (({⟨𝐴, 𝐵⟩} ∘ {⟨𝐸, 𝐴⟩}) ∪ ({⟨𝐶, 𝐷⟩} ∘ {⟨𝐸, 𝐴⟩})) = ({⟨𝐸, 𝐵⟩} ∪ ∅))
11 un0 4370 . . . . 5 ({⟨𝐸, 𝐵⟩} ∪ ∅) = {⟨𝐸, 𝐵⟩}
1210, 11eqtrdi 2787 . . . 4 (𝜑 → (({⟨𝐴, 𝐵⟩} ∘ {⟨𝐸, 𝐴⟩}) ∪ ({⟨𝐶, 𝐷⟩} ∘ {⟨𝐸, 𝐴⟩})) = {⟨𝐸, 𝐵⟩})
131, 12eqtrid 2783 . . 3 (𝜑 → (({⟨𝐴, 𝐵⟩} ∪ {⟨𝐶, 𝐷⟩}) ∘ {⟨𝐸, 𝐴⟩}) = {⟨𝐸, 𝐵⟩})
14 coundir 6220 . . . 4 (({⟨𝐴, 𝐵⟩} ∪ {⟨𝐶, 𝐷⟩}) ∘ {⟨𝐹, 𝐶⟩}) = (({⟨𝐴, 𝐵⟩} ∘ {⟨𝐹, 𝐶⟩}) ∪ ({⟨𝐶, 𝐷⟩} ∘ {⟨𝐹, 𝐶⟩}))
15 coprprop.f . . . . . . 7 (𝜑𝐹𝑋)
163, 15, 7cosnopne 31710 . . . . . 6 (𝜑 → ({⟨𝐴, 𝐵⟩} ∘ {⟨𝐹, 𝐶⟩}) = ∅)
17 brprop.c . . . . . . 7 (𝜑𝐶𝑉)
1817, 6, 15cosnop 31711 . . . . . 6 (𝜑 → ({⟨𝐶, 𝐷⟩} ∘ {⟨𝐹, 𝐶⟩}) = {⟨𝐹, 𝐷⟩})
1916, 18uneq12d 4144 . . . . 5 (𝜑 → (({⟨𝐴, 𝐵⟩} ∘ {⟨𝐹, 𝐶⟩}) ∪ ({⟨𝐶, 𝐷⟩} ∘ {⟨𝐹, 𝐶⟩})) = (∅ ∪ {⟨𝐹, 𝐷⟩}))
20 0un 4372 . . . . 5 (∅ ∪ {⟨𝐹, 𝐷⟩}) = {⟨𝐹, 𝐷⟩}
2119, 20eqtrdi 2787 . . . 4 (𝜑 → (({⟨𝐴, 𝐵⟩} ∘ {⟨𝐹, 𝐶⟩}) ∪ ({⟨𝐶, 𝐷⟩} ∘ {⟨𝐹, 𝐶⟩})) = {⟨𝐹, 𝐷⟩})
2214, 21eqtrid 2783 . . 3 (𝜑 → (({⟨𝐴, 𝐵⟩} ∪ {⟨𝐶, 𝐷⟩}) ∘ {⟨𝐹, 𝐶⟩}) = {⟨𝐹, 𝐷⟩})
2313, 22uneq12d 4144 . 2 (𝜑 → ((({⟨𝐴, 𝐵⟩} ∪ {⟨𝐶, 𝐷⟩}) ∘ {⟨𝐸, 𝐴⟩}) ∪ (({⟨𝐴, 𝐵⟩} ∪ {⟨𝐶, 𝐷⟩}) ∘ {⟨𝐹, 𝐶⟩})) = ({⟨𝐸, 𝐵⟩} ∪ {⟨𝐹, 𝐷⟩}))
24 df-pr 4609 . . . 4 {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = ({⟨𝐴, 𝐵⟩} ∪ {⟨𝐶, 𝐷⟩})
25 df-pr 4609 . . . 4 {⟨𝐸, 𝐴⟩, ⟨𝐹, 𝐶⟩} = ({⟨𝐸, 𝐴⟩} ∪ {⟨𝐹, 𝐶⟩})
2624, 25coeq12i 5839 . . 3 ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} ∘ {⟨𝐸, 𝐴⟩, ⟨𝐹, 𝐶⟩}) = (({⟨𝐴, 𝐵⟩} ∪ {⟨𝐶, 𝐷⟩}) ∘ ({⟨𝐸, 𝐴⟩} ∪ {⟨𝐹, 𝐶⟩}))
27 coundi 6219 . . 3 (({⟨𝐴, 𝐵⟩} ∪ {⟨𝐶, 𝐷⟩}) ∘ ({⟨𝐸, 𝐴⟩} ∪ {⟨𝐹, 𝐶⟩})) = ((({⟨𝐴, 𝐵⟩} ∪ {⟨𝐶, 𝐷⟩}) ∘ {⟨𝐸, 𝐴⟩}) ∪ (({⟨𝐴, 𝐵⟩} ∪ {⟨𝐶, 𝐷⟩}) ∘ {⟨𝐹, 𝐶⟩}))
2826, 27eqtri 2759 . 2 ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} ∘ {⟨𝐸, 𝐴⟩, ⟨𝐹, 𝐶⟩}) = ((({⟨𝐴, 𝐵⟩} ∪ {⟨𝐶, 𝐷⟩}) ∘ {⟨𝐸, 𝐴⟩}) ∪ (({⟨𝐴, 𝐵⟩} ∪ {⟨𝐶, 𝐷⟩}) ∘ {⟨𝐹, 𝐶⟩}))
29 df-pr 4609 . 2 {⟨𝐸, 𝐵⟩, ⟨𝐹, 𝐷⟩} = ({⟨𝐸, 𝐵⟩} ∪ {⟨𝐹, 𝐷⟩})
3023, 28, 293eqtr4g 2796 1 (𝜑 → ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} ∘ {⟨𝐸, 𝐴⟩, ⟨𝐹, 𝐶⟩}) = {⟨𝐸, 𝐵⟩, ⟨𝐹, 𝐷⟩})
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1541  wcel 2106  wne 2939  cun 3926  c0 4302  {csn 4606  {cpr 4608  cop 4612  ccom 5657
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-sep 5276  ax-nul 5283  ax-pr 5404
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-reu 3365  df-rab 3419  df-v 3461  df-dif 3931  df-un 3933  df-in 3935  df-ss 3945  df-nul 4303  df-if 4507  df-sn 4607  df-pr 4609  df-op 4613  df-br 5126  df-opab 5188  df-mpt 5209  df-id 5551  df-xp 5659  df-rel 5660  df-cnv 5661  df-co 5662  df-dm 5663  df-rn 5664  df-res 5665  df-fun 6518  df-fn 6519  df-f 6520  df-f1 6521  df-fo 6522  df-f1o 6523
This theorem is referenced by:  cycpm2tr  32072
  Copyright terms: Public domain W3C validator