eroprf

Description: Functionality of an operation defined on equivalence classes. (Contributed by Jeff Madsen, 10-Jun-2010) (Revised by Mario Carneiro, 30-Dec-2014)

	Ref	Expression
Hypotheses	eropr.1	$⊢ J = A / R$
	eropr.2	$⊢ K = B / S$
	eropr.3	$⊢ φ \to T \in Z$
	eropr.4	$⊢ φ \to R Er U$
	eropr.5	$⊢ φ \to S Er V$
	eropr.6	$⊢ φ \to T Er W$
	eropr.7	$⊢ φ \to A \subseteq U$
	eropr.8	$⊢ φ \to B \subseteq V$
	eropr.9	$⊢ φ \to C \subseteq W$
	eropr.10	$⊢ φ \to \underset{˙}{+} : A \times B ⟶ C$
	eropr.11	$⊢ (φ \land ((r \in A \land s \in A) \land (t \in B \land u \in B))) \to ((r R s \land t S u) \to (r \underset{˙}{+} t) T (s \underset{˙}{+} u))$
	eropr.12	$⊢ \underset{˙}{⨣} = \{⟨⟨x, y⟩, z⟩ \| \exists p \in A \exists q \in B ((x = [p] R \land y = [q] S) \land z = [(p \underset{˙}{+} q)] T)\}$
	eropr.13	$⊢ φ \to R \in X$
	eropr.14	$⊢ φ \to S \in Y$
	eropr.15	$⊢ L = C / T$
Assertion	eroprf	$⊢ φ \to \underset{˙}{⨣} : J \times K ⟶ L$

Proof

