caofcan

Description: Transfer a cancellation law like mulcan to the function operation. (Contributed by Steve Rodriguez, 16-Nov-2015)

	Ref	Expression
Hypotheses	caofcan.1	$⊢ φ \to A \in V$
	caofcan.2	$⊢ φ \to F : A ⟶ T$
	caofcan.3	$⊢ φ \to G : A ⟶ S$
	caofcan.4	$⊢ φ \to H : A ⟶ S$
	caofcan.5	$⊢ (φ \land (x \in T \land y \in S \land z \in S)) \to (x R y = x R z \leftrightarrow y = z)$
Assertion	caofcan	$⊢ φ \to (F R_{f} G = F R_{f} H \leftrightarrow G = H)$

Proof

Step	Hyp	Ref	Expression
1		caofcan.1	$⊢ φ \to A \in V$
2		caofcan.2	$⊢ φ \to F : A ⟶ T$
3		caofcan.3	$⊢ φ \to G : A ⟶ S$
4		caofcan.4	$⊢ φ \to H : A ⟶ S$
5		caofcan.5	$⊢ (φ \land (x \in T \land y \in S \land z \in S)) \to (x R y = x R z \leftrightarrow y = z)$
6	2	ffnd	$⊢ φ \to F Fn A$
7	3	ffnd	$⊢ φ \to G Fn A$
8		inidm	$⊢ A \cap A = A$
9		eqidd	$⊢ (φ \land w \in A) \to F (w) = F (w)$
10		eqidd	$⊢ (φ \land w \in A) \to G (w) = G (w)$
11	6 7 1 1 8 9 10	ofval	$⊢ (φ \land w \in A) \to (F R_{f} G) (w) = F (w) R G (w)$
12	4	ffnd	$⊢ φ \to H Fn A$
13		eqidd	$⊢ (φ \land w \in A) \to H (w) = H (w)$
14	6 12 1 1 8 9 13	ofval	$⊢ (φ \land w \in A) \to (F R_{f} H) (w) = F (w) R H (w)$
15	11 14	eqeq12d	$⊢ (φ \land w \in A) \to ((F R_{f} G) (w) = (F R_{f} H) (w) \leftrightarrow F (w) R G (w) = F (w) R H (w))$
16		simpl	$⊢ (φ \land w \in A) \to φ$
17	2	ffvelcdmda	$⊢ (φ \land w \in A) \to F (w) \in T$
18	3	ffvelcdmda	$⊢ (φ \land w \in A) \to G (w) \in S$
19	4	ffvelcdmda	$⊢ (φ \land w \in A) \to H (w) \in S$
20	5	caovcang	$⊢ (φ \land (F (w) \in T \land G (w) \in S \land H (w) \in S)) \to (F (w) R G (w) = F (w) R H (w) \leftrightarrow G (w) = H (w))$
21	16 17 18 19 20	syl13anc	$⊢ (φ \land w \in A) \to (F (w) R G (w) = F (w) R H (w) \leftrightarrow G (w) = H (w))$
22	15 21	bitrd	$⊢ (φ \land w \in A) \to ((F R_{f} G) (w) = (F R_{f} H) (w) \leftrightarrow G (w) = H (w))$
23	22	ralbidva	$⊢ φ \to (\forall w \in A (F R_{f} G) (w) = (F R_{f} H) (w) \leftrightarrow \forall w \in A G (w) = H (w))$
24	6 7 1 1 8	offn	$⊢ φ \to (F R_{f} G) Fn A$
25	6 12 1 1 8	offn	$⊢ φ \to (F R_{f} H) Fn A$
26		eqfnfv	$⊢ ((F R_{f} G) Fn A \land (F R_{f} H) Fn A) \to (F R_{f} G = F R_{f} H \leftrightarrow \forall w \in A (F R_{f} G) (w) = (F R_{f} H) (w))$
27	24 25 26	syl2anc	$⊢ φ \to (F R_{f} G = F R_{f} H \leftrightarrow \forall w \in A (F R_{f} G) (w) = (F R_{f} H) (w))$
28		eqfnfv	$⊢ (G Fn A \land H Fn A) \to (G = H \leftrightarrow \forall w \in A G (w) = H (w))$
29	7 12 28	syl2anc	$⊢ φ \to (G = H \leftrightarrow \forall w \in A G (w) = H (w))$
30	23 27 29	3bitr4d	$⊢ φ \to (F R_{f} G = F R_{f} H \leftrightarrow G = H)$

Metamath Proof Explorer

Theorem caofcan

Proof