Theorem ofoprabco 33312

Description: Function operation as a composition with an operation. (Contributed by Thierry Arnoux, 4-Jun-2017.)

Hypotheses

Ref	Expression
ofoprabco.1	⊢ Ⅎ𝑎𝑀
ofoprabco.2	⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
ofoprabco.3	⊢ (𝜑 → 𝐺:𝐴⟶𝐶)
ofoprabco.4	⊢ (𝜑 → 𝐴 ∈ 𝑉)
ofoprabco.5	⊢ (𝜑 → 𝑀 = (𝑎 ∈ 𝐴 ↦ ⟨(𝐹‘𝑎), (𝐺‘𝑎)⟩))
ofoprabco.6	⊢ (𝜑 → 𝑁 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐶 ↦ (𝑥𝑅𝑦)))

Assertion

Ref	Expression
ofoprabco	⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) = (𝑁 ∘ 𝑀))

Distinct variable groups:   𝑥,𝑎,𝑦,𝐴   𝐵,𝑎,𝑥,𝑦   𝐶,𝑎,𝑥,𝑦   𝐹,𝑎,𝑥,𝑦   𝐺,𝑎,𝑥,𝑦   𝑁,𝑎   𝑅,𝑎,𝑥,𝑦   𝜑,𝑎,𝑥,𝑦

Allowed substitution hints:   𝑀(𝑥, 𝑦, 𝑎)   𝑁(𝑥, 𝑦)   𝑉(𝑥, 𝑦, 𝑎)

Proof of Theorem ofoprabco

