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

Theorem f1ompt 7131
Description: Express bijection for a mapping operation. (Contributed by Mario Carneiro, 30-May-2015.) (Revised by Mario Carneiro, 4-Dec-2016.)
Hypothesis
Ref Expression
fmpt.1 𝐹 = (𝑥𝐴𝐶)
Assertion
Ref Expression
f1ompt (𝐹:𝐴1-1-onto𝐵 ↔ (∀𝑥𝐴 𝐶𝐵 ∧ ∀𝑦𝐵 ∃!𝑥𝐴 𝑦 = 𝐶))
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦   𝑦,𝐶   𝑦,𝐹
Allowed substitution hints:   𝐶(𝑥)   𝐹(𝑥)

Proof of Theorem f1ompt
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 ffn 6737 . . . . 5 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
2 dff1o4 6857 . . . . . 6 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹 Fn 𝐴𝐹 Fn 𝐵))
32baib 535 . . . . 5 (𝐹 Fn 𝐴 → (𝐹:𝐴1-1-onto𝐵𝐹 Fn 𝐵))
41, 3syl 17 . . . 4 (𝐹:𝐴𝐵 → (𝐹:𝐴1-1-onto𝐵𝐹 Fn 𝐵))
5 fnres 6696 . . . . . 6 ((𝐹𝐵) Fn 𝐵 ↔ ∀𝑦𝐵 ∃!𝑧 𝑦𝐹𝑧)
6 nfcv 2903 . . . . . . . . . 10 𝑥𝑧
7 fmpt.1 . . . . . . . . . . 11 𝐹 = (𝑥𝐴𝐶)
8 nfmpt1 5256 . . . . . . . . . . 11 𝑥(𝑥𝐴𝐶)
97, 8nfcxfr 2901 . . . . . . . . . 10 𝑥𝐹
10 nfcv 2903 . . . . . . . . . 10 𝑥𝑦
116, 9, 10nfbr 5195 . . . . . . . . 9 𝑥 𝑧𝐹𝑦
12 nfv 1912 . . . . . . . . 9 𝑧(𝑥𝐴𝑦 = 𝐶)
13 breq1 5151 . . . . . . . . . 10 (𝑧 = 𝑥 → (𝑧𝐹𝑦𝑥𝐹𝑦))
14 df-mpt 5232 . . . . . . . . . . . . 13 (𝑥𝐴𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐶)}
157, 14eqtri 2763 . . . . . . . . . . . 12 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐶)}
1615breqi 5154 . . . . . . . . . . 11 (𝑥𝐹𝑦𝑥{⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐶)}𝑦)
17 df-br 5149 . . . . . . . . . . . 12 (𝑥{⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐶)}𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐶)})
18 opabidw 5534 . . . . . . . . . . . 12 (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐶)} ↔ (𝑥𝐴𝑦 = 𝐶))
1917, 18bitri 275 . . . . . . . . . . 11 (𝑥{⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐶)}𝑦 ↔ (𝑥𝐴𝑦 = 𝐶))
2016, 19bitri 275 . . . . . . . . . 10 (𝑥𝐹𝑦 ↔ (𝑥𝐴𝑦 = 𝐶))
2113, 20bitrdi 287 . . . . . . . . 9 (𝑧 = 𝑥 → (𝑧𝐹𝑦 ↔ (𝑥𝐴𝑦 = 𝐶)))
2211, 12, 21cbveuw 2604 . . . . . . . 8 (∃!𝑧 𝑧𝐹𝑦 ↔ ∃!𝑥(𝑥𝐴𝑦 = 𝐶))
23 vex 3482 . . . . . . . . . 10 𝑦 ∈ V
24 vex 3482 . . . . . . . . . 10 𝑧 ∈ V
2523, 24brcnv 5896 . . . . . . . . 9 (𝑦𝐹𝑧𝑧𝐹𝑦)
2625eubii 2583 . . . . . . . 8 (∃!𝑧 𝑦𝐹𝑧 ↔ ∃!𝑧 𝑧𝐹𝑦)
27 df-reu 3379 . . . . . . . 8 (∃!𝑥𝐴 𝑦 = 𝐶 ↔ ∃!𝑥(𝑥𝐴𝑦 = 𝐶))
2822, 26, 273bitr4i 303 . . . . . . 7 (∃!𝑧 𝑦𝐹𝑧 ↔ ∃!𝑥𝐴 𝑦 = 𝐶)
2928ralbii 3091 . . . . . 6 (∀𝑦𝐵 ∃!𝑧 𝑦𝐹𝑧 ↔ ∀𝑦𝐵 ∃!𝑥𝐴 𝑦 = 𝐶)
305, 29bitri 275 . . . . 5 ((𝐹𝐵) Fn 𝐵 ↔ ∀𝑦𝐵 ∃!𝑥𝐴 𝑦 = 𝐶)
31 relcnv 6125 . . . . . . 7 Rel 𝐹
32 df-rn 5700 . . . . . . . 8 ran 𝐹 = dom 𝐹
33 frn 6744 . . . . . . . 8 (𝐹:𝐴𝐵 → ran 𝐹𝐵)
3432, 33eqsstrrid 4045 . . . . . . 7 (𝐹:𝐴𝐵 → dom 𝐹𝐵)
35 relssres 6042 . . . . . . 7 ((Rel 𝐹 ∧ dom 𝐹𝐵) → (𝐹𝐵) = 𝐹)
3631, 34, 35sylancr 587 . . . . . 6 (𝐹:𝐴𝐵 → (𝐹𝐵) = 𝐹)
3736fneq1d 6662 . . . . 5 (𝐹:𝐴𝐵 → ((𝐹𝐵) Fn 𝐵𝐹 Fn 𝐵))
3830, 37bitr3id 285 . . . 4 (𝐹:𝐴𝐵 → (∀𝑦𝐵 ∃!𝑥𝐴 𝑦 = 𝐶𝐹 Fn 𝐵))
394, 38bitr4d 282 . . 3 (𝐹:𝐴𝐵 → (𝐹:𝐴1-1-onto𝐵 ↔ ∀𝑦𝐵 ∃!𝑥𝐴 𝑦 = 𝐶))
4039pm5.32i 574 . 2 ((𝐹:𝐴𝐵𝐹:𝐴1-1-onto𝐵) ↔ (𝐹:𝐴𝐵 ∧ ∀𝑦𝐵 ∃!𝑥𝐴 𝑦 = 𝐶))
41 f1of 6849 . . 3 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴𝐵)
4241pm4.71ri 560 . 2 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹:𝐴𝐵𝐹:𝐴1-1-onto𝐵))
437fmpt 7130 . . 3 (∀𝑥𝐴 𝐶𝐵𝐹:𝐴𝐵)
4443anbi1i 624 . 2 ((∀𝑥𝐴 𝐶𝐵 ∧ ∀𝑦𝐵 ∃!𝑥𝐴 𝑦 = 𝐶) ↔ (𝐹:𝐴𝐵 ∧ ∀𝑦𝐵 ∃!𝑥𝐴 𝑦 = 𝐶))
4540, 42, 443bitr4i 303 1 (𝐹:𝐴1-1-onto𝐵 ↔ (∀𝑥𝐴 𝐶𝐵 ∧ ∀𝑦𝐵 ∃!𝑥𝐴 𝑦 = 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395   = wceq 1537  wcel 2106  ∃!weu 2566  wral 3059  ∃!wreu 3376  wss 3963  cop 4637   class class class wbr 5148  {copab 5210  cmpt 5231  ccnv 5688  dom cdm 5689  ran crn 5690  cres 5691  Rel wrel 5694   Fn wfn 6558  wf 6559  1-1-ontowf1o 6562
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ral 3060  df-rex 3069  df-reu 3379  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570
This theorem is referenced by:  oaf1o  8600  xpf1o  9178  icoshftf1o  13511  fprodser  15982  dfod2  19597  gsummptf1o  19996  nbusgrf1o0  29401  cusgrfilem2  29489  numclwlk2lem2f1o  30408  f1mptrn  32652  ccatws1f1o  32921  gsummptfsf1o  33040  xrmulc1cn  33891  poimirlem4  37611  poimirlem16  37623  poimirlem17  37624  poimirlem19  37626  poimirlem20  37627  isuspgrim0lem  47809  isuspgrim0  47810  isuspgrimlem  47812
  Copyright terms: Public domain W3C validator