afvco2

Description: Value of a function composition, analogous to fvco2 . (Contributed by Alexander van der Vekens, 23-Jul-2017)

		Ref	Expression
	Assertion	afvco2	$⊢ (G Fn A \land X \in A) \to ((F \circ G)''' X) = (F''' (G''' X))$

Proof

Step	Hyp	Ref	Expression
1		fvco2	$⊢ (G Fn A \land X \in A) \to (F \circ G) (X) = F (G (X))$
2	1	adantl	$⊢ ((G (X) \in dom F \land Fun ({F ↾}_{\{G (X)\}})) \land (G Fn A \land X \in A)) \to (F \circ G) (X) = F (G (X))$
3		simpll	$⊢ ((G (X) \in dom F \land Fun ({F ↾}_{\{G (X)\}})) \land (G Fn A \land X \in A)) \to G (X) \in dom F$
4		df-fn	$⊢ G Fn A \leftrightarrow (Fun G \land dom G = A)$
5		simpll	$⊢ ((Fun G \land dom G = A) \land X \in A) \to Fun G$
6		eleq2	$⊢ A = dom G \to (X \in A \leftrightarrow X \in dom G)$
7	6	eqcoms	$⊢ dom G = A \to (X \in A \leftrightarrow X \in dom G)$
8	7	biimpd	$⊢ dom G = A \to (X \in A \to X \in dom G)$
9	8	adantl	$⊢ (Fun G \land dom G = A) \to (X \in A \to X \in dom G)$
10	9	imp	$⊢ ((Fun G \land dom G = A) \land X \in A) \to X \in dom G$
11	5 10	jca	$⊢ ((Fun G \land dom G = A) \land X \in A) \to (Fun G \land X \in dom G)$
12	4 11	sylanb	$⊢ (G Fn A \land X \in A) \to (Fun G \land X \in dom G)$
13	12	adantl	$⊢ ((G (X) \in dom F \land Fun ({F ↾}_{\{G (X)\}})) \land (G Fn A \land X \in A)) \to (Fun G \land X \in dom G)$
14		dmfco	$⊢ (Fun G \land X \in dom G) \to (X \in dom (F \circ G) \leftrightarrow G (X) \in dom F)$
15	13 14	syl	$⊢ ((G (X) \in dom F \land Fun ({F ↾}_{\{G (X)\}})) \land (G Fn A \land X \in A)) \to (X \in dom (F \circ G) \leftrightarrow G (X) \in dom F)$
16	3 15	mpbird	$⊢ ((G (X) \in dom F \land Fun ({F ↾}_{\{G (X)\}})) \land (G Fn A \land X \in A)) \to X \in dom (F \circ G)$
17		funcoressn	$⊢ ((G (X) \in dom F \land Fun ({F ↾}_{\{G (X)\}})) \land (G Fn A \land X \in A)) \to Fun ({(F \circ G) ↾}_{\{X\}})$
18		df-dfat	$⊢ (F \circ G) defAt X \leftrightarrow (X \in dom (F \circ G) \land Fun ({(F \circ G) ↾}_{\{X\}}))$
19		afvfundmfveq	$⊢ (F \circ G) defAt X \to ((F \circ G)''' X) = (F \circ G) (X)$
20	18 19	sylbir	$⊢ (X \in dom (F \circ G) \land Fun ({(F \circ G) ↾}_{\{X\}})) \to ((F \circ G)''' X) = (F \circ G) (X)$
21	16 17 20	syl2anc	$⊢ ((G (X) \in dom F \land Fun ({F ↾}_{\{G (X)\}})) \land (G Fn A \land X \in A)) \to ((F \circ G)''' X) = (F \circ G) (X)$
22		df-dfat	$⊢ F defAt G (X) \leftrightarrow (G (X) \in dom F \land Fun ({F ↾}_{\{G (X)\}}))$
23		afvfundmfveq	$⊢ F defAt G (X) \to (F''' G (X)) = F (G (X))$
24	22 23	sylbir	$⊢ (G (X) \in dom F \land Fun ({F ↾}_{\{G (X)\}})) \to (F''' G (X)) = F (G (X))$
25	24	adantr	$⊢ ((G (X) \in dom F \land Fun ({F ↾}_{\{G (X)\}})) \land (G Fn A \land X \in A)) \to (F''' G (X)) = F (G (X))$
26	2 21 25	3eqtr4d	$⊢ ((G (X) \in dom F \land Fun ({F ↾}_{\{G (X)\}})) \land (G Fn A \land X \in A)) \to ((F \circ G)''' X) = (F''' G (X))$
27		ianor	$⊢ \neg (G (X) \in dom F \land Fun ({F ↾}_{\{G (X)\}})) \leftrightarrow (\neg G (X) \in dom F \lor \neg Fun ({F ↾}_{\{G (X)\}}))$
28	14	funfni	$⊢ (G Fn A \land X \in A) \to (X \in dom (F \circ G) \leftrightarrow G (X) \in dom F)$
29	28	bicomd	$⊢ (G Fn A \land X \in A) \to (G (X) \in dom F \leftrightarrow X \in dom (F \circ G))$
30	29	notbid	$⊢ (G Fn A \land X \in A) \to (\neg G (X) \in dom F \leftrightarrow \neg X \in dom (F \circ G))$
31	30	biimpd	$⊢ (G Fn A \land X \in A) \to (\neg G (X) \in dom F \to \neg X \in dom (F \circ G))$
32		ndmafv	$⊢ \neg X \in dom (F \circ G) \to ((F \circ G)''' X) = V$
33	31 32	syl6com	$⊢ \neg G (X) \in dom F \to ((G Fn A \land X \in A) \to ((F \circ G)''' X) = V)$
34		funressnfv	$⊢ ((X \in dom (F \circ G) \land Fun ({(F \circ G) ↾}_{\{X\}})) \land (G Fn A \land X \in A)) \to Fun ({F ↾}_{\{G (X)\}})$
35	34	ex	$⊢ (X \in dom (F \circ G) \land Fun ({(F \circ G) ↾}_{\{X\}})) \to ((G Fn A \land X \in A) \to Fun ({F ↾}_{\{G (X)\}}))$
36		afvnfundmuv	$⊢ \neg (F \circ G) defAt X \to ((F \circ G)''' X) = V$
37	18 36	sylnbir	$⊢ \neg (X \in dom (F \circ G) \land Fun ({(F \circ G) ↾}_{\{X\}})) \to ((F \circ G)''' X) = V$
38	35 37	nsyl4	$⊢ \neg ((F \circ G)''' X) = V \to ((G Fn A \land X \in A) \to Fun ({F ↾}_{\{G (X)\}}))$
39	38	com12	$⊢ (G Fn A \land X \in A) \to (\neg ((F \circ G)''' X) = V \to Fun ({F ↾}_{\{G (X)\}}))$
40	39	con1d	$⊢ (G Fn A \land X \in A) \to (\neg Fun ({F ↾}_{\{G (X)\}}) \to ((F \circ G)''' X) = V)$
41	40	com12	$⊢ \neg Fun ({F ↾}_{\{G (X)\}}) \to ((G Fn A \land X \in A) \to ((F \circ G)''' X) = V)$
42	33 41	jaoi	$⊢ (\neg G (X) \in dom F \lor \neg Fun ({F ↾}_{\{G (X)\}})) \to ((G Fn A \land X \in A) \to ((F \circ G)''' X) = V)$
43	27 42	sylbi	$⊢ \neg (G (X) \in dom F \land Fun ({F ↾}_{\{G (X)\}})) \to ((G Fn A \land X \in A) \to ((F \circ G)''' X) = V)$
44	43	imp	$⊢ (\neg (G (X) \in dom F \land Fun ({F ↾}_{\{G (X)\}})) \land (G Fn A \land X \in A)) \to ((F \circ G)''' X) = V$
45		afvnfundmuv	$⊢ \neg F defAt G (X) \to (F''' G (X)) = V$
46	22 45	sylnbir	$⊢ \neg (G (X) \in dom F \land Fun ({F ↾}_{\{G (X)\}})) \to (F''' G (X)) = V$
47	46	eqcomd	$⊢ \neg (G (X) \in dom F \land Fun ({F ↾}_{\{G (X)\}})) \to V = (F''' G (X))$
48	47	adantr	$⊢ (\neg (G (X) \in dom F \land Fun ({F ↾}_{\{G (X)\}})) \land (G Fn A \land X \in A)) \to V = (F''' G (X))$
49	44 48	eqtrd	$⊢ (\neg (G (X) \in dom F \land Fun ({F ↾}_{\{G (X)\}})) \land (G Fn A \land X \in A)) \to ((F \circ G)''' X) = (F''' G (X))$
50	26 49	pm2.61ian	$⊢ (G Fn A \land X \in A) \to ((F \circ G)''' X) = (F''' G (X))$
51		eqidd	$⊢ (G Fn A \land X \in A) \to F = F$
52	4 9	sylbi	$⊢ G Fn A \to (X \in A \to X \in dom G)$
53	52	imp	$⊢ (G Fn A \land X \in A) \to X \in dom G$
54		fnfun	$⊢ G Fn A \to Fun G$
55	54	funresd	$⊢ G Fn A \to Fun ({G ↾}_{\{X\}})$
56	55	adantr	$⊢ (G Fn A \land X \in A) \to Fun ({G ↾}_{\{X\}})$
57		df-dfat	$⊢ G defAt X \leftrightarrow (X \in dom G \land Fun ({G ↾}_{\{X\}}))$
58		afvfundmfveq	$⊢ G defAt X \to (G''' X) = G (X)$
59	57 58	sylbir	$⊢ (X \in dom G \land Fun ({G ↾}_{\{X\}})) \to (G''' X) = G (X)$
60	53 56 59	syl2anc	$⊢ (G Fn A \land X \in A) \to (G''' X) = G (X)$
61	60	eqcomd	$⊢ (G Fn A \land X \in A) \to G (X) = (G''' X)$
62	51 61	afveq12d	$⊢ (G Fn A \land X \in A) \to (F''' G (X)) = (F''' (G''' X))$
63	50 62	eqtrd	$⊢ (G Fn A \land X \in A) \to ((F \circ G)''' X) = (F''' (G''' X))$

Metamath Proof Explorer

Theorem afvco2

Proof