Theorem ofrfval2 7693

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.

Step	Hyp	Ref	Expression
1		offval2.2	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊)
2	1	ralrimiva 3163	. . . . 5 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊)
3		eqid 2769	. . . . . 6 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
4	3	fnmpt 6673	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 → (𝑥 ∈ 𝐴 ↦ 𝐵) Fn 𝐴)
5	2, 4	syl 18	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) Fn 𝐴)
6		offval2.4	. . . . 5 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵))
7	6	fneq1d 6626	. . . 4 ⊢ (𝜑 → (𝐹 Fn 𝐴 ↔ (𝑥 ∈ 𝐴 ↦ 𝐵) Fn 𝐴))
8	5, 7	mpbird 260	. . 3 ⊢ (𝜑 → 𝐹 Fn 𝐴)
9		offval2.3	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑋)
10	9	ralrimiva 3163	. . . . 5 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐶 ∈ 𝑋)
11		eqid 2769	. . . . . 6 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐴 ↦ 𝐶)
12	11	fnmpt 6673	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝑋 → (𝑥 ∈ 𝐴 ↦ 𝐶) Fn 𝐴)
13	10, 12	syl 18	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) Fn 𝐴)
14		offval2.5	. . . . 5 ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐶))
15	14	fneq1d 6626	. . . 4 ⊢ (𝜑 → (𝐺 Fn 𝐴 ↔ (𝑥 ∈ 𝐴 ↦ 𝐶) Fn 𝐴))
16	13, 15	mpbird 260	. . 3 ⊢ (𝜑 → 𝐺 Fn 𝐴)
17		offval2.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
18		inidm 4187	. . 3 ⊢ (𝐴 ∩ 𝐴) = 𝐴
19	6	adantr 485	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵))
20	19	fveq1d 6881	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝐹‘𝑦) = ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑦))
21	14	adantr 485	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐶))
22	21	fveq1d 6881	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝐺‘𝑦) = ((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑦))
23	8, 16, 17, 17, 18, 20, 22	ofrfval 7682	. 2 ⊢ (𝜑 → (𝐹 ∘r 𝑅𝐺 ↔ ∀𝑦 ∈ 𝐴 ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑦)𝑅((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑦)))
24		nffvmpt1 6890	. . . . 5 ⊢ Ⅎ𝑥((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑦)
25		nfcv 2931	. . . . 5 ⊢ Ⅎ𝑥𝑅
26		nffvmpt1 6890	. . . . 5 ⊢ Ⅎ𝑥((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑦)
27	24, 25, 26	nfbr 5159	. . . 4 ⊢ Ⅎ𝑥((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑦)𝑅((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑦)
28		nfv 1941	. . . 4 ⊢ Ⅎ𝑦((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)𝑅((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑥)
29		fveq2 6879	. . . . 5 ⊢ (𝑦 = 𝑥 → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑦) = ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥))
30		fveq2 6879	. . . . 5 ⊢ (𝑦 = 𝑥 → ((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑦) = ((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑥))
31	29, 30	breq12d 5123	. . . 4 ⊢ (𝑦 = 𝑥 → (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑦)𝑅((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑦) ↔ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)𝑅((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑥)))
32	27, 28, 31	cbvralw 3313	. . 3 ⊢ (∀𝑦 ∈ 𝐴 ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑦)𝑅((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑦) ↔ ∀𝑥 ∈ 𝐴 ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)𝑅((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑥))
33		simpr 489	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴)
34	3	fvmpt2 6999	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑊) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = 𝐵)
35	33, 1, 34	syl2anc 595	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = 𝐵)
36	11	fvmpt2 6999	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐶 ∈ 𝑋) → ((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑥) = 𝐶)
37	33, 9, 36	syl2anc 595	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑥) = 𝐶)
38	35, 37	breq12d 5123	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)𝑅((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑥) ↔ 𝐵𝑅𝐶))
39	38	ralbidva 3192	. . 3 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)𝑅((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑥) ↔ ∀𝑥 ∈ 𝐴 𝐵𝑅𝐶))
40	32, 39	bitrid 286	. 2 ⊢ (𝜑 → (∀𝑦 ∈ 𝐴 ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑦)𝑅((𝑥 ∈ 𝐴 ↦ 𝐶)‘𝑦) ↔ ∀𝑥 ∈ 𝐴 𝐵𝑅𝐶))
41	23, 40	bitrd 282	1 ⊢ (𝜑 → (𝐹 ∘r 𝑅𝐺 ↔ ∀𝑥 ∈ 𝐴 𝐵𝑅𝐶))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1567   ∈ wcel 2149  ∀wral 3085   class class class wbr 5110   ↦ cmpt 5193   Fn wfn 6529  ‘cfv 6534   ∘_r cofr 7671

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-rep 5239  ax-sep 5258  ax-nul 5268  ax-pr 5402

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-iun 4959  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6490  df-fun 6536  df-fn 6537  df-f 6538  df-f1 6539  df-fo 6540  df-f1o 6541  df-fv 6542  df-ofr 7673

This theorem is referenced by:  gsumbagdiaglem  22046  mplmonmul  22152  coe1mul2lem1  22393  itg2const  25864  itg2const2  25865  itg2uba  25867  itg2mulclem  25870  itg2splitlem  25872  itg2split  25873  itg2monolem1  25874  itg2gt0  25884  itg2cnlem1  25885  itg2cnlem2  25886  iblss  25929  i1fibl  25932  itgitg1  25933  itgle  25934  ibladdlem  25944  iblabs  25953  iblabsr  25954  iblmulc2  25955  bddmulibl  25963  bddiblnc  25966  mplmulmvr  33870  psrmonmul  33881  itg2addnclem  38205  itg2addnclem3  38207  itg2addnc  38208  itg2gt0cn  38209  ibladdnclem  38210  iblabsnc  38218  iblmulc2nc  38219  ftc1anclem4  38230  ftc1anclem5  38231  ftc1anclem6  38232  ftc1anclem7  38233  ftc1anclem8  38234  ftc1anc  38235