Step	Hyp	Ref	Expression
1		eropr.1	$⊢ J = A / R$
2		eropr.2	$⊢ K = B / S$
3		eropr.3	$⊢ φ \to T \in Z$
4		eropr.4	$⊢ φ \to R Er U$
5		eropr.5	$⊢ φ \to S Er V$
6		eropr.6	$⊢ φ \to T Er W$
7		eropr.7	$⊢ φ \to A \subseteq U$
8		eropr.8	$⊢ φ \to B \subseteq V$
9		eropr.9	$⊢ φ \to C \subseteq W$
10		eropr.10	$⊢ φ \to \underset{˙}{+} : A \times B ⟶ C$
11		eropr.11	$⊢ (φ \land ((r \in A \land s \in A) \land (t \in B \land u \in B))) \to ((r R s \land t S u) \to (r \underset{˙}{+} t) T (s \underset{˙}{+} u))$
12		eropr.12	$⊢ \underset{˙}{⨣} = \{⟨⟨x, y⟩, z⟩ \| \exists p \in A \exists q \in B ((x = [p] R \land y = [q] S) \land z = [(p \underset{˙}{+} q)] T)\}$
13		eropr.13	$⊢ φ \to R \in X$
14		eropr.14	$⊢ φ \to S \in Y$
15		eropr.15	$⊢ L = C / T$
16	3	ad2antrr	$⊢ ((φ \land (x \in J \land y \in K)) \land (p \in A \land q \in B)) \to T \in Z$
17	10	adantr	$⊢ (φ \land (x \in J \land y \in K)) \to \underset{˙}{+} : A \times B ⟶ C$
18	17	fovrnda	$⊢ ((φ \land (x \in J \land y \in K)) \land (p \in A \land q \in B)) \to p \underset{˙}{+} q \in C$
19		ecelqsg	$⊢ (T \in Z \land p \underset{˙}{+} q \in C) \to [(p \underset{˙}{+} q)] T \in (C / T)$
20	16 18 19	syl2anc	$⊢ ((φ \land (x \in J \land y \in K)) \land (p \in A \land q \in B)) \to [(p \underset{˙}{+} q)] T \in (C / T)$
21	20 15	eleqtrrdi	$⊢ ((φ \land (x \in J \land y \in K)) \land (p \in A \land q \in B)) \to [(p \underset{˙}{+} q)] T \in L$
22		eleq1a	$⊢ [(p \underset{˙}{+} q)] T \in L \to (z = [(p \underset{˙}{+} q)] T \to z \in L)$
23	21 22	syl	$⊢ ((φ \land (x \in J \land y \in K)) \land (p \in A \land q \in B)) \to (z = [(p \underset{˙}{+} q)] T \to z \in L)$
24	23	adantld	$⊢ ((φ \land (x \in J \land y \in K)) \land (p \in A \land q \in B)) \to (((x = [p] R \land y = [q] S) \land z = [(p \underset{˙}{+} q)] T) \to z \in L)$
25	24	rexlimdvva	$⊢ (φ \land (x \in J \land y \in K)) \to (\exists p \in A \exists q \in B ((x = [p] R \land y = [q] S) \land z = [(p \underset{˙}{+} q)] T) \to z \in L)$
26	25	abssdv	$⊢ (φ \land (x \in J \land y \in K)) \to \{z \| \exists p \in A \exists q \in B ((x = [p] R \land y = [q] S) \land z = [(p \underset{˙}{+} q)] T)\} \subseteq L$
27	1 2 3 4 5 6 7 8 9 10 11	eroveu	$⊢ (φ \land (x \in J \land y \in K)) \to \exists! z \exists p \in A \exists q \in B ((x = [p] R \land y = [q] S) \land z = [(p \underset{˙}{+} q)] T)$
28		iotacl	$⊢ \exists! z \exists p \in A \exists q \in B ((x = [p] R \land y = [q] S) \land z = [(p \underset{˙}{+} q)] T) \to (ι z \| \exists p \in A \exists q \in B ((x = [p] R \land y = [q] S) \land z = [(p \underset{˙}{+} q)] T)) \in \{z \| \exists p \in A \exists q \in B ((x = [p] R \land y = [q] S) \land z = [(p \underset{˙}{+} q)] T)\}$
29	27 28	syl	$⊢ (φ \land (x \in J \land y \in K)) \to (ι z \| \exists p \in A \exists q \in B ((x = [p] R \land y = [q] S) \land z = [(p \underset{˙}{+} q)] T)) \in \{z \| \exists p \in A \exists q \in B ((x = [p] R \land y = [q] S) \land z = [(p \underset{˙}{+} q)] T)\}$
30	26 29	sseldd	$⊢ (φ \land (x \in J \land y \in K)) \to (ι z \| \exists p \in A \exists q \in B ((x = [p] R \land y = [q] S) \land z = [(p \underset{˙}{+} q)] T)) \in L$
31	30	ralrimivva	$⊢ φ \to \forall x \in J \forall y \in K (ι z \| \exists p \in A \exists q \in B ((x = [p] R \land y = [q] S) \land z = [(p \underset{˙}{+} q)] T)) \in L$
32		eqid	$⊢ (x \in J, y \in K ⟼ (ι z \| \exists p \in A \exists q \in B ((x = [p] R \land y = [q] S) \land z = [(p \underset{˙}{+} q)] T))) = (x \in J, y \in K ⟼ (ι z \| \exists p \in A \exists q \in B ((x = [p] R \land y = [q] S) \land z = [(p \underset{˙}{+} q)] T)))$
33	32	fmpo	$⊢ \forall x \in J \forall y \in K (ι z \| \exists p \in A \exists q \in B ((x = [p] R \land y = [q] S) \land z = [(p \underset{˙}{+} q)] T)) \in L \leftrightarrow (x \in J, y \in K ⟼ (ι z \| \exists p \in A \exists q \in B ((x = [p] R \land y = [q] S) \land z = [(p \underset{˙}{+} q)] T))) : J \times K ⟶ L$
34	31 33	sylib	$⊢ φ \to (x \in J, y \in K ⟼ (ι z \| \exists p \in A \exists q \in B ((x = [p] R \land y = [q] S) \land z = [(p \underset{˙}{+} q)] T))) : J \times K ⟶ L$
35	1 2 3 4 5 6 7 8 9 10 11 12	erovlem	$⊢ φ \to \underset{˙}{⨣} = (x \in J, y \in K ⟼ (ι z \| \exists p \in A \exists q \in B ((x = [p] R \land y = [q] S) \land z = [(p \underset{˙}{+} q)] T)))$
36	35	feq1d	$⊢ φ \to (\underset{˙}{⨣} : J \times K ⟶ L \leftrightarrow (x \in J, y \in K ⟼ (ι z \| \exists p \in A \exists q \in B ((x = [p] R \land y = [q] S) \land z = [(p \underset{˙}{+} q)] T))) : J \times K ⟶ L)$
37	34 36	mpbird	$⊢ φ \to \underset{˙}{⨣} : J \times K ⟶ L$

Metamath Proof Explorer

Theorem eroprf

Proof