fmptco

Description: Composition of two functions expressed as ordered-pair class abstractions. If F has the equation ( x + 2 ) and G the equation ( 3 * z ) then ( G o. F ) has the equation ( 3 * ( x + 2 ) ) . (Contributed by FL, 21-Jun-2012) (Revised by Mario Carneiro, 24-Jul-2014)

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

Proof

Step	Hyp	Ref	Expression
1		fmptco.1	$⊢ (φ \land x \in A) \to R \in B$
2		fmptco.2	$⊢ φ \to F = (x \in A ⟼ R)$
3		fmptco.3	$⊢ φ \to G = (y \in B ⟼ S)$
4		fmptco.4	$⊢ y = R \to S = T$
5		relco	$⊢ Rel (G \circ F)$
6		mptrel	$⊢ Rel (x \in A ⟼ T)$
7	2 1	fmpt3d	$⊢ φ \to F : A ⟶ B$
8	7	ffund	$⊢ φ \to Fun F$
9		funbrfv	$⊢ Fun F \to (z F u \to F (z) = u)$
10	9	imp	$⊢ (Fun F \land z F u) \to F (z) = u$
11	8 10	sylan	$⊢ (φ \land z F u) \to F (z) = u$
12	11	eqcomd	$⊢ (φ \land z F u) \to u = F (z)$
13	12	a1d	$⊢ (φ \land z F u) \to (u G w \to u = F (z))$
14	13	expimpd	$⊢ φ \to ((z F u \land u G w) \to u = F (z))$
15	14	pm4.71rd	$⊢ φ \to ((z F u \land u G w) \leftrightarrow (u = F (z) \land (z F u \land u G w)))$
16	15	exbidv	$⊢ φ \to (\exists u (z F u \land u G w) \leftrightarrow \exists u (u = F (z) \land (z F u \land u G w)))$
17		fvex	$⊢ F (z) \in V$
18		breq2	$⊢ u = F (z) \to (z F u \leftrightarrow z F F (z))$
19		breq1	$⊢ u = F (z) \to (u G w \leftrightarrow F (z) G w)$
20	18 19	anbi12d	$⊢ u = F (z) \to ((z F u \land u G w) \leftrightarrow (z F F (z) \land F (z) G w))$
21	17 20	ceqsexv	$⊢ \exists u (u = F (z) \land (z F u \land u G w)) \leftrightarrow (z F F (z) \land F (z) G w)$
22		funfvbrb	$⊢ Fun F \to (z \in dom F \leftrightarrow z F F (z))$
23	8 22	syl	$⊢ φ \to (z \in dom F \leftrightarrow z F F (z))$
24	7	fdmd	$⊢ φ \to dom F = A$
25	24	eleq2d	$⊢ φ \to (z \in dom F \leftrightarrow z \in A)$
26	23 25	bitr3d	$⊢ φ \to (z F F (z) \leftrightarrow z \in A)$
27	2	fveq1d	$⊢ φ \to F (z) = (x \in A ⟼ R) (z)$
28		eqidd	$⊢ φ \to w = w$
29	27 3 28	breq123d	$⊢ φ \to (F (z) G w \leftrightarrow (x \in A ⟼ R) (z) (y \in B ⟼ S) w)$
30	26 29	anbi12d	$⊢ φ \to ((z F F (z) \land F (z) G w) \leftrightarrow (z \in A \land (x \in A ⟼ R) (z) (y \in B ⟼ S) w))$
31		nfcv	$⊢ \underline{Ⅎ} x z$
32		nfv	$⊢ Ⅎ x φ$
33		nffvmpt1	$⊢ \underline{Ⅎ} x (x \in A ⟼ R) (z)$
34		nfcv	$⊢ \underline{Ⅎ} x (y \in B ⟼ S)$
35		nfcv	$⊢ \underline{Ⅎ} x w$
36	33 34 35	nfbr	$⊢ Ⅎ x (x \in A ⟼ R) (z) (y \in B ⟼ S) w$
37		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ z / x ⦌ T$
38	37	nfeq2	$⊢ Ⅎ x w = ⦋ z / x ⦌ T$
39	36 38	nfbi	$⊢ Ⅎ x ((x \in A ⟼ R) (z) (y \in B ⟼ S) w \leftrightarrow w = ⦋ z / x ⦌ T)$
40	32 39	nfim	$⊢ Ⅎ x (φ \to ((x \in A ⟼ R) (z) (y \in B ⟼ S) w \leftrightarrow w = ⦋ z / x ⦌ T))$
41		fveq2	$⊢ x = z \to (x \in A ⟼ R) (x) = (x \in A ⟼ R) (z)$
42	41	breq1d	$⊢ x = z \to ((x \in A ⟼ R) (x) (y \in B ⟼ S) w \leftrightarrow (x \in A ⟼ R) (z) (y \in B ⟼ S) w)$
43		csbeq1a	$⊢ x = z \to T = ⦋ z / x ⦌ T$
44	43	eqeq2d	$⊢ x = z \to (w = T \leftrightarrow w = ⦋ z / x ⦌ T)$
45	42 44	bibi12d	$⊢ x = z \to (((x \in A ⟼ R) (x) (y \in B ⟼ S) w \leftrightarrow w = T) \leftrightarrow ((x \in A ⟼ R) (z) (y \in B ⟼ S) w \leftrightarrow w = ⦋ z / x ⦌ T))$
46	45	imbi2d	$⊢ x = z \to ((φ \to ((x \in A ⟼ R) (x) (y \in B ⟼ S) w \leftrightarrow w = T)) \leftrightarrow (φ \to ((x \in A ⟼ R) (z) (y \in B ⟼ S) w \leftrightarrow w = ⦋ z / x ⦌ T)))$
47		vex	$⊢ w \in V$
48		simpl	$⊢ (y = R \land u = w) \to y = R$
49	48	eleq1d	$⊢ (y = R \land u = w) \to (y \in B \leftrightarrow R \in B)$
50		id	$⊢ u = w \to u = w$
51	50 4	eqeqan12rd	$⊢ (y = R \land u = w) \to (u = S \leftrightarrow w = T)$
52	49 51	anbi12d	$⊢ (y = R \land u = w) \to ((y \in B \land u = S) \leftrightarrow (R \in B \land w = T))$
53		df-mpt	$⊢ (y \in B ⟼ S) = \{⟨y, u⟩ \| (y \in B \land u = S)\}$
54	52 53	brabga	$⊢ (R \in B \land w \in V) \to (R (y \in B ⟼ S) w \leftrightarrow (R \in B \land w = T))$
55	1 47 54	sylancl	$⊢ (φ \land x \in A) \to (R (y \in B ⟼ S) w \leftrightarrow (R \in B \land w = T))$
56		id	$⊢ x \in A \to x \in A$
57		eqid	$⊢ (x \in A ⟼ R) = (x \in A ⟼ R)$
58	57	fvmpt2	$⊢ (x \in A \land R \in B) \to (x \in A ⟼ R) (x) = R$
59	56 1 58	syl2an2	$⊢ (φ \land x \in A) \to (x \in A ⟼ R) (x) = R$
60	59	breq1d	$⊢ (φ \land x \in A) \to ((x \in A ⟼ R) (x) (y \in B ⟼ S) w \leftrightarrow R (y \in B ⟼ S) w)$
61	1	biantrurd	$⊢ (φ \land x \in A) \to (w = T \leftrightarrow (R \in B \land w = T))$
62	55 60 61	3bitr4d	$⊢ (φ \land x \in A) \to ((x \in A ⟼ R) (x) (y \in B ⟼ S) w \leftrightarrow w = T)$
63	62	expcom	$⊢ x \in A \to (φ \to ((x \in A ⟼ R) (x) (y \in B ⟼ S) w \leftrightarrow w = T))$
64	31 40 46 63	vtoclgaf	$⊢ z \in A \to (φ \to ((x \in A ⟼ R) (z) (y \in B ⟼ S) w \leftrightarrow w = ⦋ z / x ⦌ T))$
65	64	impcom	$⊢ (φ \land z \in A) \to ((x \in A ⟼ R) (z) (y \in B ⟼ S) w \leftrightarrow w = ⦋ z / x ⦌ T)$
66	65	pm5.32da	$⊢ φ \to ((z \in A \land (x \in A ⟼ R) (z) (y \in B ⟼ S) w) \leftrightarrow (z \in A \land w = ⦋ z / x ⦌ T))$
67	30 66	bitrd	$⊢ φ \to ((z F F (z) \land F (z) G w) \leftrightarrow (z \in A \land w = ⦋ z / x ⦌ T))$
68	21 67	syl5bb	$⊢ φ \to (\exists u (u = F (z) \land (z F u \land u G w)) \leftrightarrow (z \in A \land w = ⦋ z / x ⦌ T))$
69	16 68	bitrd	$⊢ φ \to (\exists u (z F u \land u G w) \leftrightarrow (z \in A \land w = ⦋ z / x ⦌ T))$
70		vex	$⊢ z \in V$
71	70 47	opelco	$⊢ ⟨z, w⟩ \in (G \circ F) \leftrightarrow \exists u (z F u \land u G w)$
72		df-mpt	$⊢ (x \in A ⟼ T) = \{⟨x, v⟩ \| (x \in A \land v = T)\}$
73	72	eleq2i	$⊢ ⟨z, w⟩ \in (x \in A ⟼ T) \leftrightarrow ⟨z, w⟩ \in \{⟨x, v⟩ \| (x \in A \land v = T)\}$
74		nfv	$⊢ Ⅎ x z \in A$
75	37	nfeq2	$⊢ Ⅎ x v = ⦋ z / x ⦌ T$
76	74 75	nfan	$⊢ Ⅎ x (z \in A \land v = ⦋ z / x ⦌ T)$
77		nfv	$⊢ Ⅎ v (z \in A \land w = ⦋ z / x ⦌ T)$
78		eleq1w	$⊢ x = z \to (x \in A \leftrightarrow z \in A)$
79	43	eqeq2d	$⊢ x = z \to (v = T \leftrightarrow v = ⦋ z / x ⦌ T)$
80	78 79	anbi12d	$⊢ x = z \to ((x \in A \land v = T) \leftrightarrow (z \in A \land v = ⦋ z / x ⦌ T))$
81		eqeq1	$⊢ v = w \to (v = ⦋ z / x ⦌ T \leftrightarrow w = ⦋ z / x ⦌ T)$
82	81	anbi2d	$⊢ v = w \to ((z \in A \land v = ⦋ z / x ⦌ T) \leftrightarrow (z \in A \land w = ⦋ z / x ⦌ T))$
83	76 77 70 47 80 82	opelopabf	$⊢ ⟨z, w⟩ \in \{⟨x, v⟩ \| (x \in A \land v = T)\} \leftrightarrow (z \in A \land w = ⦋ z / x ⦌ T)$
84	73 83	bitri	$⊢ ⟨z, w⟩ \in (x \in A ⟼ T) \leftrightarrow (z \in A \land w = ⦋ z / x ⦌ T)$
85	69 71 84	3bitr4g	$⊢ φ \to (⟨z, w⟩ \in (G \circ F) \leftrightarrow ⟨z, w⟩ \in (x \in A ⟼ T))$
86	5 6 85	eqrelrdv	$⊢ φ \to G \circ F = (x \in A ⟼ T)$

Metamath Proof Explorer

Theorem fmptco

Proof