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

Theorem f1ocnv2d 6846
Description: Describe an implicit one-to-one onto function. (Contributed by Mario Carneiro, 30-Apr-2015.)
Hypotheses
Ref Expression
f1od.1 𝐹 = (𝑥𝐴𝐶)
f1o2d.2 ((𝜑𝑥𝐴) → 𝐶𝐵)
f1o2d.3 ((𝜑𝑦𝐵) → 𝐷𝐴)
f1o2d.4 ((𝜑 ∧ (𝑥𝐴𝑦𝐵)) → (𝑥 = 𝐷𝑦 = 𝐶))
Assertion
Ref Expression
f1ocnv2d (𝜑 → (𝐹:𝐴1-1-onto𝐵𝐹 = (𝑦𝐵𝐷)))
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦   𝑦,𝐶   𝑥,𝐷   𝜑,𝑥,𝑦
Allowed substitution hints:   𝐶(𝑥)   𝐷(𝑦)   𝐹(𝑥,𝑦)

Proof of Theorem f1ocnv2d
StepHypRef Expression
1 f1od.1 . 2 𝐹 = (𝑥𝐴𝐶)
2 f1o2d.2 . 2 ((𝜑𝑥𝐴) → 𝐶𝐵)
3 f1o2d.3 . 2 ((𝜑𝑦𝐵) → 𝐷𝐴)
4 eleq1a 2693 . . . . . 6 (𝐶𝐵 → (𝑦 = 𝐶𝑦𝐵))
52, 4syl 17 . . . . 5 ((𝜑𝑥𝐴) → (𝑦 = 𝐶𝑦𝐵))
65impr 648 . . . 4 ((𝜑 ∧ (𝑥𝐴𝑦 = 𝐶)) → 𝑦𝐵)
7 f1o2d.4 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐴𝑦𝐵)) → (𝑥 = 𝐷𝑦 = 𝐶))
87biimpar 502 . . . . . . 7 (((𝜑 ∧ (𝑥𝐴𝑦𝐵)) ∧ 𝑦 = 𝐶) → 𝑥 = 𝐷)
98exp42 638 . . . . . 6 (𝜑 → (𝑥𝐴 → (𝑦𝐵 → (𝑦 = 𝐶𝑥 = 𝐷))))
109com34 91 . . . . 5 (𝜑 → (𝑥𝐴 → (𝑦 = 𝐶 → (𝑦𝐵𝑥 = 𝐷))))
1110imp32 449 . . . 4 ((𝜑 ∧ (𝑥𝐴𝑦 = 𝐶)) → (𝑦𝐵𝑥 = 𝐷))
126, 11jcai 558 . . 3 ((𝜑 ∧ (𝑥𝐴𝑦 = 𝐶)) → (𝑦𝐵𝑥 = 𝐷))
13 eleq1a 2693 . . . . . 6 (𝐷𝐴 → (𝑥 = 𝐷𝑥𝐴))
143, 13syl 17 . . . . 5 ((𝜑𝑦𝐵) → (𝑥 = 𝐷𝑥𝐴))
1514impr 648 . . . 4 ((𝜑 ∧ (𝑦𝐵𝑥 = 𝐷)) → 𝑥𝐴)
167biimpa 501 . . . . . . . 8 (((𝜑 ∧ (𝑥𝐴𝑦𝐵)) ∧ 𝑥 = 𝐷) → 𝑦 = 𝐶)
1716exp42 638 . . . . . . 7 (𝜑 → (𝑥𝐴 → (𝑦𝐵 → (𝑥 = 𝐷𝑦 = 𝐶))))
1817com23 86 . . . . . 6 (𝜑 → (𝑦𝐵 → (𝑥𝐴 → (𝑥 = 𝐷𝑦 = 𝐶))))
1918com34 91 . . . . 5 (𝜑 → (𝑦𝐵 → (𝑥 = 𝐷 → (𝑥𝐴𝑦 = 𝐶))))
2019imp32 449 . . . 4 ((𝜑 ∧ (𝑦𝐵𝑥 = 𝐷)) → (𝑥𝐴𝑦 = 𝐶))
2115, 20jcai 558 . . 3 ((𝜑 ∧ (𝑦𝐵𝑥 = 𝐷)) → (𝑥𝐴𝑦 = 𝐶))
2212, 21impbida 876 . 2 (𝜑 → ((𝑥𝐴𝑦 = 𝐶) ↔ (𝑦𝐵𝑥 = 𝐷)))
231, 2, 3, 22f1ocnvd 6844 1 (𝜑 → (𝐹:𝐴1-1-onto𝐵𝐹 = (𝑦𝐵𝐷)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1480  wcel 1987  cmpt 4678  ccnv 5078  1-1-ontowf1o 5851
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4746  ax-nul 4754  ax-pr 4872
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rab 2916  df-v 3191  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-nul 3897  df-if 4064  df-sn 4154  df-pr 4156  df-op 4160  df-br 4619  df-opab 4679  df-mpt 4680  df-id 4994  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859
This theorem is referenced by:  f1o2d  6847  negf1o  10412  negiso  10955  iccf1o  12266  bitsf1ocnv  15101  grpinvcnv  17415  grplactcnv  17450  issrngd  18793  opncldf1  20811  txhmeo  21529  ptuncnv  21533  icopnfcnv  22664  iccpnfcnv  22666  xrge0iifcnv  29785  rfovcnvf1od  37815
  Copyright terms: Public domain W3C validator