Step	Hyp	Ref	Expression
1		ofoprabco.5	. . . . . 6 ⊢ (𝜑 → 𝑀 = (𝑎 ∈ 𝐴 ↦ ⟨(𝐹‘𝑎), (𝐺‘𝑎)⟩))
2		ofoprabco.2	. . . . . . . 8 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
3	2	ffvelcdmda 7092	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝐹‘𝑎) ∈ 𝐵)
4		ofoprabco.3	. . . . . . . 8 ⊢ (𝜑 → 𝐺:𝐴⟶𝐶)
5	4	ffvelcdmda 7092	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝐺‘𝑎) ∈ 𝐶)
6		opelxpi 5691	. . . . . . 7 ⊢ (((𝐹‘𝑎) ∈ 𝐵 ∧ (𝐺‘𝑎) ∈ 𝐶) → ⟨(𝐹‘𝑎), (𝐺‘𝑎)⟩ ∈ (𝐵 × 𝐶))
7	3, 5, 6	syl2anc 596	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ⟨(𝐹‘𝑎), (𝐺‘𝑎)⟩ ∈ (𝐵 × 𝐶))
8	1, 7	fvmpt2d 7015	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑀‘𝑎) = ⟨(𝐹‘𝑎), (𝐺‘𝑎)⟩)
9	8	fveq2d 6897	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑁‘(𝑀‘𝑎)) = (𝑁‘⟨(𝐹‘𝑎), (𝐺‘𝑎)⟩))
10		df-ov 7430	. . . . 5 ⊢ ((𝐹‘𝑎)𝑁(𝐺‘𝑎)) = (𝑁‘⟨(𝐹‘𝑎), (𝐺‘𝑎)⟩)
11	10	a1i 11	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ((𝐹‘𝑎)𝑁(𝐺‘𝑎)) = (𝑁‘⟨(𝐹‘𝑎), (𝐺‘𝑎)⟩))
12		ofoprabco.6	. . . . . 6 ⊢ (𝜑 → 𝑁 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐶 ↦ (𝑥𝑅𝑦)))
13	12	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → 𝑁 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐶 ↦ (𝑥𝑅𝑦)))
14		simprl 783	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ (𝑥 = (𝐹‘𝑎) ∧ 𝑦 = (𝐺‘𝑎))) → 𝑥 = (𝐹‘𝑎))
15		simprr 785	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ (𝑥 = (𝐹‘𝑎) ∧ 𝑦 = (𝐺‘𝑎))) → 𝑦 = (𝐺‘𝑎))
16	14, 15	oveq12d 7445	. . . . 5 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ (𝑥 = (𝐹‘𝑎) ∧ 𝑦 = (𝐺‘𝑎))) → (𝑥𝑅𝑦) = ((𝐹‘𝑎)𝑅(𝐺‘𝑎)))
17		ovexd 7462	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ((𝐹‘𝑎)𝑅(𝐺‘𝑎)) ∈ V)
18	13, 16, 3, 5, 17	ovmpod 7579	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ((𝐹‘𝑎)𝑁(𝐺‘𝑎)) = ((𝐹‘𝑎)𝑅(𝐺‘𝑎)))
19	9, 11, 18	3eqtr2d 2804	. . 3 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑁‘(𝑀‘𝑎)) = ((𝐹‘𝑎)𝑅(𝐺‘𝑎)))
20	19	mpteq2dva 5200	. 2 ⊢ (𝜑 → (𝑎 ∈ 𝐴 ↦ (𝑁‘(𝑀‘𝑎))) = (𝑎 ∈ 𝐴 ↦ ((𝐹‘𝑎)𝑅(𝐺‘𝑎))))
21		ovex 7460	. . . . . 6 ⊢ (𝑥𝑅𝑦) ∈ V
22	21	rgen2w 3084	. . . . 5 ⊢ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐶 (𝑥𝑅𝑦) ∈ V
23		eqid 2763	. . . . . 6 ⊢ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐶 ↦ (𝑥𝑅𝑦)) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐶 ↦ (𝑥𝑅𝑦))
24	23	fmpo 8087	. . . . 5 ⊢ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐶 (𝑥𝑅𝑦) ∈ V ↔ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐶 ↦ (𝑥𝑅𝑦)):(𝐵 × 𝐶)⟶V)
25	22, 24	mpbi 233	. . . 4 ⊢ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐶 ↦ (𝑥𝑅𝑦)):(𝐵 × 𝐶)⟶V
26	12	feq1d 6699	. . . 4 ⊢ (𝜑 → (𝑁:(𝐵 × 𝐶)⟶V ↔ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐶 ↦ (𝑥𝑅𝑦)):(𝐵 × 𝐶)⟶V))
27	25, 26	mpbiri 261	. . 3 ⊢ (𝜑 → 𝑁:(𝐵 × 𝐶)⟶V)
28	1, 7	fmpt3d 7124	. . 3 ⊢ (𝜑 → 𝑀:𝐴⟶(𝐵 × 𝐶))
29		ofoprabco.1	. . . 4 ⊢ Ⅎ𝑎𝑀
30	29	fcomptf 33306	. . 3 ⊢ ((𝑁:(𝐵 × 𝐶)⟶V ∧ 𝑀:𝐴⟶(𝐵 × 𝐶)) → (𝑁 ∘ 𝑀) = (𝑎 ∈ 𝐴 ↦ (𝑁‘(𝑀‘𝑎))))
31	27, 28, 30	syl2anc 596	. 2 ⊢ (𝜑 → (𝑁 ∘ 𝑀) = (𝑎 ∈ 𝐴 ↦ (𝑁‘(𝑀‘𝑎))))
32		ofoprabco.4	. . 3 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
33	2	feqmptd 6961	. . 3 ⊢ (𝜑 → 𝐹 = (𝑎 ∈ 𝐴 ↦ (𝐹‘𝑎)))
34	4	feqmptd 6961	. . 3 ⊢ (𝜑 → 𝐺 = (𝑎 ∈ 𝐴 ↦ (𝐺‘𝑎)))
35	32, 3, 5, 33, 34	offval2 7720	. 2 ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) = (𝑎 ∈ 𝐴 ↦ ((𝐹‘𝑎)𝑅(𝐺‘𝑎))))
36	20, 31, 35	3eqtr4rd 2809	1 ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) = (𝑁 ∘ 𝑀))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569   ∈ wcel 2146  Ⅎwnfc 2910  ∀wral 3079  Vcvv 3453  ⟨cop 4837   ↦ cmpt 5188   × cxp 5652   ∘ ccom 5658  ⟶wf 6542  ‘cfv 6546  (class class class)co 7427   ∈ cmpo 7429   ∘_f cof 7698

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2196  ax-12 2215  ax-ext 2735  ax-rep 5234  ax-sep 5251  ax-nul 5262  ax-pr 5394  ax-un 7758

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2101  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-reu 3369  df-rab 3416  df-v 3455  df-sbc 3742  df-csb 3851  df-ss 3900  df-dif 4049  df-in 4093  df-un 4153  df-nul 4281  df-if 4485  df-sn 4588  df-pr 4590  df-op 4838  df-uni 4870  df-iun 4955  df-br 5106  df-opab 5170  df-mpt 5189  df-id 5549  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-iota 6500  df-fun 6548  df-fn 6549  df-f 6550  df-f1 6551  df-fo 6552  df-f1o 6553  df-fv 6554  df-ov 7430  df-oprab 7431  df-mpo 7432  df-of 7700  df-1st 8008  df-2nd 8009

This theorem is used by:  ofpreima  33313  rrvadd  35137