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

Theorem dom2lem 8853
Description: A mapping (first hypothesis) that is one-to-one (second hypothesis) implies its domain is dominated by its codomain. (Contributed by NM, 24-Jul-2004.)
Hypotheses
Ref Expression
dom2d.1 (𝜑 → (𝑥𝐴𝐶𝐵))
dom2d.2 (𝜑 → ((𝑥𝐴𝑦𝐴) → (𝐶 = 𝐷𝑥 = 𝑦)))
Assertion
Ref Expression
dom2lem (𝜑 → (𝑥𝐴𝐶):𝐴1-1𝐵)
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦   𝑦,𝐶   𝑥,𝐷   𝜑,𝑥,𝑦
Allowed substitution hints:   𝐶(𝑥)   𝐷(𝑦)

Proof of Theorem dom2lem
StepHypRef Expression
1 dom2d.1 . . . 4 (𝜑 → (𝑥𝐴𝐶𝐵))
21ralrimiv 3138 . . 3 (𝜑 → ∀𝑥𝐴 𝐶𝐵)
3 eqid 2736 . . . 4 (𝑥𝐴𝐶) = (𝑥𝐴𝐶)
43fmpt 7040 . . 3 (∀𝑥𝐴 𝐶𝐵 ↔ (𝑥𝐴𝐶):𝐴𝐵)
52, 4sylib 217 . 2 (𝜑 → (𝑥𝐴𝐶):𝐴𝐵)
61imp 407 . . . . . . 7 ((𝜑𝑥𝐴) → 𝐶𝐵)
73fvmpt2 6942 . . . . . . . 8 ((𝑥𝐴𝐶𝐵) → ((𝑥𝐴𝐶)‘𝑥) = 𝐶)
87adantll 711 . . . . . . 7 (((𝜑𝑥𝐴) ∧ 𝐶𝐵) → ((𝑥𝐴𝐶)‘𝑥) = 𝐶)
96, 8mpdan 684 . . . . . 6 ((𝜑𝑥𝐴) → ((𝑥𝐴𝐶)‘𝑥) = 𝐶)
109adantrr 714 . . . . 5 ((𝜑 ∧ (𝑥𝐴𝑦𝐴)) → ((𝑥𝐴𝐶)‘𝑥) = 𝐶)
11 nfv 1916 . . . . . . . 8 𝑥(𝜑𝑦𝐴)
12 nffvmpt1 6836 . . . . . . . . 9 𝑥((𝑥𝐴𝐶)‘𝑦)
1312nfeq1 2919 . . . . . . . 8 𝑥((𝑥𝐴𝐶)‘𝑦) = 𝐷
1411, 13nfim 1898 . . . . . . 7 𝑥((𝜑𝑦𝐴) → ((𝑥𝐴𝐶)‘𝑦) = 𝐷)
15 eleq1w 2819 . . . . . . . . . 10 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
1615anbi2d 629 . . . . . . . . 9 (𝑥 = 𝑦 → ((𝜑𝑥𝐴) ↔ (𝜑𝑦𝐴)))
1716imbi1d 341 . . . . . . . 8 (𝑥 = 𝑦 → (((𝜑𝑥𝐴) → ((𝑥𝐴𝐶)‘𝑥) = 𝐶) ↔ ((𝜑𝑦𝐴) → ((𝑥𝐴𝐶)‘𝑥) = 𝐶)))
1815anbi1d 630 . . . . . . . . . . . 12 (𝑥 = 𝑦 → ((𝑥𝐴𝑦𝐴) ↔ (𝑦𝐴𝑦𝐴)))
19 anidm 565 . . . . . . . . . . . 12 ((𝑦𝐴𝑦𝐴) ↔ 𝑦𝐴)
2018, 19bitrdi 286 . . . . . . . . . . 11 (𝑥 = 𝑦 → ((𝑥𝐴𝑦𝐴) ↔ 𝑦𝐴))
2120anbi2d 629 . . . . . . . . . 10 (𝑥 = 𝑦 → ((𝜑 ∧ (𝑥𝐴𝑦𝐴)) ↔ (𝜑𝑦𝐴)))
22 fveq2 6825 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → ((𝑥𝐴𝐶)‘𝑥) = ((𝑥𝐴𝐶)‘𝑦))
2322adantr 481 . . . . . . . . . . . 12 ((𝑥 = 𝑦 ∧ (𝜑 ∧ (𝑥𝐴𝑦𝐴))) → ((𝑥𝐴𝐶)‘𝑥) = ((𝑥𝐴𝐶)‘𝑦))
24 dom2d.2 . . . . . . . . . . . . . 14 (𝜑 → ((𝑥𝐴𝑦𝐴) → (𝐶 = 𝐷𝑥 = 𝑦)))
2524imp 407 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥𝐴𝑦𝐴)) → (𝐶 = 𝐷𝑥 = 𝑦))
2625biimparc 480 . . . . . . . . . . . 12 ((𝑥 = 𝑦 ∧ (𝜑 ∧ (𝑥𝐴𝑦𝐴))) → 𝐶 = 𝐷)
2723, 26eqeq12d 2752 . . . . . . . . . . 11 ((𝑥 = 𝑦 ∧ (𝜑 ∧ (𝑥𝐴𝑦𝐴))) → (((𝑥𝐴𝐶)‘𝑥) = 𝐶 ↔ ((𝑥𝐴𝐶)‘𝑦) = 𝐷))
2827ex 413 . . . . . . . . . 10 (𝑥 = 𝑦 → ((𝜑 ∧ (𝑥𝐴𝑦𝐴)) → (((𝑥𝐴𝐶)‘𝑥) = 𝐶 ↔ ((𝑥𝐴𝐶)‘𝑦) = 𝐷)))
2921, 28sylbird 259 . . . . . . . . 9 (𝑥 = 𝑦 → ((𝜑𝑦𝐴) → (((𝑥𝐴𝐶)‘𝑥) = 𝐶 ↔ ((𝑥𝐴𝐶)‘𝑦) = 𝐷)))
3029pm5.74d 272 . . . . . . . 8 (𝑥 = 𝑦 → (((𝜑𝑦𝐴) → ((𝑥𝐴𝐶)‘𝑥) = 𝐶) ↔ ((𝜑𝑦𝐴) → ((𝑥𝐴𝐶)‘𝑦) = 𝐷)))
3117, 30bitrd 278 . . . . . . 7 (𝑥 = 𝑦 → (((𝜑𝑥𝐴) → ((𝑥𝐴𝐶)‘𝑥) = 𝐶) ↔ ((𝜑𝑦𝐴) → ((𝑥𝐴𝐶)‘𝑦) = 𝐷)))
3214, 31, 9chvarfv 2232 . . . . . 6 ((𝜑𝑦𝐴) → ((𝑥𝐴𝐶)‘𝑦) = 𝐷)
3332adantrl 713 . . . . 5 ((𝜑 ∧ (𝑥𝐴𝑦𝐴)) → ((𝑥𝐴𝐶)‘𝑦) = 𝐷)
3410, 33eqeq12d 2752 . . . 4 ((𝜑 ∧ (𝑥𝐴𝑦𝐴)) → (((𝑥𝐴𝐶)‘𝑥) = ((𝑥𝐴𝐶)‘𝑦) ↔ 𝐶 = 𝐷))
3525biimpd 228 . . . 4 ((𝜑 ∧ (𝑥𝐴𝑦𝐴)) → (𝐶 = 𝐷𝑥 = 𝑦))
3634, 35sylbid 239 . . 3 ((𝜑 ∧ (𝑥𝐴𝑦𝐴)) → (((𝑥𝐴𝐶)‘𝑥) = ((𝑥𝐴𝐶)‘𝑦) → 𝑥 = 𝑦))
3736ralrimivva 3193 . 2 (𝜑 → ∀𝑥𝐴𝑦𝐴 (((𝑥𝐴𝐶)‘𝑥) = ((𝑥𝐴𝐶)‘𝑦) → 𝑥 = 𝑦))
38 nfmpt1 5200 . . 3 𝑥(𝑥𝐴𝐶)
39 nfcv 2904 . . 3 𝑦(𝑥𝐴𝐶)
4038, 39dff13f 7185 . 2 ((𝑥𝐴𝐶):𝐴1-1𝐵 ↔ ((𝑥𝐴𝐶):𝐴𝐵 ∧ ∀𝑥𝐴𝑦𝐴 (((𝑥𝐴𝐶)‘𝑥) = ((𝑥𝐴𝐶)‘𝑦) → 𝑥 = 𝑦)))
415, 37, 40sylanbrc 583 1 (𝜑 → (𝑥𝐴𝐶):𝐴1-1𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1540  wcel 2105  wral 3061  cmpt 5175  wf 6475  1-1wf1 6476  cfv 6479
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-sep 5243  ax-nul 5250  ax-pr 5372
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3404  df-v 3443  df-sbc 3728  df-csb 3844  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4270  df-if 4474  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4853  df-br 5093  df-opab 5155  df-mpt 5176  df-id 5518  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633  df-iota 6431  df-fun 6481  df-fn 6482  df-f 6483  df-f1 6484  df-fv 6487
This theorem is referenced by:  dom2d  8854  dom3d  8855  ixpfi2  9215  infxpenc2lem1  9876  dfac12lem2  10001  4sqlem11  16753  odf1o1  19273  odf1o2  19274  dis2ndc  22717  hauspwpwf1  23244  itg1addlem4  24969  itg1addlem4OLD  24970  basellem3  26338  fsumvma  26467  dchrisum0fno1  26765
  Copyright terms: Public domain W3C validator