fmpoco

Description: Composition of two functions. Variation of fmptco when the second function has two arguments. (Contributed by Mario Carneiro, 8-Feb-2015)

	Ref	Expression
Hypotheses	fmpoco.1	$⊢ (φ \land (x \in A \land y \in B)) \to R \in C$
	fmpoco.2	$⊢ φ \to F = (x \in A, y \in B ⟼ R)$
	fmpoco.3	$⊢ φ \to G = (z \in C ⟼ S)$
	fmpoco.4	$⊢ z = R \to S = T$
Assertion	fmpoco	$⊢ φ \to G \circ F = (x \in A, y \in B ⟼ T)$

Proof

Step	Hyp	Ref	Expression
1		fmpoco.1	$⊢ (φ \land (x \in A \land y \in B)) \to R \in C$
2		fmpoco.2	$⊢ φ \to F = (x \in A, y \in B ⟼ R)$
3		fmpoco.3	$⊢ φ \to G = (z \in C ⟼ S)$
4		fmpoco.4	$⊢ z = R \to S = T$
5	1	ralrimivva	$⊢ φ \to \forall x \in A \forall y \in B R \in C$
6		eqid	$⊢ (x \in A, y \in B ⟼ R) = (x \in A, y \in B ⟼ R)$
7	6	fmpo	$⊢ \forall x \in A \forall y \in B R \in C \leftrightarrow (x \in A, y \in B ⟼ R) : A \times B ⟶ C$
8	5 7	sylib	$⊢ φ \to (x \in A, y \in B ⟼ R) : A \times B ⟶ C$
9		nfcv	$⊢ \underline{Ⅎ} u R$
10		nfcv	$⊢ \underline{Ⅎ} v R$
11		nfcv	$⊢ \underline{Ⅎ} x v$
12		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ u / x ⦌ R$
13	11 12	nfcsbw	$⊢ \underline{Ⅎ} x ⦋ v / y ⦌ ⦋ u / x ⦌ R$
14		nfcsb1v	$⊢ \underline{Ⅎ} y ⦋ v / y ⦌ ⦋ u / x ⦌ R$
15		csbeq1a	$⊢ x = u \to R = ⦋ u / x ⦌ R$
16		csbeq1a	$⊢ y = v \to ⦋ u / x ⦌ R = ⦋ v / y ⦌ ⦋ u / x ⦌ R$
17	15 16	sylan9eq	$⊢ (x = u \land y = v) \to R = ⦋ v / y ⦌ ⦋ u / x ⦌ R$
18	9 10 13 14 17	cbvmpo	$⊢ (x \in A, y \in B ⟼ R) = (u \in A, v \in B ⟼ ⦋ v / y ⦌ ⦋ u / x ⦌ R)$
19		vex	$⊢ u \in V$
20		vex	$⊢ v \in V$
21	19 20	op2ndd	$⊢ w = ⟨u, v⟩ \to 2^{nd} (w) = v$
22	21	csbeq1d	$⊢ w = ⟨u, v⟩ \to ⦋ 2^{nd} (w) / y ⦌ ⦋ 1^{st} (w) / x ⦌ R = ⦋ v / y ⦌ ⦋ 1^{st} (w) / x ⦌ R$
23	19 20	op1std	$⊢ w = ⟨u, v⟩ \to 1^{st} (w) = u$
24	23	csbeq1d	$⊢ w = ⟨u, v⟩ \to ⦋ 1^{st} (w) / x ⦌ R = ⦋ u / x ⦌ R$
25	24	csbeq2dv	$⊢ w = ⟨u, v⟩ \to ⦋ v / y ⦌ ⦋ 1^{st} (w) / x ⦌ R = ⦋ v / y ⦌ ⦋ u / x ⦌ R$
26	22 25	eqtrd	$⊢ w = ⟨u, v⟩ \to ⦋ 2^{nd} (w) / y ⦌ ⦋ 1^{st} (w) / x ⦌ R = ⦋ v / y ⦌ ⦋ u / x ⦌ R$
27	26	mpompt	$⊢ (w \in (A \times B) ⟼ ⦋ 2^{nd} (w) / y ⦌ ⦋ 1^{st} (w) / x ⦌ R) = (u \in A, v \in B ⟼ ⦋ v / y ⦌ ⦋ u / x ⦌ R)$
28	18 27	eqtr4i	$⊢ (x \in A, y \in B ⟼ R) = (w \in (A \times B) ⟼ ⦋ 2^{nd} (w) / y ⦌ ⦋ 1^{st} (w) / x ⦌ R)$
29	28	fmpt	$⊢ \forall w \in (A \times B) ⦋ 2^{nd} (w) / y ⦌ ⦋ 1^{st} (w) / x ⦌ R \in C \leftrightarrow (x \in A, y \in B ⟼ R) : A \times B ⟶ C$
30	8 29	sylibr	$⊢ φ \to \forall w \in (A \times B) ⦋ 2^{nd} (w) / y ⦌ ⦋ 1^{st} (w) / x ⦌ R \in C$
31	2 28	eqtrdi	$⊢ φ \to F = (w \in (A \times B) ⟼ ⦋ 2^{nd} (w) / y ⦌ ⦋ 1^{st} (w) / x ⦌ R)$
32	30 31 3	fmptcos	$⊢ φ \to G \circ F = (w \in (A \times B) ⟼ ⦋ ⦋ 2^{nd} (w) / y ⦌ ⦋ 1^{st} (w) / x ⦌ R / z ⦌ S)$
33	26	csbeq1d	$⊢ w = ⟨u, v⟩ \to ⦋ ⦋ 2^{nd} (w) / y ⦌ ⦋ 1^{st} (w) / x ⦌ R / z ⦌ S = ⦋ ⦋ v / y ⦌ ⦋ u / x ⦌ R / z ⦌ S$
34	33	mpompt	$⊢ (w \in (A \times B) ⟼ ⦋ ⦋ 2^{nd} (w) / y ⦌ ⦋ 1^{st} (w) / x ⦌ R / z ⦌ S) = (u \in A, v \in B ⟼ ⦋ ⦋ v / y ⦌ ⦋ u / x ⦌ R / z ⦌ S)$
35		nfcv	$⊢ \underline{Ⅎ} u ⦋ R / z ⦌ S$
36		nfcv	$⊢ \underline{Ⅎ} v ⦋ R / z ⦌ S$
37		nfcv	$⊢ \underline{Ⅎ} x S$
38	13 37	nfcsbw	$⊢ \underline{Ⅎ} x ⦋ ⦋ v / y ⦌ ⦋ u / x ⦌ R / z ⦌ S$
39		nfcv	$⊢ \underline{Ⅎ} y S$
40	14 39	nfcsbw	$⊢ \underline{Ⅎ} y ⦋ ⦋ v / y ⦌ ⦋ u / x ⦌ R / z ⦌ S$
41	17	csbeq1d	$⊢ (x = u \land y = v) \to ⦋ R / z ⦌ S = ⦋ ⦋ v / y ⦌ ⦋ u / x ⦌ R / z ⦌ S$
42	35 36 38 40 41	cbvmpo	$⊢ (x \in A, y \in B ⟼ ⦋ R / z ⦌ S) = (u \in A, v \in B ⟼ ⦋ ⦋ v / y ⦌ ⦋ u / x ⦌ R / z ⦌ S)$
43	34 42	eqtr4i	$⊢ (w \in (A \times B) ⟼ ⦋ ⦋ 2^{nd} (w) / y ⦌ ⦋ 1^{st} (w) / x ⦌ R / z ⦌ S) = (x \in A, y \in B ⟼ ⦋ R / z ⦌ S)$
44	1	3impb	$⊢ (φ \land x \in A \land y \in B) \to R \in C$
45		nfcvd	$⊢ R \in C \to \underline{Ⅎ} z T$
46	45 4	csbiegf	$⊢ R \in C \to ⦋ R / z ⦌ S = T$
47	44 46	syl	$⊢ (φ \land x \in A \land y \in B) \to ⦋ R / z ⦌ S = T$
48	47	mpoeq3dva	$⊢ φ \to (x \in A, y \in B ⟼ ⦋ R / z ⦌ S) = (x \in A, y \in B ⟼ T)$
49	43 48	syl5eq	$⊢ φ \to (w \in (A \times B) ⟼ ⦋ ⦋ 2^{nd} (w) / y ⦌ ⦋ 1^{st} (w) / x ⦌ R / z ⦌ S) = (x \in A, y \in B ⟼ T)$
50	32 49	eqtrd	$⊢ φ \to G \circ F = (x \in A, y \in B ⟼ T)$

Metamath Proof Explorer

Theorem fmpoco

Proof