caofinvl

Description: Transfer a left inverse law to the function operation. (Contributed by NM, 22-Oct-2014)

	Ref	Expression
Hypotheses	caofref.1	$⊢ φ \to A \in V$
	caofref.2	$⊢ φ \to F : A ⟶ S$
	caofinv.3	$⊢ φ \to B \in W$
	caofinv.4	$⊢ φ \to N : S ⟶ S$
	caofinv.5	$⊢ φ \to G = (v \in A ⟼ N (F (v)))$
	caofinvl.6	$⊢ (φ \land x \in S) \to N (x) R x = B$
Assertion	caofinvl	$⊢ φ \to G R_{f} F = A \times \{B\}$

Proof

Step	Hyp	Ref	Expression
1		caofref.1	$⊢ φ \to A \in V$
2		caofref.2	$⊢ φ \to F : A ⟶ S$
3		caofinv.3	$⊢ φ \to B \in W$
4		caofinv.4	$⊢ φ \to N : S ⟶ S$
5		caofinv.5	$⊢ φ \to G = (v \in A ⟼ N (F (v)))$
6		caofinvl.6	$⊢ (φ \land x \in S) \to N (x) R x = B$
7	4	adantr	$⊢ (φ \land v \in A) \to N : S ⟶ S$
8	2	ffvelcdmda	$⊢ (φ \land v \in A) \to F (v) \in S$
9	7 8	ffvelcdmd	$⊢ (φ \land v \in A) \to N (F (v)) \in S$
10	5 9	fmpt3d	$⊢ φ \to G : A ⟶ S$
11	10	ffvelcdmda	$⊢ (φ \land w \in A) \to G (w) \in S$
12	2	ffvelcdmda	$⊢ (φ \land w \in A) \to F (w) \in S$
13		fvex	$⊢ N (F (v)) \in V$
14		eqid	$⊢ (v \in A ⟼ N (F (v))) = (v \in A ⟼ N (F (v)))$
15	13 14	fnmpti	$⊢ (v \in A ⟼ N (F (v))) Fn A$
16	5	fneq1d	$⊢ φ \to (G Fn A \leftrightarrow (v \in A ⟼ N (F (v))) Fn A)$
17	15 16	mpbiri	$⊢ φ \to G Fn A$
18		dffn5	$⊢ G Fn A \leftrightarrow G = (w \in A ⟼ G (w))$
19	17 18	sylib	$⊢ φ \to G = (w \in A ⟼ G (w))$
20	2	feqmptd	$⊢ φ \to F = (w \in A ⟼ F (w))$
21	1 11 12 19 20	offval2	$⊢ φ \to G R_{f} F = (w \in A ⟼ G (w) R F (w))$
22	5	fveq1d	$⊢ φ \to G (w) = (v \in A ⟼ N (F (v))) (w)$
23		2fveq3	$⊢ v = w \to N (F (v)) = N (F (w))$
24		fvex	$⊢ N (F (w)) \in V$
25	23 14 24	fvmpt	$⊢ w \in A \to (v \in A ⟼ N (F (v))) (w) = N (F (w))$
26	22 25	sylan9eq	$⊢ (φ \land w \in A) \to G (w) = N (F (w))$
27	26	oveq1d	$⊢ (φ \land w \in A) \to G (w) R F (w) = N (F (w)) R F (w)$
28		fveq2	$⊢ x = F (w) \to N (x) = N (F (w))$
29		id	$⊢ x = F (w) \to x = F (w)$
30	28 29	oveq12d	$⊢ x = F (w) \to N (x) R x = N (F (w)) R F (w)$
31	30	eqeq1d	$⊢ x = F (w) \to (N (x) R x = B \leftrightarrow N (F (w)) R F (w) = B)$
32	6	ralrimiva	$⊢ φ \to \forall x \in S N (x) R x = B$
33	32	adantr	$⊢ (φ \land w \in A) \to \forall x \in S N (x) R x = B$
34	31 33 12	rspcdva	$⊢ (φ \land w \in A) \to N (F (w)) R F (w) = B$
35	27 34	eqtrd	$⊢ (φ \land w \in A) \to G (w) R F (w) = B$
36	35	mpteq2dva	$⊢ φ \to (w \in A ⟼ G (w) R F (w)) = (w \in A ⟼ B)$
37	21 36	eqtrd	$⊢ φ \to G R_{f} F = (w \in A ⟼ B)$
38		fconstmpt	$⊢ A \times \{B\} = (w \in A ⟼ B)$
39	37 38	eqtr4di	$⊢ φ \to G R_{f} F = A \times \{B\}$

Metamath Proof Explorer

Theorem caofinvl

Proof