eroprf2

Description: Functionality of an operation defined on equivalence classes. (Contributed by Jeff Madsen, 10-Jun-2010)

	Ref	Expression
Hypotheses	eropr2.1	$⊢ J = A / \underset{˙}{\sim}$
	eropr2.2	$⊢ \underset{˙}{⨣} = \{⟨⟨x, y⟩, z⟩ \| \exists p \in A \exists q \in A ((x = [p] \underset{˙}{\sim} \land y = [q] \underset{˙}{\sim}) \land z = [(p \underset{˙}{+} q)] \underset{˙}{\sim})\}$
	eropr2.3	$⊢ φ \to \underset{˙}{\sim} \in X$
	eropr2.4	$⊢ φ \to \underset{˙}{\sim} Er U$
	eropr2.5	$⊢ φ \to A \subseteq U$
	eropr2.6	$⊢ φ \to \underset{˙}{+} : A \times A ⟶ A$
	eropr2.7	$⊢ (φ \land ((r \in A \land s \in A) \land (t \in A \land u \in A))) \to ((r \underset{˙}{\sim} s \land t \underset{˙}{\sim} u) \to (r \underset{˙}{+} t) \underset{˙}{\sim} (s \underset{˙}{+} u))$
Assertion	eroprf2	$⊢ φ \to \underset{˙}{⨣} : J \times J ⟶ J$

Step	Hyp	Ref	Expression
1		eropr2.1	$⊢ J = A / \underset{˙}{\sim}$
2		eropr2.2	$⊢ \underset{˙}{⨣} = \{⟨⟨x, y⟩, z⟩ \| \exists p \in A \exists q \in A ((x = [p] \underset{˙}{\sim} \land y = [q] \underset{˙}{\sim}) \land z = [(p \underset{˙}{+} q)] \underset{˙}{\sim})\}$
3		eropr2.3	$⊢ φ \to \underset{˙}{\sim} \in X$
4		eropr2.4	$⊢ φ \to \underset{˙}{\sim} Er U$
5		eropr2.5	$⊢ φ \to A \subseteq U$
6		eropr2.6	$⊢ φ \to \underset{˙}{+} : A \times A ⟶ A$
7		eropr2.7	$⊢ (φ \land ((r \in A \land s \in A) \land (t \in A \land u \in A))) \to ((r \underset{˙}{\sim} s \land t \underset{˙}{\sim} u) \to (r \underset{˙}{+} t) \underset{˙}{\sim} (s \underset{˙}{+} u))$
8	1 1 3 4 4 4 5 5 5 6 7 2 3 3 1	eroprf	$⊢ φ \to \underset{˙}{⨣} : J \times J ⟶ J$

Metamath Proof Explorer