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

Theorem dom2lem 8987
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 3145 . . 3 (𝜑 → ∀𝑥𝐴 𝐶𝐵)
3 eqid 2732 . . . 4 (𝑥𝐴𝐶) = (𝑥𝐴𝐶)
43fmpt 7109 . . 3 (∀𝑥𝐴 𝐶𝐵 ↔ (𝑥𝐴𝐶):𝐴𝐵)
52, 4sylib 217 . 2 (𝜑 → (𝑥𝐴𝐶):𝐴𝐵)
61imp 407 . . . . . . 7 ((𝜑𝑥𝐴) → 𝐶𝐵)
73fvmpt2 7009 . . . . . . . 8 ((𝑥𝐴𝐶𝐵) → ((𝑥𝐴𝐶)‘𝑥) = 𝐶)
87adantll 712 . . . . . . 7 (((𝜑𝑥𝐴) ∧ 𝐶𝐵) → ((𝑥𝐴𝐶)‘𝑥) = 𝐶)
96, 8mpdan 685 . . . . . 6 ((𝜑𝑥𝐴) → ((𝑥𝐴𝐶)‘𝑥) = 𝐶)
109adantrr 715 . . . . 5 ((𝜑 ∧ (𝑥𝐴𝑦𝐴)) → ((𝑥𝐴𝐶)‘𝑥) = 𝐶)
11 nfv 1917 . . . . . . . 8 𝑥(𝜑𝑦𝐴)
12 nffvmpt1 6902 . . . . . . . . 9 𝑥((𝑥𝐴𝐶)‘𝑦)
1312nfeq1 2918 . . . . . . . 8 𝑥((𝑥𝐴𝐶)‘𝑦) = 𝐷
1411, 13nfim 1899 . . . . . . 7 𝑥((𝜑𝑦𝐴) → ((𝑥𝐴𝐶)‘𝑦) = 𝐷)
15 eleq1w 2816 . . . . . . . . . 10 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
1615anbi2d 629 . . . . . . . . 9 (𝑥 = 𝑦 → ((𝜑𝑥𝐴) ↔ (𝜑𝑦𝐴)))
1716imbi1d 341 . . . . . . . 8 (𝑥 = 𝑦 → (((𝜑𝑥𝐴) → ((𝑥𝐴𝐶)‘𝑥) = 𝐶) ↔ ((𝜑𝑦𝐴) → ((𝑥𝐴𝐶)‘𝑥) = 𝐶)))
1815anbi1d 630 . . . . . . . . . . . 12 (𝑥 = 𝑦 → ((𝑥𝐴𝑦𝐴) ↔ (𝑦𝐴𝑦𝐴)))
19 anidm 565 . . . . . . . . . . . 12 ((𝑦𝐴𝑦𝐴) ↔ 𝑦𝐴)
2018, 19bitrdi 286 . . . . . . . . . . 11 (𝑥 = 𝑦 → ((𝑥𝐴𝑦𝐴) ↔ 𝑦𝐴))
2120anbi2d 629 . . . . . . . . . 10 (𝑥 = 𝑦 → ((𝜑 ∧ (𝑥𝐴𝑦𝐴)) ↔ (𝜑𝑦𝐴)))
22 fveq2 6891 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → ((𝑥𝐴𝐶)‘𝑥) = ((𝑥𝐴𝐶)‘𝑦))
2322adantr 481 . . . . . . . . . . . 12 ((𝑥 = 𝑦 ∧ (𝜑 ∧ (𝑥𝐴𝑦𝐴))) → ((𝑥𝐴𝐶)‘𝑥) = ((𝑥𝐴𝐶)‘𝑦))
24 dom2d.2 . . . . . . . . . . . . . 14 (𝜑 → ((𝑥𝐴𝑦𝐴) → (𝐶 = 𝐷𝑥 = 𝑦)))
2524imp 407 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥𝐴𝑦𝐴)) → (𝐶 = 𝐷𝑥 = 𝑦))
2625biimparc 480 . . . . . . . . . . . 12 ((𝑥 = 𝑦 ∧ (𝜑 ∧ (𝑥𝐴𝑦𝐴))) → 𝐶 = 𝐷)
2723, 26eqeq12d 2748 . . . . . . . . . . 11 ((𝑥 = 𝑦 ∧ (𝜑 ∧ (𝑥𝐴𝑦𝐴))) → (((𝑥𝐴𝐶)‘𝑥) = 𝐶 ↔ ((𝑥𝐴𝐶)‘𝑦) = 𝐷))
2827ex 413 . . . . . . . . . 10 (𝑥 = 𝑦 → ((𝜑 ∧ (𝑥𝐴𝑦𝐴)) → (((𝑥𝐴𝐶)‘𝑥) = 𝐶 ↔ ((𝑥𝐴𝐶)‘𝑦) = 𝐷)))
2921, 28sylbird 259 . . . . . . . . 9 (𝑥 = 𝑦 → ((𝜑𝑦𝐴) → (((𝑥𝐴𝐶)‘𝑥) = 𝐶 ↔ ((𝑥𝐴𝐶)‘𝑦) = 𝐷)))
3029pm5.74d 272 . . . . . . . 8 (𝑥 = 𝑦 → (((𝜑𝑦𝐴) → ((𝑥𝐴𝐶)‘𝑥) = 𝐶) ↔ ((𝜑𝑦𝐴) → ((𝑥𝐴𝐶)‘𝑦) = 𝐷)))
3117, 30bitrd 278 . . . . . . 7 (𝑥 = 𝑦 → (((𝜑𝑥𝐴) → ((𝑥𝐴𝐶)‘𝑥) = 𝐶) ↔ ((𝜑𝑦𝐴) → ((𝑥𝐴𝐶)‘𝑦) = 𝐷)))
3214, 31, 9chvarfv 2233 . . . . . 6 ((𝜑𝑦𝐴) → ((𝑥𝐴𝐶)‘𝑦) = 𝐷)
3332adantrl 714 . . . . 5 ((𝜑 ∧ (𝑥𝐴𝑦𝐴)) → ((𝑥𝐴𝐶)‘𝑦) = 𝐷)
3410, 33eqeq12d 2748 . . . 4 ((𝜑 ∧ (𝑥𝐴𝑦𝐴)) → (((𝑥𝐴𝐶)‘𝑥) = ((𝑥𝐴𝐶)‘𝑦) ↔ 𝐶 = 𝐷))
3525biimpd 228 . . . 4 ((𝜑 ∧ (𝑥𝐴𝑦𝐴)) → (𝐶 = 𝐷𝑥 = 𝑦))
3634, 35sylbid 239 . . 3 ((𝜑 ∧ (𝑥𝐴𝑦𝐴)) → (((𝑥𝐴𝐶)‘𝑥) = ((𝑥𝐴𝐶)‘𝑦) → 𝑥 = 𝑦))
3736ralrimivva 3200 . 2 (𝜑 → ∀𝑥𝐴𝑦𝐴 (((𝑥𝐴𝐶)‘𝑥) = ((𝑥𝐴𝐶)‘𝑦) → 𝑥 = 𝑦))
38 nfmpt1 5256 . . 3 𝑥(𝑥𝐴𝐶)
39 nfcv 2903 . . 3 𝑦(𝑥𝐴𝐶)
4038, 39dff13f 7254 . 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 1541  wcel 2106  wral 3061  cmpt 5231  wf 6539  1-1wf1 6540  cfv 6543
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fv 6551
This theorem is referenced by:  dom2d  8988  dom3d  8989  ixpfi2  9349  infxpenc2lem1  10013  dfac12lem2  10138  4sqlem11  16887  odf1o1  19439  odf1o2  19440  dis2ndc  22963  hauspwpwf1  23490  itg1addlem4  25215  itg1addlem4OLD  25216  basellem3  26584  fsumvma  26713  dchrisum0fno1  27011
  Copyright terms: Public domain W3C validator