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

Theorem ofrfval 6803
 Description: Value of a relation applied to two functions. (Contributed by Mario Carneiro, 28-Jul-2014.)
Hypotheses
Ref Expression
offval.1 (𝜑𝐹 Fn 𝐴)
offval.2 (𝜑𝐺 Fn 𝐵)
offval.3 (𝜑𝐴𝑉)
offval.4 (𝜑𝐵𝑊)
offval.5 (𝐴𝐵) = 𝑆
offval.6 ((𝜑𝑥𝐴) → (𝐹𝑥) = 𝐶)
offval.7 ((𝜑𝑥𝐵) → (𝐺𝑥) = 𝐷)
Assertion
Ref Expression
ofrfval (𝜑 → (𝐹𝑟 𝑅𝐺 ↔ ∀𝑥𝑆 𝐶𝑅𝐷))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐹   𝑥,𝐺   𝜑,𝑥   𝑥,𝑆   𝑥,𝑅
Allowed substitution hints:   𝐵(𝑥)   𝐶(𝑥)   𝐷(𝑥)   𝑉(𝑥)   𝑊(𝑥)

Proof of Theorem ofrfval
Dummy variables 𝑓 𝑔 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 offval.1 . . . 4 (𝜑𝐹 Fn 𝐴)
2 offval.3 . . . 4 (𝜑𝐴𝑉)
3 fnex 6386 . . . 4 ((𝐹 Fn 𝐴𝐴𝑉) → 𝐹 ∈ V)
41, 2, 3syl2anc 691 . . 3 (𝜑𝐹 ∈ V)
5 offval.2 . . . 4 (𝜑𝐺 Fn 𝐵)
6 offval.4 . . . 4 (𝜑𝐵𝑊)
7 fnex 6386 . . . 4 ((𝐺 Fn 𝐵𝐵𝑊) → 𝐺 ∈ V)
85, 6, 7syl2anc 691 . . 3 (𝜑𝐺 ∈ V)
9 dmeq 5246 . . . . . 6 (𝑓 = 𝐹 → dom 𝑓 = dom 𝐹)
10 dmeq 5246 . . . . . 6 (𝑔 = 𝐺 → dom 𝑔 = dom 𝐺)
119, 10ineqan12d 3778 . . . . 5 ((𝑓 = 𝐹𝑔 = 𝐺) → (dom 𝑓 ∩ dom 𝑔) = (dom 𝐹 ∩ dom 𝐺))
12 fveq1 6102 . . . . . 6 (𝑓 = 𝐹 → (𝑓𝑥) = (𝐹𝑥))
13 fveq1 6102 . . . . . 6 (𝑔 = 𝐺 → (𝑔𝑥) = (𝐺𝑥))
1412, 13breqan12d 4599 . . . . 5 ((𝑓 = 𝐹𝑔 = 𝐺) → ((𝑓𝑥)𝑅(𝑔𝑥) ↔ (𝐹𝑥)𝑅(𝐺𝑥)))
1511, 14raleqbidv 3129 . . . 4 ((𝑓 = 𝐹𝑔 = 𝐺) → (∀𝑥 ∈ (dom 𝑓 ∩ dom 𝑔)(𝑓𝑥)𝑅(𝑔𝑥) ↔ ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝐹𝑥)𝑅(𝐺𝑥)))
16 df-ofr 6796 . . . 4 𝑟 𝑅 = {⟨𝑓, 𝑔⟩ ∣ ∀𝑥 ∈ (dom 𝑓 ∩ dom 𝑔)(𝑓𝑥)𝑅(𝑔𝑥)}
1715, 16brabga 4914 . . 3 ((𝐹 ∈ V ∧ 𝐺 ∈ V) → (𝐹𝑟 𝑅𝐺 ↔ ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝐹𝑥)𝑅(𝐺𝑥)))
184, 8, 17syl2anc 691 . 2 (𝜑 → (𝐹𝑟 𝑅𝐺 ↔ ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝐹𝑥)𝑅(𝐺𝑥)))
19 fndm 5904 . . . . . 6 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
201, 19syl 17 . . . . 5 (𝜑 → dom 𝐹 = 𝐴)
21 fndm 5904 . . . . . 6 (𝐺 Fn 𝐵 → dom 𝐺 = 𝐵)
225, 21syl 17 . . . . 5 (𝜑 → dom 𝐺 = 𝐵)
2320, 22ineq12d 3777 . . . 4 (𝜑 → (dom 𝐹 ∩ dom 𝐺) = (𝐴𝐵))
24 offval.5 . . . 4 (𝐴𝐵) = 𝑆
2523, 24syl6eq 2660 . . 3 (𝜑 → (dom 𝐹 ∩ dom 𝐺) = 𝑆)
2625raleqdv 3121 . 2 (𝜑 → (∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝐹𝑥)𝑅(𝐺𝑥) ↔ ∀𝑥𝑆 (𝐹𝑥)𝑅(𝐺𝑥)))
27 inss1 3795 . . . . . . 7 (𝐴𝐵) ⊆ 𝐴
2824, 27eqsstr3i 3599 . . . . . 6 𝑆𝐴
2928sseli 3564 . . . . 5 (𝑥𝑆𝑥𝐴)
30 offval.6 . . . . 5 ((𝜑𝑥𝐴) → (𝐹𝑥) = 𝐶)
3129, 30sylan2 490 . . . 4 ((𝜑𝑥𝑆) → (𝐹𝑥) = 𝐶)
32 inss2 3796 . . . . . . 7 (𝐴𝐵) ⊆ 𝐵
3324, 32eqsstr3i 3599 . . . . . 6 𝑆𝐵
3433sseli 3564 . . . . 5 (𝑥𝑆𝑥𝐵)
35 offval.7 . . . . 5 ((𝜑𝑥𝐵) → (𝐺𝑥) = 𝐷)
3634, 35sylan2 490 . . . 4 ((𝜑𝑥𝑆) → (𝐺𝑥) = 𝐷)
3731, 36breq12d 4596 . . 3 ((𝜑𝑥𝑆) → ((𝐹𝑥)𝑅(𝐺𝑥) ↔ 𝐶𝑅𝐷))
3837ralbidva 2968 . 2 (𝜑 → (∀𝑥𝑆 (𝐹𝑥)𝑅(𝐺𝑥) ↔ ∀𝑥𝑆 𝐶𝑅𝐷))
3918, 26, 383bitrd 293 1 (𝜑 → (𝐹𝑟 𝑅𝐺 ↔ ∀𝑥𝑆 𝐶𝑅𝐷))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977  ∀wral 2896  Vcvv 3173   ∩ cin 3539   class class class wbr 4583  dom cdm 5038   Fn wfn 5799  ‘cfv 5804   ∘𝑟 cofr 6794 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pr 4833 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-ofr 6796 This theorem is referenced by:  ofrval  6805  ofrfval2  6813  caofref  6821  caofrss  6828  caoftrn  6830  ofsubge0  10896  pwsle  15975  pwsleval  15976  psrbaglesupp  19189  psrbagcon  19192  psrbaglefi  19193  psrlidm  19224  0plef  23245  0pledm  23246  itg1ge0  23259  mbfi1fseqlem5  23292  xrge0f  23304  itg2ge0  23308  itg2lea  23317  itg2splitlem  23321  itg2monolem1  23323  itg2mono  23326  itg2i1fseqle  23327  itg2i1fseq  23328  itg2addlem  23331  itg2cnlem1  23334  itg2addnclem  32631
 Copyright terms: Public domain W3C validator