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

Theorem f1ompt 6575
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 6225 . . . . 5 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
2 dff1o4 6332 . . . . . 6 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹 Fn 𝐴𝐹 Fn 𝐵))
32baib 531 . . . . 5 (𝐹 Fn 𝐴 → (𝐹:𝐴1-1-onto𝐵𝐹 Fn 𝐵))
41, 3syl 17 . . . 4 (𝐹:𝐴𝐵 → (𝐹:𝐴1-1-onto𝐵𝐹 Fn 𝐵))
5 fnres 6187 . . . . . 6 ((𝐹𝐵) Fn 𝐵 ↔ ∀𝑦𝐵 ∃!𝑧 𝑦𝐹𝑧)
6 nfcv 2907 . . . . . . . . . 10 𝑥𝑧
7 fmpt.1 . . . . . . . . . . 11 𝐹 = (𝑥𝐴𝐶)
8 nfmpt1 4908 . . . . . . . . . . 11 𝑥(𝑥𝐴𝐶)
97, 8nfcxfr 2905 . . . . . . . . . 10 𝑥𝐹
10 nfcv 2907 . . . . . . . . . 10 𝑥𝑦
116, 9, 10nfbr 4858 . . . . . . . . 9 𝑥 𝑧𝐹𝑦
12 nfv 2009 . . . . . . . . 9 𝑧(𝑥𝐴𝑦 = 𝐶)
13 breq1 4814 . . . . . . . . . 10 (𝑧 = 𝑥 → (𝑧𝐹𝑦𝑥𝐹𝑦))
14 df-mpt 4891 . . . . . . . . . . . . 13 (𝑥𝐴𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐶)}
157, 14eqtri 2787 . . . . . . . . . . . 12 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐶)}
1615breqi 4817 . . . . . . . . . . 11 (𝑥𝐹𝑦𝑥{⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐶)}𝑦)
17 df-br 4812 . . . . . . . . . . . 12 (𝑥{⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐶)}𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐶)})
18 opabid 5145 . . . . . . . . . . . 12 (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐶)} ↔ (𝑥𝐴𝑦 = 𝐶))
1917, 18bitri 266 . . . . . . . . . . 11 (𝑥{⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐶)}𝑦 ↔ (𝑥𝐴𝑦 = 𝐶))
2016, 19bitri 266 . . . . . . . . . 10 (𝑥𝐹𝑦 ↔ (𝑥𝐴𝑦 = 𝐶))
2113, 20syl6bb 278 . . . . . . . . 9 (𝑧 = 𝑥 → (𝑧𝐹𝑦 ↔ (𝑥𝐴𝑦 = 𝐶)))
2211, 12, 21cbveu 2626 . . . . . . . 8 (∃!𝑧 𝑧𝐹𝑦 ↔ ∃!𝑥(𝑥𝐴𝑦 = 𝐶))
23 vex 3353 . . . . . . . . . 10 𝑦 ∈ V
24 vex 3353 . . . . . . . . . 10 𝑧 ∈ V
2523, 24brcnv 5475 . . . . . . . . 9 (𝑦𝐹𝑧𝑧𝐹𝑦)
2625eubii 2584 . . . . . . . 8 (∃!𝑧 𝑦𝐹𝑧 ↔ ∃!𝑧 𝑧𝐹𝑦)
27 df-reu 3062 . . . . . . . 8 (∃!𝑥𝐴 𝑦 = 𝐶 ↔ ∃!𝑥(𝑥𝐴𝑦 = 𝐶))
2822, 26, 273bitr4i 294 . . . . . . 7 (∃!𝑧 𝑦𝐹𝑧 ↔ ∃!𝑥𝐴 𝑦 = 𝐶)
2928ralbii 3127 . . . . . 6 (∀𝑦𝐵 ∃!𝑧 𝑦𝐹𝑧 ↔ ∀𝑦𝐵 ∃!𝑥𝐴 𝑦 = 𝐶)
305, 29bitri 266 . . . . 5 ((𝐹𝐵) Fn 𝐵 ↔ ∀𝑦𝐵 ∃!𝑥𝐴 𝑦 = 𝐶)
31 relcnv 5687 . . . . . . 7 Rel 𝐹
32 df-rn 5290 . . . . . . . 8 ran 𝐹 = dom 𝐹
33 frn 6231 . . . . . . . 8 (𝐹:𝐴𝐵 → ran 𝐹𝐵)
3432, 33syl5eqssr 3812 . . . . . . 7 (𝐹:𝐴𝐵 → dom 𝐹𝐵)
35 relssres 5615 . . . . . . 7 ((Rel 𝐹 ∧ dom 𝐹𝐵) → (𝐹𝐵) = 𝐹)
3631, 34, 35sylancr 581 . . . . . 6 (𝐹:𝐴𝐵 → (𝐹𝐵) = 𝐹)
3736fneq1d 6161 . . . . 5 (𝐹:𝐴𝐵 → ((𝐹𝐵) Fn 𝐵𝐹 Fn 𝐵))
3830, 37syl5bbr 276 . . . 4 (𝐹:𝐴𝐵 → (∀𝑦𝐵 ∃!𝑥𝐴 𝑦 = 𝐶𝐹 Fn 𝐵))
394, 38bitr4d 273 . . 3 (𝐹:𝐴𝐵 → (𝐹:𝐴1-1-onto𝐵 ↔ ∀𝑦𝐵 ∃!𝑥𝐴 𝑦 = 𝐶))
4039pm5.32i 570 . 2 ((𝐹:𝐴𝐵𝐹:𝐴1-1-onto𝐵) ↔ (𝐹:𝐴𝐵 ∧ ∀𝑦𝐵 ∃!𝑥𝐴 𝑦 = 𝐶))
41 f1of 6324 . . 3 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴𝐵)
4241pm4.71ri 556 . 2 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹:𝐴𝐵𝐹:𝐴1-1-onto𝐵))
437fmpt 6574 . . 3 (∀𝑥𝐴 𝐶𝐵𝐹:𝐴𝐵)
4443anbi1i 617 . 2 ((∀𝑥𝐴 𝐶𝐵 ∧ ∀𝑦𝐵 ∃!𝑥𝐴 𝑦 = 𝐶) ↔ (𝐹:𝐴𝐵 ∧ ∀𝑦𝐵 ∃!𝑥𝐴 𝑦 = 𝐶))
4540, 42, 443bitr4i 294 1 (𝐹:𝐴1-1-onto𝐵 ↔ (∀𝑥𝐴 𝐶𝐵 ∧ ∀𝑦𝐵 ∃!𝑥𝐴 𝑦 = 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wb 197  wa 384   = wceq 1652  wcel 2155  ∃!weu 2581  wral 3055  ∃!wreu 3057  wss 3734  cop 4342   class class class wbr 4811  {copab 4873  cmpt 4890  ccnv 5278  dom cdm 5279  ran crn 5280  cres 5281  Rel wrel 5284   Fn wfn 6065  wf 6066  1-1-ontowf1o 6069
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4943  ax-nul 4951  ax-pr 5064
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-ral 3060  df-rex 3061  df-reu 3062  df-rab 3064  df-v 3352  df-sbc 3599  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-nul 4082  df-if 4246  df-sn 4337  df-pr 4339  df-op 4343  df-uni 4597  df-br 4812  df-opab 4874  df-mpt 4891  df-id 5187  df-xp 5285  df-rel 5286  df-cnv 5287  df-co 5288  df-dm 5289  df-rn 5290  df-res 5291  df-ima 5292  df-iota 6033  df-fun 6072  df-fn 6073  df-f 6074  df-f1 6075  df-fo 6076  df-f1o 6077  df-fv 6078
This theorem is referenced by:  oaf1o  7852  xpf1o  8333  icoshftf1o  12505  fprodser  14976  dfod2  18259  gsummptf1o  18642  nbusgrf1o0  26564  cusgrfilem2  26657  numclwlk2lem2f1o  27704  numclwlk2lem2f1oOLD  27707  numclwlk2lem2f1oOLDOLD  27715  f1mptrn  29906  xrmulc1cn  30444  poimirlem4  33858  poimirlem16  33870  poimirlem17  33871  poimirlem19  33873  poimirlem20  33874
  Copyright terms: Public domain W3C validator