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

Theorem fmptcof 7130
Description: Version of fmptco 7129 where 𝜑 needn't be distinct from 𝑥. (Contributed by NM, 27-Dec-2014.)
Hypotheses
Ref Expression
fmptcof.1 (𝜑 → ∀𝑥𝐴 𝑅𝐵)
fmptcof.2 (𝜑𝐹 = (𝑥𝐴𝑅))
fmptcof.3 (𝜑𝐺 = (𝑦𝐵𝑆))
fmptcof.4 (𝑦 = 𝑅𝑆 = 𝑇)
Assertion
Ref Expression
fmptcof (𝜑 → (𝐺𝐹) = (𝑥𝐴𝑇))
Distinct variable groups:   𝑥,𝑦,𝐵   𝑦,𝑅   𝑥,𝑆   𝑥,𝐴   𝑦,𝑇
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐴(𝑦)   𝑅(𝑥)   𝑆(𝑦)   𝑇(𝑥)   𝐹(𝑥,𝑦)   𝐺(𝑥,𝑦)

Proof of Theorem fmptcof
Dummy variables 𝑤 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fmptcof.1 . . . . 5 (𝜑 → ∀𝑥𝐴 𝑅𝐵)
2 nfcsb1v 3918 . . . . . . 7 𝑥𝑧 / 𝑥𝑅
32nfel1 2919 . . . . . 6 𝑥𝑧 / 𝑥𝑅𝐵
4 csbeq1a 3907 . . . . . . 7 (𝑥 = 𝑧𝑅 = 𝑧 / 𝑥𝑅)
54eleq1d 2818 . . . . . 6 (𝑥 = 𝑧 → (𝑅𝐵𝑧 / 𝑥𝑅𝐵))
63, 5rspc 3600 . . . . 5 (𝑧𝐴 → (∀𝑥𝐴 𝑅𝐵𝑧 / 𝑥𝑅𝐵))
71, 6mpan9 507 . . . 4 ((𝜑𝑧𝐴) → 𝑧 / 𝑥𝑅𝐵)
8 fmptcof.2 . . . . 5 (𝜑𝐹 = (𝑥𝐴𝑅))
9 nfcv 2903 . . . . . 6 𝑧𝑅
109, 2, 4cbvmpt 5259 . . . . 5 (𝑥𝐴𝑅) = (𝑧𝐴𝑧 / 𝑥𝑅)
118, 10eqtrdi 2788 . . . 4 (𝜑𝐹 = (𝑧𝐴𝑧 / 𝑥𝑅))
12 fmptcof.3 . . . . 5 (𝜑𝐺 = (𝑦𝐵𝑆))
13 nfcv 2903 . . . . . 6 𝑤𝑆
14 nfcsb1v 3918 . . . . . 6 𝑦𝑤 / 𝑦𝑆
15 csbeq1a 3907 . . . . . 6 (𝑦 = 𝑤𝑆 = 𝑤 / 𝑦𝑆)
1613, 14, 15cbvmpt 5259 . . . . 5 (𝑦𝐵𝑆) = (𝑤𝐵𝑤 / 𝑦𝑆)
1712, 16eqtrdi 2788 . . . 4 (𝜑𝐺 = (𝑤𝐵𝑤 / 𝑦𝑆))
18 csbeq1 3896 . . . 4 (𝑤 = 𝑧 / 𝑥𝑅𝑤 / 𝑦𝑆 = 𝑧 / 𝑥𝑅 / 𝑦𝑆)
197, 11, 17, 18fmptco 7129 . . 3 (𝜑 → (𝐺𝐹) = (𝑧𝐴𝑧 / 𝑥𝑅 / 𝑦𝑆))
20 nfcv 2903 . . . 4 𝑧𝑅 / 𝑦𝑆
21 nfcv 2903 . . . . 5 𝑥𝑆
222, 21nfcsbw 3920 . . . 4 𝑥𝑧 / 𝑥𝑅 / 𝑦𝑆
234csbeq1d 3897 . . . 4 (𝑥 = 𝑧𝑅 / 𝑦𝑆 = 𝑧 / 𝑥𝑅 / 𝑦𝑆)
2420, 22, 23cbvmpt 5259 . . 3 (𝑥𝐴𝑅 / 𝑦𝑆) = (𝑧𝐴𝑧 / 𝑥𝑅 / 𝑦𝑆)
2519, 24eqtr4di 2790 . 2 (𝜑 → (𝐺𝐹) = (𝑥𝐴𝑅 / 𝑦𝑆))
26 eqid 2732 . . . 4 𝐴 = 𝐴
27 nfcvd 2904 . . . . . 6 (𝑅𝐵𝑦𝑇)
28 fmptcof.4 . . . . . 6 (𝑦 = 𝑅𝑆 = 𝑇)
2927, 28csbiegf 3927 . . . . 5 (𝑅𝐵𝑅 / 𝑦𝑆 = 𝑇)
3029ralimi 3083 . . . 4 (∀𝑥𝐴 𝑅𝐵 → ∀𝑥𝐴 𝑅 / 𝑦𝑆 = 𝑇)
31 mpteq12 5240 . . . 4 ((𝐴 = 𝐴 ∧ ∀𝑥𝐴 𝑅 / 𝑦𝑆 = 𝑇) → (𝑥𝐴𝑅 / 𝑦𝑆) = (𝑥𝐴𝑇))
3226, 30, 31sylancr 587 . . 3 (∀𝑥𝐴 𝑅𝐵 → (𝑥𝐴𝑅 / 𝑦𝑆) = (𝑥𝐴𝑇))
331, 32syl 17 . 2 (𝜑 → (𝑥𝐴𝑅 / 𝑦𝑆) = (𝑥𝐴𝑇))
3425, 33eqtrd 2772 1 (𝜑 → (𝐺𝐹) = (𝑥𝐴𝑇))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1541  wcel 2106  wral 3061  csb 3893  cmpt 5231  ccom 5680
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-fv 6551
This theorem is referenced by:  fmptcos  7131  yonedalem3b  18236  gsumcom2  19884  evl1sca  22073  cnmptk1  23405  cnmpt1k  23406  cnmptkk  23407  cncfcompt2  24648  cncfmpt1f  24654  copco  24758  pcoass  24764  sincn  26180  coscn  26181  lgseisenlem3  27104  fcomptf  32138  eulerpartgbij  33657
  Copyright terms: Public domain W3C validator