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

Theorem ofrfval2 7694
Description: The function relation acting on maps. (Contributed by Mario Carneiro, 20-Jul-2014.)
Hypotheses
Ref Expression
offval2.1 (𝜑𝐴𝑉)
offval2.2 ((𝜑𝑥𝐴) → 𝐵𝑊)
offval2.3 ((𝜑𝑥𝐴) → 𝐶𝑋)
offval2.4 (𝜑𝐹 = (𝑥𝐴𝐵))
offval2.5 (𝜑𝐺 = (𝑥𝐴𝐶))
Assertion
Ref Expression
ofrfval2 (𝜑 → (𝐹r 𝑅𝐺 ↔ ∀𝑥𝐴 𝐵𝑅𝐶))
Distinct variable groups:   𝑥,𝐴   𝜑,𝑥   𝑥,𝑅
Allowed substitution hints:   𝐵(𝑥)   𝐶(𝑥)   𝐹(𝑥)   𝐺(𝑥)   𝑉(𝑥)   𝑊(𝑥)   𝑋(𝑥)

Proof of Theorem ofrfval2
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 offval2.2 . . . . . 6 ((𝜑𝑥𝐴) → 𝐵𝑊)
21ralrimiva 3145 . . . . 5 (𝜑 → ∀𝑥𝐴 𝐵𝑊)
3 eqid 2731 . . . . . 6 (𝑥𝐴𝐵) = (𝑥𝐴𝐵)
43fnmpt 6690 . . . . 5 (∀𝑥𝐴 𝐵𝑊 → (𝑥𝐴𝐵) Fn 𝐴)
52, 4syl 17 . . . 4 (𝜑 → (𝑥𝐴𝐵) Fn 𝐴)
6 offval2.4 . . . . 5 (𝜑𝐹 = (𝑥𝐴𝐵))
76fneq1d 6642 . . . 4 (𝜑 → (𝐹 Fn 𝐴 ↔ (𝑥𝐴𝐵) Fn 𝐴))
85, 7mpbird 257 . . 3 (𝜑𝐹 Fn 𝐴)
9 offval2.3 . . . . . 6 ((𝜑𝑥𝐴) → 𝐶𝑋)
109ralrimiva 3145 . . . . 5 (𝜑 → ∀𝑥𝐴 𝐶𝑋)
11 eqid 2731 . . . . . 6 (𝑥𝐴𝐶) = (𝑥𝐴𝐶)
1211fnmpt 6690 . . . . 5 (∀𝑥𝐴 𝐶𝑋 → (𝑥𝐴𝐶) Fn 𝐴)
1310, 12syl 17 . . . 4 (𝜑 → (𝑥𝐴𝐶) Fn 𝐴)
14 offval2.5 . . . . 5 (𝜑𝐺 = (𝑥𝐴𝐶))
1514fneq1d 6642 . . . 4 (𝜑 → (𝐺 Fn 𝐴 ↔ (𝑥𝐴𝐶) Fn 𝐴))
1613, 15mpbird 257 . . 3 (𝜑𝐺 Fn 𝐴)
17 offval2.1 . . 3 (𝜑𝐴𝑉)
18 inidm 4218 . . 3 (𝐴𝐴) = 𝐴
196adantr 480 . . . 4 ((𝜑𝑦𝐴) → 𝐹 = (𝑥𝐴𝐵))
2019fveq1d 6893 . . 3 ((𝜑𝑦𝐴) → (𝐹𝑦) = ((𝑥𝐴𝐵)‘𝑦))
2114adantr 480 . . . 4 ((𝜑𝑦𝐴) → 𝐺 = (𝑥𝐴𝐶))
2221fveq1d 6893 . . 3 ((𝜑𝑦𝐴) → (𝐺𝑦) = ((𝑥𝐴𝐶)‘𝑦))
238, 16, 17, 17, 18, 20, 22ofrfval 7683 . 2 (𝜑 → (𝐹r 𝑅𝐺 ↔ ∀𝑦𝐴 ((𝑥𝐴𝐵)‘𝑦)𝑅((𝑥𝐴𝐶)‘𝑦)))
24 nffvmpt1 6902 . . . . 5 𝑥((𝑥𝐴𝐵)‘𝑦)
25 nfcv 2902 . . . . 5 𝑥𝑅
26 nffvmpt1 6902 . . . . 5 𝑥((𝑥𝐴𝐶)‘𝑦)
2724, 25, 26nfbr 5195 . . . 4 𝑥((𝑥𝐴𝐵)‘𝑦)𝑅((𝑥𝐴𝐶)‘𝑦)
28 nfv 1916 . . . 4 𝑦((𝑥𝐴𝐵)‘𝑥)𝑅((𝑥𝐴𝐶)‘𝑥)
29 fveq2 6891 . . . . 5 (𝑦 = 𝑥 → ((𝑥𝐴𝐵)‘𝑦) = ((𝑥𝐴𝐵)‘𝑥))
30 fveq2 6891 . . . . 5 (𝑦 = 𝑥 → ((𝑥𝐴𝐶)‘𝑦) = ((𝑥𝐴𝐶)‘𝑥))
3129, 30breq12d 5161 . . . 4 (𝑦 = 𝑥 → (((𝑥𝐴𝐵)‘𝑦)𝑅((𝑥𝐴𝐶)‘𝑦) ↔ ((𝑥𝐴𝐵)‘𝑥)𝑅((𝑥𝐴𝐶)‘𝑥)))
3227, 28, 31cbvralw 3302 . . 3 (∀𝑦𝐴 ((𝑥𝐴𝐵)‘𝑦)𝑅((𝑥𝐴𝐶)‘𝑦) ↔ ∀𝑥𝐴 ((𝑥𝐴𝐵)‘𝑥)𝑅((𝑥𝐴𝐶)‘𝑥))
33 simpr 484 . . . . . 6 ((𝜑𝑥𝐴) → 𝑥𝐴)
343fvmpt2 7009 . . . . . 6 ((𝑥𝐴𝐵𝑊) → ((𝑥𝐴𝐵)‘𝑥) = 𝐵)
3533, 1, 34syl2anc 583 . . . . 5 ((𝜑𝑥𝐴) → ((𝑥𝐴𝐵)‘𝑥) = 𝐵)
3611fvmpt2 7009 . . . . . 6 ((𝑥𝐴𝐶𝑋) → ((𝑥𝐴𝐶)‘𝑥) = 𝐶)
3733, 9, 36syl2anc 583 . . . . 5 ((𝜑𝑥𝐴) → ((𝑥𝐴𝐶)‘𝑥) = 𝐶)
3835, 37breq12d 5161 . . . 4 ((𝜑𝑥𝐴) → (((𝑥𝐴𝐵)‘𝑥)𝑅((𝑥𝐴𝐶)‘𝑥) ↔ 𝐵𝑅𝐶))
3938ralbidva 3174 . . 3 (𝜑 → (∀𝑥𝐴 ((𝑥𝐴𝐵)‘𝑥)𝑅((𝑥𝐴𝐶)‘𝑥) ↔ ∀𝑥𝐴 𝐵𝑅𝐶))
4032, 39bitrid 283 . 2 (𝜑 → (∀𝑦𝐴 ((𝑥𝐴𝐵)‘𝑦)𝑅((𝑥𝐴𝐶)‘𝑦) ↔ ∀𝑥𝐴 𝐵𝑅𝐶))
4123, 40bitrd 279 1 (𝜑 → (𝐹r 𝑅𝐺 ↔ ∀𝑥𝐴 𝐵𝑅𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395   = wceq 1540  wcel 2105  wral 3060   class class class wbr 5148  cmpt 5231   Fn wfn 6538  cfv 6543  r cofr 7672
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 2702  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pr 5427
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-reu 3376  df-rab 3432  df-v 3475  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-iun 4999  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-fo 6549  df-f1o 6550  df-fv 6551  df-ofr 7674
This theorem is referenced by:  gsumbagdiaglemOLD  21711  gsumbagdiaglem  21714  mplmonmul  21811  coe1mul2lem1  22010  itg2const  25491  itg2const2  25492  itg2uba  25494  itg2mulclem  25497  itg2splitlem  25499  itg2split  25500  itg2monolem1  25501  itg2gt0  25511  itg2cnlem1  25512  itg2cnlem2  25513  iblss  25555  i1fibl  25558  itgitg1  25559  itgle  25560  ibladdlem  25570  iblabs  25579  iblabsr  25580  iblmulc2  25581  bddmulibl  25589  bddiblnc  25592  itg2addnclem  36843  itg2addnclem3  36845  itg2addnc  36846  itg2gt0cn  36847  ibladdnclem  36848  iblabsnc  36856  iblmulc2nc  36857  ftc1anclem4  36868  ftc1anclem5  36869  ftc1anclem6  36870  ftc1anclem7  36871  ftc1anclem8  36872  ftc1anc  36873
  Copyright terms: Public domain W3C validator