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

Theorem f1oprg 6651
 Description: An unordered pair of ordered pairs with different elements is a one-to-one onto function, analogous to f1oprswap 6650. (Contributed by Alexander van der Vekens, 14-Aug-2017.)
Assertion
Ref Expression
f1oprg (((𝐴𝑉𝐵𝑊) ∧ (𝐶𝑋𝐷𝑌)) → ((𝐴𝐶𝐵𝐷) → {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩}:{𝐴, 𝐶}–1-1-onto→{𝐵, 𝐷}))

Proof of Theorem f1oprg
StepHypRef Expression
1 f1osng 6647 . . . . 5 ((𝐴𝑉𝐵𝑊) → {⟨𝐴, 𝐵⟩}:{𝐴}–1-1-onto→{𝐵})
21ad2antrr 725 . . . 4 ((((𝐴𝑉𝐵𝑊) ∧ (𝐶𝑋𝐷𝑌)) ∧ (𝐴𝐶𝐵𝐷)) → {⟨𝐴, 𝐵⟩}:{𝐴}–1-1-onto→{𝐵})
3 f1osng 6647 . . . . 5 ((𝐶𝑋𝐷𝑌) → {⟨𝐶, 𝐷⟩}:{𝐶}–1-1-onto→{𝐷})
43ad2antlr 726 . . . 4 ((((𝐴𝑉𝐵𝑊) ∧ (𝐶𝑋𝐷𝑌)) ∧ (𝐴𝐶𝐵𝐷)) → {⟨𝐶, 𝐷⟩}:{𝐶}–1-1-onto→{𝐷})
5 disjsn2 4608 . . . . 5 (𝐴𝐶 → ({𝐴} ∩ {𝐶}) = ∅)
65ad2antrl 727 . . . 4 ((((𝐴𝑉𝐵𝑊) ∧ (𝐶𝑋𝐷𝑌)) ∧ (𝐴𝐶𝐵𝐷)) → ({𝐴} ∩ {𝐶}) = ∅)
7 disjsn2 4608 . . . . 5 (𝐵𝐷 → ({𝐵} ∩ {𝐷}) = ∅)
87ad2antll 728 . . . 4 ((((𝐴𝑉𝐵𝑊) ∧ (𝐶𝑋𝐷𝑌)) ∧ (𝐴𝐶𝐵𝐷)) → ({𝐵} ∩ {𝐷}) = ∅)
9 f1oun 6626 . . . 4 ((({⟨𝐴, 𝐵⟩}:{𝐴}–1-1-onto→{𝐵} ∧ {⟨𝐶, 𝐷⟩}:{𝐶}–1-1-onto→{𝐷}) ∧ (({𝐴} ∩ {𝐶}) = ∅ ∧ ({𝐵} ∩ {𝐷}) = ∅)) → ({⟨𝐴, 𝐵⟩} ∪ {⟨𝐶, 𝐷⟩}):({𝐴} ∪ {𝐶})–1-1-onto→({𝐵} ∪ {𝐷}))
102, 4, 6, 8, 9syl22anc 837 . . 3 ((((𝐴𝑉𝐵𝑊) ∧ (𝐶𝑋𝐷𝑌)) ∧ (𝐴𝐶𝐵𝐷)) → ({⟨𝐴, 𝐵⟩} ∪ {⟨𝐶, 𝐷⟩}):({𝐴} ∪ {𝐶})–1-1-onto→({𝐵} ∪ {𝐷}))
11 df-pr 4528 . . . . . 6 {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = ({⟨𝐴, 𝐵⟩} ∪ {⟨𝐶, 𝐷⟩})
1211eqcomi 2767 . . . . 5 ({⟨𝐴, 𝐵⟩} ∪ {⟨𝐶, 𝐷⟩}) = {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩}
1312a1i 11 . . . 4 ((((𝐴𝑉𝐵𝑊) ∧ (𝐶𝑋𝐷𝑌)) ∧ (𝐴𝐶𝐵𝐷)) → ({⟨𝐴, 𝐵⟩} ∪ {⟨𝐶, 𝐷⟩}) = {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩})
14 df-pr 4528 . . . . . 6 {𝐴, 𝐶} = ({𝐴} ∪ {𝐶})
1514eqcomi 2767 . . . . 5 ({𝐴} ∪ {𝐶}) = {𝐴, 𝐶}
1615a1i 11 . . . 4 ((((𝐴𝑉𝐵𝑊) ∧ (𝐶𝑋𝐷𝑌)) ∧ (𝐴𝐶𝐵𝐷)) → ({𝐴} ∪ {𝐶}) = {𝐴, 𝐶})
17 df-pr 4528 . . . . . 6 {𝐵, 𝐷} = ({𝐵} ∪ {𝐷})
1817eqcomi 2767 . . . . 5 ({𝐵} ∪ {𝐷}) = {𝐵, 𝐷}
1918a1i 11 . . . 4 ((((𝐴𝑉𝐵𝑊) ∧ (𝐶𝑋𝐷𝑌)) ∧ (𝐴𝐶𝐵𝐷)) → ({𝐵} ∪ {𝐷}) = {𝐵, 𝐷})
2013, 16, 19f1oeq123d 6601 . . 3 ((((𝐴𝑉𝐵𝑊) ∧ (𝐶𝑋𝐷𝑌)) ∧ (𝐴𝐶𝐵𝐷)) → (({⟨𝐴, 𝐵⟩} ∪ {⟨𝐶, 𝐷⟩}):({𝐴} ∪ {𝐶})–1-1-onto→({𝐵} ∪ {𝐷}) ↔ {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩}:{𝐴, 𝐶}–1-1-onto→{𝐵, 𝐷}))
2110, 20mpbid 235 . 2 ((((𝐴𝑉𝐵𝑊) ∧ (𝐶𝑋𝐷𝑌)) ∧ (𝐴𝐶𝐵𝐷)) → {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩}:{𝐴, 𝐶}–1-1-onto→{𝐵, 𝐷})
2221ex 416 1 (((𝐴𝑉𝐵𝑊) ∧ (𝐶𝑋𝐷𝑌)) → ((𝐴𝐶𝐵𝐷) → {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩}:{𝐴, 𝐶}–1-1-onto→{𝐵, 𝐷}))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2111   ≠ wne 2951   ∪ cun 3858   ∩ cin 3859  ∅c0 4227  {csn 4525  {cpr 4527  ⟨cop 4531  –1-1-onto→wf1o 6339 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5173  ax-nul 5180  ax-pr 5302 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-ral 3075  df-rex 3076  df-rab 3079  df-v 3411  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-nul 4228  df-if 4424  df-sn 4526  df-pr 4528  df-op 4532  df-br 5037  df-opab 5099  df-id 5434  df-xp 5534  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-rn 5539  df-fun 6342  df-fn 6343  df-f 6344  df-f1 6345  df-fo 6346  df-f1o 6347 This theorem is referenced by:  f1prex  7038  s2f1o  14338  f1oun2prg  14339  symg2bas  18601  s2f1  30755  poimirlem9  35380  poimirlem15  35386
 Copyright terms: Public domain W3C validator