erovlem

	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)\}$
Assertion	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)))$

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		simpl	$⊢ ((x = [p] R \land y = [q] S) \land z = [(p \underset{˙}{+} q)] T) \to (x = [p] R \land y = [q] S)$
14	13	reximi	$⊢ \exists q \in B ((x = [p] R \land y = [q] S) \land z = [(p \underset{˙}{+} q)] T) \to \exists q \in B (x = [p] R \land y = [q] S)$
15	14	reximi	$⊢ \exists p \in A \exists q \in B ((x = [p] R \land y = [q] S) \land z = [(p \underset{˙}{+} q)] T) \to \exists p \in A \exists q \in B (x = [p] R \land y = [q] S)$
16	1	eleq2i	$⊢ x \in J \leftrightarrow x \in (A / R)$
17		vex	$⊢ x \in V$
18	17	elqs	$⊢ x \in (A / R) \leftrightarrow \exists p \in A x = [p] R$
19	16 18	bitri	$⊢ x \in J \leftrightarrow \exists p \in A x = [p] R$
20	2	eleq2i	$⊢ y \in K \leftrightarrow y \in (B / S)$
21		vex	$⊢ y \in V$
22	21	elqs	$⊢ y \in (B / S) \leftrightarrow \exists q \in B y = [q] S$
23	20 22	bitri	$⊢ y \in K \leftrightarrow \exists q \in B y = [q] S$
24	19 23	anbi12i	$⊢ (x \in J \land y \in K) \leftrightarrow (\exists p \in A x = [p] R \land \exists q \in B y = [q] S)$
25		reeanv	$⊢ \exists p \in A \exists q \in B (x = [p] R \land y = [q] S) \leftrightarrow (\exists p \in A x = [p] R \land \exists q \in B y = [q] S)$
26	24 25	bitr4i	$⊢ (x \in J \land y \in K) \leftrightarrow \exists p \in A \exists q \in B (x = [p] R \land y = [q] S)$
27	15 26	sylibr	$⊢ \exists p \in A \exists q \in B ((x = [p] R \land y = [q] S) \land z = [(p \underset{˙}{+} q)] T) \to (x \in J \land y \in K)$
28	27	pm4.71ri	$⊢ \exists p \in A \exists q \in B ((x = [p] R \land y = [q] S) \land z = [(p \underset{˙}{+} q)] T) \leftrightarrow ((x \in J \land y \in K) \land \exists p \in A \exists q \in B ((x = [p] R \land y = [q] S) \land z = [(p \underset{˙}{+} q)] T))$
29	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)$
30		iota1	$⊢ \exists! z \exists p \in A \exists q \in B ((x = [p] R \land y = [q] S) \land z = [(p \underset{˙}{+} q)] T) \to (\exists p \in A \exists q \in B ((x = [p] R \land y = [q] S) \land z = [(p \underset{˙}{+} q)] T) \leftrightarrow (ι z \| \exists p \in A \exists q \in B ((x = [p] R \land y = [q] S) \land z = [(p \underset{˙}{+} q)] T)) = z)$
31	29 30	syl	$⊢ (φ \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) \leftrightarrow (ι z \| \exists p \in A \exists q \in B ((x = [p] R \land y = [q] S) \land z = [(p \underset{˙}{+} q)] T)) = z)$
32		eqcom	$⊢ (ι z \| \exists p \in A \exists q \in B ((x = [p] R \land y = [q] S) \land z = [(p \underset{˙}{+} q)] T)) = z \leftrightarrow z = (ι z \| \exists p \in A \exists q \in B ((x = [p] R \land y = [q] S) \land z = [(p \underset{˙}{+} q)] T))$
33	31 32	bitrdi	$⊢ (φ \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) \leftrightarrow z = (ι z \| \exists p \in A \exists q \in B ((x = [p] R \land y = [q] S) \land z = [(p \underset{˙}{+} q)] T)))$
34	33	pm5.32da	$⊢ φ \to (((x \in J \land y \in K) \land \exists p \in A \exists q \in B ((x = [p] R \land y = [q] S) \land z = [(p \underset{˙}{+} q)] T)) \leftrightarrow ((x \in J \land y \in K) \land z = (ι z \| \exists p \in A \exists q \in B ((x = [p] R \land y = [q] S) \land z = [(p \underset{˙}{+} q)] T))))$
35	28 34	bitrid	$⊢ φ \to (\exists p \in A \exists q \in B ((x = [p] R \land y = [q] S) \land z = [(p \underset{˙}{+} q)] T) \leftrightarrow ((x \in J \land y \in K) \land z = (ι z \| \exists p \in A \exists q \in B ((x = [p] R \land y = [q] S) \land z = [(p \underset{˙}{+} q)] T))))$
36	35	oprabbidv	$⊢ φ \to \{⟨⟨x, y⟩, z⟩ \| \exists p \in A \exists q \in B ((x = [p] R \land y = [q] S) \land z = [(p \underset{˙}{+} q)] T)\} = \{⟨⟨x, y⟩, z⟩ \| ((x \in J \land y \in K) \land z = (ι z \| \exists p \in A \exists q \in B ((x = [p] R \land y = [q] S) \land z = [(p \underset{˙}{+} q)] T)))\}$
37		df-mpo	$⊢ (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, y⟩, w⟩ \| ((x \in J \land y \in K) \land w = (ι z \| \exists p \in A \exists q \in B ((x = [p] R \land y = [q] S) \land z = [(p \underset{˙}{+} q)] T)))\}$
38		nfv	$⊢ Ⅎ w ((x \in J \land y \in K) \land z = (ι z \| \exists p \in A \exists q \in B ((x = [p] R \land y = [q] S) \land z = [(p \underset{˙}{+} q)] T)))$
39		nfv	$⊢ Ⅎ z (x \in J \land y \in K)$
40		nfiota1	$⊢ \underline{Ⅎ} z (ι z \| \exists p \in A \exists q \in B ((x = [p] R \land y = [q] S) \land z = [(p \underset{˙}{+} q)] T))$
41	40	nfeq2	$⊢ Ⅎ z w = (ι z \| \exists p \in A \exists q \in B ((x = [p] R \land y = [q] S) \land z = [(p \underset{˙}{+} q)] T))$
42	39 41	nfan	$⊢ Ⅎ z ((x \in J \land y \in K) \land w = (ι z \| \exists p \in A \exists q \in B ((x = [p] R \land y = [q] S) \land z = [(p \underset{˙}{+} q)] T)))$
43		eqeq1	$⊢ z = w \to (z = (ι z \| \exists p \in A \exists q \in B ((x = [p] R \land y = [q] S) \land z = [(p \underset{˙}{+} q)] T)) \leftrightarrow w = (ι z \| \exists p \in A \exists q \in B ((x = [p] R \land y = [q] S) \land z = [(p \underset{˙}{+} q)] T)))$
44	43	anbi2d	$⊢ z = w \to (((x \in J \land y \in K) \land z = (ι z \| \exists p \in A \exists q \in B ((x = [p] R \land y = [q] S) \land z = [(p \underset{˙}{+} q)] T))) \leftrightarrow ((x \in J \land y \in K) \land w = (ι z \| \exists p \in A \exists q \in B ((x = [p] R \land y = [q] S) \land z = [(p \underset{˙}{+} q)] T))))$
45	38 42 44	cbvoprab3	$⊢ \{⟨⟨x, y⟩, z⟩ \| ((x \in J \land y \in K) \land z = (ι z \| \exists p \in A \exists q \in B ((x = [p] R \land y = [q] S) \land z = [(p \underset{˙}{+} q)] T)))\} = \{⟨⟨x, y⟩, w⟩ \| ((x \in J \land y \in K) \land w = (ι z \| \exists p \in A \exists q \in B ((x = [p] R \land y = [q] S) \land z = [(p \underset{˙}{+} q)] T)))\}$
46	37 45	eqtr4i	$⊢ (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, y⟩, z⟩ \| ((x \in J \land y \in K) \land z = (ι z \| \exists p \in A \exists q \in B ((x = [p] R \land y = [q] S) \land z = [(p \underset{˙}{+} q)] T)))\}$
47	36 12 46	3eqtr4g	$⊢ φ \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)))$

Metamath Proof Explorer

Theorem erovlem

Proof