fmptcof2

Description: Composition of two functions expressed as ordered-pair class abstractions. (Contributed by FL, 21-Jun-2012) (Revised by Mario Carneiro, 24-Jul-2014) (Revised by Thierry Arnoux, 10-May-2017)

	Ref	Expression
Hypotheses	fmptcof2.x	$⊢ \underline{Ⅎ} x S$
	fmptcof2.y	$⊢ \underline{Ⅎ} y T$
	fmptcof2.1	$⊢ \underline{Ⅎ} x A$
	fmptcof2.2	$⊢ \underline{Ⅎ} x B$
	fmptcof2.3	$⊢ Ⅎ x φ$
	fmptcof2.4	$⊢ φ \to \forall x \in A R \in B$
	fmptcof2.5	$⊢ φ \to F = (x \in A ⟼ R)$
	fmptcof2.6	$⊢ φ \to G = (y \in B ⟼ S)$
	fmptcof2.7	$⊢ y = R \to S = T$
Assertion	fmptcof2	$⊢ φ \to G \circ F = (x \in A ⟼ T)$

Proof

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

Metamath Proof Explorer

Theorem fmptcof2

Proof