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

Theorem ofrfval2 7639
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 3144 . . . . 5 (𝜑 → ∀𝑥𝐴 𝐵𝑊)
3 eqid 2737 . . . . . 6 (𝑥𝐴𝐵) = (𝑥𝐴𝐵)
43fnmpt 6642 . . . . 5 (∀𝑥𝐴 𝐵𝑊 → (𝑥𝐴𝐵) Fn 𝐴)
52, 4syl 17 . . . 4 (𝜑 → (𝑥𝐴𝐵) Fn 𝐴)
6 offval2.4 . . . . 5 (𝜑𝐹 = (𝑥𝐴𝐵))
76fneq1d 6596 . . . 4 (𝜑 → (𝐹 Fn 𝐴 ↔ (𝑥𝐴𝐵) Fn 𝐴))
85, 7mpbird 257 . . 3 (𝜑𝐹 Fn 𝐴)
9 offval2.3 . . . . . 6 ((𝜑𝑥𝐴) → 𝐶𝑋)
109ralrimiva 3144 . . . . 5 (𝜑 → ∀𝑥𝐴 𝐶𝑋)
11 eqid 2737 . . . . . 6 (𝑥𝐴𝐶) = (𝑥𝐴𝐶)
1211fnmpt 6642 . . . . 5 (∀𝑥𝐴 𝐶𝑋 → (𝑥𝐴𝐶) Fn 𝐴)
1310, 12syl 17 . . . 4 (𝜑 → (𝑥𝐴𝐶) Fn 𝐴)
14 offval2.5 . . . . 5 (𝜑𝐺 = (𝑥𝐴𝐶))
1514fneq1d 6596 . . . 4 (𝜑 → (𝐺 Fn 𝐴 ↔ (𝑥𝐴𝐶) Fn 𝐴))
1613, 15mpbird 257 . . 3 (𝜑𝐺 Fn 𝐴)
17 offval2.1 . . 3 (𝜑𝐴𝑉)
18 inidm 4179 . . 3 (𝐴𝐴) = 𝐴
196adantr 482 . . . 4 ((𝜑𝑦𝐴) → 𝐹 = (𝑥𝐴𝐵))
2019fveq1d 6845 . . 3 ((𝜑𝑦𝐴) → (𝐹𝑦) = ((𝑥𝐴𝐵)‘𝑦))
2114adantr 482 . . . 4 ((𝜑𝑦𝐴) → 𝐺 = (𝑥𝐴𝐶))
2221fveq1d 6845 . . 3 ((𝜑𝑦𝐴) → (𝐺𝑦) = ((𝑥𝐴𝐶)‘𝑦))
238, 16, 17, 17, 18, 20, 22ofrfval 7628 . 2 (𝜑 → (𝐹r 𝑅𝐺 ↔ ∀𝑦𝐴 ((𝑥𝐴𝐵)‘𝑦)𝑅((𝑥𝐴𝐶)‘𝑦)))
24 nffvmpt1 6854 . . . . 5 𝑥((𝑥𝐴𝐵)‘𝑦)
25 nfcv 2908 . . . . 5 𝑥𝑅
26 nffvmpt1 6854 . . . . 5 𝑥((𝑥𝐴𝐶)‘𝑦)
2724, 25, 26nfbr 5153 . . . 4 𝑥((𝑥𝐴𝐵)‘𝑦)𝑅((𝑥𝐴𝐶)‘𝑦)
28 nfv 1918 . . . 4 𝑦((𝑥𝐴𝐵)‘𝑥)𝑅((𝑥𝐴𝐶)‘𝑥)
29 fveq2 6843 . . . . 5 (𝑦 = 𝑥 → ((𝑥𝐴𝐵)‘𝑦) = ((𝑥𝐴𝐵)‘𝑥))
30 fveq2 6843 . . . . 5 (𝑦 = 𝑥 → ((𝑥𝐴𝐶)‘𝑦) = ((𝑥𝐴𝐶)‘𝑥))
3129, 30breq12d 5119 . . . 4 (𝑦 = 𝑥 → (((𝑥𝐴𝐵)‘𝑦)𝑅((𝑥𝐴𝐶)‘𝑦) ↔ ((𝑥𝐴𝐵)‘𝑥)𝑅((𝑥𝐴𝐶)‘𝑥)))
3227, 28, 31cbvralw 3290 . . 3 (∀𝑦𝐴 ((𝑥𝐴𝐵)‘𝑦)𝑅((𝑥𝐴𝐶)‘𝑦) ↔ ∀𝑥𝐴 ((𝑥𝐴𝐵)‘𝑥)𝑅((𝑥𝐴𝐶)‘𝑥))
33 simpr 486 . . . . . 6 ((𝜑𝑥𝐴) → 𝑥𝐴)
343fvmpt2 6960 . . . . . 6 ((𝑥𝐴𝐵𝑊) → ((𝑥𝐴𝐵)‘𝑥) = 𝐵)
3533, 1, 34syl2anc 585 . . . . 5 ((𝜑𝑥𝐴) → ((𝑥𝐴𝐵)‘𝑥) = 𝐵)
3611fvmpt2 6960 . . . . . 6 ((𝑥𝐴𝐶𝑋) → ((𝑥𝐴𝐶)‘𝑥) = 𝐶)
3733, 9, 36syl2anc 585 . . . . 5 ((𝜑𝑥𝐴) → ((𝑥𝐴𝐶)‘𝑥) = 𝐶)
3835, 37breq12d 5119 . . . 4 ((𝜑𝑥𝐴) → (((𝑥𝐴𝐵)‘𝑥)𝑅((𝑥𝐴𝐶)‘𝑥) ↔ 𝐵𝑅𝐶))
3938ralbidva 3173 . . 3 (𝜑 → (∀𝑥𝐴 ((𝑥𝐴𝐵)‘𝑥)𝑅((𝑥𝐴𝐶)‘𝑥) ↔ ∀𝑥𝐴 𝐵𝑅𝐶))
4032, 39bitrid 283 . 2 (𝜑 → (∀𝑦𝐴 ((𝑥𝐴𝐵)‘𝑦)𝑅((𝑥𝐴𝐶)‘𝑦) ↔ ∀𝑥𝐴 𝐵𝑅𝐶))
4123, 40bitrd 279 1 (𝜑 → (𝐹r 𝑅𝐺 ↔ ∀𝑥𝐴 𝐵𝑅𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397   = wceq 1542  wcel 2107  wral 3065   class class class wbr 5106  cmpt 5189   Fn wfn 6492  cfv 6497  r cofr 7617
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5243  ax-sep 5257  ax-nul 5264  ax-pr 5385
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-ral 3066  df-rex 3075  df-reu 3355  df-rab 3409  df-v 3448  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-iun 4957  df-br 5107  df-opab 5169  df-mpt 5190  df-id 5532  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-ofr 7619
This theorem is referenced by:  gsumbagdiaglemOLD  21343  gsumbagdiaglem  21346  mplmonmul  21440  coe1mul2lem1  21641  itg2const  25108  itg2const2  25109  itg2uba  25111  itg2mulclem  25114  itg2splitlem  25116  itg2split  25117  itg2monolem1  25118  itg2gt0  25128  itg2cnlem1  25129  itg2cnlem2  25130  iblss  25172  i1fibl  25175  itgitg1  25176  itgle  25177  ibladdlem  25187  iblabs  25196  iblabsr  25197  iblmulc2  25198  bddmulibl  25206  bddiblnc  25209  itg2addnclem  36132  itg2addnclem3  36134  itg2addnc  36135  itg2gt0cn  36136  ibladdnclem  36137  iblabsnc  36145  iblmulc2nc  36146  ftc1anclem4  36157  ftc1anclem5  36158  ftc1anclem6  36159  ftc1anclem7  36160  ftc1anclem8  36161  ftc1anc  36162
  Copyright terms: Public domain W3C validator