caofidlcan

Description: Transfer a cancellation/identity law to the function operation. (Contributed by SN, 16-Oct-2025)

	Ref	Expression
Hypotheses	caofref.1	$⊢ φ \to A \in V$
	caofref.2	$⊢ φ \to F : A ⟶ S$
	caofcom.3	$⊢ φ \to G : A ⟶ S$
	caofidlcan.4	$⊢ (φ \land (x \in S \land y \in S)) \to (x R y = y \leftrightarrow x = \underset{˙}{0})$
Assertion	caofidlcan	$⊢ φ \to (F R_{f} G = G \leftrightarrow F = A \times \{\underset{˙}{0}\})$

Proof

Step	Hyp	Ref	Expression
1		caofref.1	$⊢ φ \to A \in V$
2		caofref.2	$⊢ φ \to F : A ⟶ S$
3		caofcom.3	$⊢ φ \to G : A ⟶ S$
4		caofidlcan.4	$⊢ (φ \land (x \in S \land y \in S)) \to (x R y = y \leftrightarrow x = \underset{˙}{0})$
5	2	ffvelcdmda	$⊢ (φ \land w \in A) \to F (w) \in S$
6	3	ffvelcdmda	$⊢ (φ \land w \in A) \to G (w) \in S$
7	5 6	jca	$⊢ (φ \land w \in A) \to (F (w) \in S \land G (w) \in S)$
8	4	ralrimivva	$⊢ φ \to \forall x \in S \forall y \in S (x R y = y \leftrightarrow x = \underset{˙}{0})$
9		oveq1	$⊢ x = F (w) \to x R y = F (w) R y$
10	9	eqeq1d	$⊢ x = F (w) \to (x R y = y \leftrightarrow F (w) R y = y)$
11		eqeq1	$⊢ x = F (w) \to (x = \underset{˙}{0} \leftrightarrow F (w) = \underset{˙}{0})$
12	10 11	bibi12d	$⊢ x = F (w) \to ((x R y = y \leftrightarrow x = \underset{˙}{0}) \leftrightarrow (F (w) R y = y \leftrightarrow F (w) = \underset{˙}{0}))$
13		oveq2	$⊢ y = G (w) \to F (w) R y = F (w) R G (w)$
14		id	$⊢ y = G (w) \to y = G (w)$
15	13 14	eqeq12d	$⊢ y = G (w) \to (F (w) R y = y \leftrightarrow F (w) R G (w) = G (w))$
16	15	bibi1d	$⊢ y = G (w) \to ((F (w) R y = y \leftrightarrow F (w) = \underset{˙}{0}) \leftrightarrow (F (w) R G (w) = G (w) \leftrightarrow F (w) = \underset{˙}{0}))$
17	12 16	rspc2v	$⊢ (F (w) \in S \land G (w) \in S) \to (\forall x \in S \forall y \in S (x R y = y \leftrightarrow x = \underset{˙}{0}) \to (F (w) R G (w) = G (w) \leftrightarrow F (w) = \underset{˙}{0}))$
18	8 17	mpan9	$⊢ (φ \land (F (w) \in S \land G (w) \in S)) \to (F (w) R G (w) = G (w) \leftrightarrow F (w) = \underset{˙}{0})$
19	7 18	syldan	$⊢ (φ \land w \in A) \to (F (w) R G (w) = G (w) \leftrightarrow F (w) = \underset{˙}{0})$
20	19	ralbidva	$⊢ φ \to (\forall w \in A F (w) R G (w) = G (w) \leftrightarrow \forall w \in A F (w) = \underset{˙}{0})$
21		ovexd	$⊢ (φ \land w \in A) \to F (w) R G (w) \in V$
22	21	ralrimiva	$⊢ φ \to \forall w \in A F (w) R G (w) \in V$
23		mpteqb	$⊢ \forall w \in A F (w) R G (w) \in V \to ((w \in A ⟼ F (w) R G (w)) = (w \in A ⟼ G (w)) \leftrightarrow \forall w \in A F (w) R G (w) = G (w))$
24	22 23	syl	$⊢ φ \to ((w \in A ⟼ F (w) R G (w)) = (w \in A ⟼ G (w)) \leftrightarrow \forall w \in A F (w) R G (w) = G (w))$
25	5	ralrimiva	$⊢ φ \to \forall w \in A F (w) \in S$
26		mpteqb	$⊢ \forall w \in A F (w) \in S \to ((w \in A ⟼ F (w)) = (w \in A ⟼ \underset{˙}{0}) \leftrightarrow \forall w \in A F (w) = \underset{˙}{0})$
27	25 26	syl	$⊢ φ \to ((w \in A ⟼ F (w)) = (w \in A ⟼ \underset{˙}{0}) \leftrightarrow \forall w \in A F (w) = \underset{˙}{0})$
28	20 24 27	3bitr4d	$⊢ φ \to ((w \in A ⟼ F (w) R G (w)) = (w \in A ⟼ G (w)) \leftrightarrow (w \in A ⟼ F (w)) = (w \in A ⟼ \underset{˙}{0}))$
29	2	feqmptd	$⊢ φ \to F = (w \in A ⟼ F (w))$
30	3	feqmptd	$⊢ φ \to G = (w \in A ⟼ G (w))$
31	1 5 6 29 30	offval2	$⊢ φ \to F R_{f} G = (w \in A ⟼ F (w) R G (w))$
32	31 30	eqeq12d	$⊢ φ \to (F R_{f} G = G \leftrightarrow (w \in A ⟼ F (w) R G (w)) = (w \in A ⟼ G (w)))$
33		fconstmpt	$⊢ A \times \{\underset{˙}{0}\} = (w \in A ⟼ \underset{˙}{0})$
34	33	a1i	$⊢ φ \to A \times \{\underset{˙}{0}\} = (w \in A ⟼ \underset{˙}{0})$
35	29 34	eqeq12d	$⊢ φ \to (F = A \times \{\underset{˙}{0}\} \leftrightarrow (w \in A ⟼ F (w)) = (w \in A ⟼ \underset{˙}{0}))$
36	28 32 35	3bitr4d	$⊢ φ \to (F R_{f} G = G \leftrightarrow F = A \times \{\underset{˙}{0}\})$

Metamath Proof Explorer

Theorem caofidlcan

Proof