Metamath Proof Explorer

Theorem ercpbl

Description: Translate the function compatibility relation to a quotient set. (Contributed by Mario Carneiro, 24-Feb-2015) (Revised by Mario Carneiro, 12-Aug-2015) (Revised by AV, 12-Jul-2024)

		Ref	Expression
	Hypotheses	ercpbl.r	$⊢ φ \to \underset{˙}{\sim} Er V$
		ercpbl.v	$⊢ φ \to V \in W$
		ercpbl.f	$⊢ F = (x \in V ⟼ [x] \underset{˙}{\sim})$
		ercpbl.c	$⊢ (φ \land (a \in V \land b \in V)) \to a \underset{˙}{+} b \in V$
		ercpbl.e	$⊢ φ \to ((A \underset{˙}{\sim} C \land B \underset{˙}{\sim} D) \to (A \underset{˙}{+} B) \underset{˙}{\sim} (C \underset{˙}{+} D))$
	Assertion	ercpbl	$⊢ (φ \land (A \in V \land B \in V) \land (C \in V \land D \in V)) \to ((F (A) = F (C) \land F (B) = F (D)) \to F (A \underset{˙}{+} B) = F (C \underset{˙}{+} D))$

Proof

Step	Hyp	Ref	Expression
1		ercpbl.r	$⊢ φ \to \underset{˙}{\sim} Er V$
2		ercpbl.v	$⊢ φ \to V \in W$
3		ercpbl.f	$⊢ F = (x \in V ⟼ [x] \underset{˙}{\sim})$
4		ercpbl.c	$⊢ (φ \land (a \in V \land b \in V)) \to a \underset{˙}{+} b \in V$
5		ercpbl.e	$⊢ φ \to ((A \underset{˙}{\sim} C \land B \underset{˙}{\sim} D) \to (A \underset{˙}{+} B) \underset{˙}{\sim} (C \underset{˙}{+} D))$
6	5	3ad2ant1	$⊢ (φ \land (A \in V \land B \in V) \land (C \in V \land D \in V)) \to ((A \underset{˙}{\sim} C \land B \underset{˙}{\sim} D) \to (A \underset{˙}{+} B) \underset{˙}{\sim} (C \underset{˙}{+} D))$
7	1	3ad2ant1	$⊢ (φ \land (A \in V \land B \in V) \land (C \in V \land D \in V)) \to \underset{˙}{\sim} Er V$
8	2	3ad2ant1	$⊢ (φ \land (A \in V \land B \in V) \land (C \in V \land D \in V)) \to V \in W$
9		simp2l	$⊢ (φ \land (A \in V \land B \in V) \land (C \in V \land D \in V)) \to A \in V$
10	7 8 3 9	ercpbllem	$⊢ (φ \land (A \in V \land B \in V) \land (C \in V \land D \in V)) \to (F (A) = F (C) \leftrightarrow A \underset{˙}{\sim} C)$
11		simp2r	$⊢ (φ \land (A \in V \land B \in V) \land (C \in V \land D \in V)) \to B \in V$
12	7 8 3 11	ercpbllem	$⊢ (φ \land (A \in V \land B \in V) \land (C \in V \land D \in V)) \to (F (B) = F (D) \leftrightarrow B \underset{˙}{\sim} D)$
13	10 12	anbi12d	$⊢ (φ \land (A \in V \land B \in V) \land (C \in V \land D \in V)) \to ((F (A) = F (C) \land F (B) = F (D)) \leftrightarrow (A \underset{˙}{\sim} C \land B \underset{˙}{\sim} D))$
14	4	caovclg	$⊢ (φ \land (A \in V \land B \in V)) \to A \underset{˙}{+} B \in V$
15	14	3adant3	$⊢ (φ \land (A \in V \land B \in V) \land (C \in V \land D \in V)) \to A \underset{˙}{+} B \in V$
16	7 8 3 15	ercpbllem	$⊢ (φ \land (A \in V \land B \in V) \land (C \in V \land D \in V)) \to (F (A \underset{˙}{+} B) = F (C \underset{˙}{+} D) \leftrightarrow (A \underset{˙}{+} B) \underset{˙}{\sim} (C \underset{˙}{+} D))$
17	6 13 16	3imtr4d	$⊢ (φ \land (A \in V \land B \in V) \land (C \in V \land D \in V)) \to ((F (A) = F (C) \land F (B) = F (D)) \to F (A \underset{˙}{+} B) = F (C \underset{˙}{+} D))$