Theorem xpmapenlem5 3395

Description: Lemma for xpmapen 3396.

Hypotheses

Ref	Expression
xpmapen.1	⊢ A ∈ V
xpmapen.2	⊢ B ∈ V
xpmapen.3	⊢ C ∈ V
xpmapenlem.4	⊢ D = {⟨z, w⟩∣(z ∈ C ∧ w = ∪dom {(x ‘z)})}
xpmapenlem.5	⊢ R = {⟨z, w⟩∣(z ∈ C ∧ w = ∪ran {(x ‘z)})}
xpmapenlem.6	⊢ S = {⟨z, w⟩∣(z ∈ C ∧ w = ⟨(∪dom {y} ‘z), (∪ran {y} ‘z)⟩)}

Assertion

Ref	Expression
xpmapenlem5	⊢ ((A × B) ↑m C) ≈ ((A ↑m C) × (B ↑m C))

Distinct variable group(s):   x,y,z,w,A   x,B,y,z,w   x,C,y,z,w   y,D   y,R   x,S

Proof of Theorem xpmapenlem5

Step	Hyp	Ref	Expression
1		oprex 3018	. 2 ⊢ ((A × B) ↑m C) ∈ V
2		opex 1893	. . 3 ⊢ ⟨D, R⟩ ∈ V
3	2	a1i 7	. 2 ⊢ (x ∈ ((A × B) ↑m C) → ⟨D, R⟩ ∈ V)
4		xpmapenlem.6	. . . 4 ⊢ S = {⟨z, w⟩∣(z ∈ C ∧ w = ⟨(∪dom {y} ‘z), (∪ran {y} ‘z)⟩)}
5		xpmapen.3	. . . . 5 ⊢ C ∈ V
6		moeq 1431	. . . . . 6 ⊢ ∃*w w = ⟨(∪dom {y} ‘z), (∪ran {y} ‘z)⟩
7	6	a1i 7	. . . . 5 ⊢ (z ∈ C → ∃*w w = ⟨(∪dom {y} ‘z), (∪ran {y} ‘z)⟩)
8	5, 7	funopabex 2742	. . . 4 ⊢ {⟨z, w⟩∣(z ∈ C ∧ w = ⟨(∪dom {y} ‘z), (∪ran {y} ‘z)⟩)} ∈ V
9	4, 8	eqeltr 1159	. . 3 ⊢ S ∈ V
10	9	a1i 7	. 2 ⊢ (y ∈ ((A ↑m C) × (B ↑m C)) → S ∈ V)
11		xpmapenlem.4	. . . . . . . . . . . 12 ⊢ D = {⟨z, w⟩∣(z ∈ C ∧ w = ∪dom {(x ‘z)})}
12		moeq 1431	. . . . . . . . . . . . . 14 ⊢ ∃*w w = ∪dom {(x ‘z)}
13	12	a1i 7	. . . . . . . . . . . . 13 ⊢ (z ∈ C → ∃*w w = ∪dom {(x ‘z)})
14	5, 13	funopabex 2742	. . . . . . . . . . . 12 ⊢ {⟨z, w⟩∣(z ∈ C ∧ w = ∪dom {(x ‘z)})} ∈ V
15	11, 14	eqeltr 1159	. . . . . . . . . . 11 ⊢ D ∈ V
16		xpmapenlem.5	. . . . . . . . . . . 12 ⊢ R = {⟨z, w⟩∣(z ∈ C ∧ w = ∪ran {(x ‘z)})}
17		moeq 1431	. . . . . . . . . . . . . 14 ⊢ ∃*w w = ∪ran {(x ‘z)}
18	17	a1i 7	. . . . . . . . . . . . 13 ⊢ (z ∈ C → ∃*w w = ∪ran {(x ‘z)})
19	5, 18	funopabex 2742	. . . . . . . . . . . 12 ⊢ {⟨z, w⟩∣(z ∈ C ∧ w = ∪ran {(x ‘z)})} ∈ V
20	16, 19	eqeltr 1159	. . . . . . . . . . 11 ⊢ R ∈ V
21	15, 20	pm3.2i 234	. . . . . . . . . 10 ⊢ (D ∈ V ∧ R ∈ V)
22	20	opelxp 2452	. . . . . . . . . 10 ⊢ (⟨D, R⟩ ∈ (V × V) ↔ (D ∈ V ∧ R ∈ V))
23	21, 22	mpbir 165	. . . . . . . . 9 ⊢ ⟨D, R⟩ ∈ (V × V)
24		eleq1 1149	. . . . . . . . 9 ⊢ (y = ⟨D, R⟩ → (y ∈ (V × V) ↔ ⟨D, R⟩ ∈ (V × V)))
25	23, 24	mpbiri 169	. . . . . . . 8 ⊢ (y = ⟨D, R⟩ → y ∈ (V × V))
26	25	adantl 305	. . . . . . 7 ⊢ ((x:C–→(A × B) ∧ y = ⟨D, R⟩) → y ∈ (V × V))
27		elxp4 2640	. . . . . . . 8 ⊢ (y ∈ (V × V) ↔ (y = ⟨∪dom {y}, ∪ran {y}⟩ ∧ (∪dom {y} ∈ V ∧ ∪ran {y} ∈ V)))
28	27	pm3.26bd 259	. . . . . . 7 ⊢ (y ∈ (V × V) → y = ⟨∪dom {y}, ∪ran {y}⟩)
29	26, 28	syl 12	. . . . . 6 ⊢ ((x:C–→(A × B) ∧ y = ⟨D, R⟩) → y = ⟨∪dom {y}, ∪ran {y}⟩)
30		sneq 1816	. . . . . . . . . . . . . 14 ⊢ (y = ⟨D, R⟩ → {y} = {⟨D, R⟩})
31	30	dmeqd 2533	. . . . . . . . . . . . 13 ⊢ (y = ⟨D, R⟩ → dom {y} = dom {⟨D, R⟩})
32	31	unieqd 1929	. . . . . . . . . . . 12 ⊢ (y = ⟨D, R⟩ → ∪dom {y} = ∪dom {⟨D, R⟩})
33	15	op1sta 2635	. . . . . . . . . . . 12 ⊢ ∪dom {⟨D, R⟩} = D
34	32, 33	syl6eq 1140	. . . . . . . . . . 11 ⊢ (y = ⟨D, R⟩ → ∪dom {y} = D)
35		xpmapen.1	. . . . . . . . . . . . . . 15 ⊢ A ∈ V
36		xpmapen.2	. . . . . . . . . . . . . . 15 ⊢ B ∈ V
37	35, 36, 5, 11, 16, 4	xpmapenlem1 3391	. . . . . . . . . . . . . 14 ⊢ ((y = ⟨D, R⟩ → ∀z y = ⟨D, R⟩) ∧ (y = ⟨D, R⟩ → ∀w y = ⟨D, R⟩))
38	37	pm3.26i 257	. . . . . . . . . . . . 13 ⊢ (y = ⟨D, R⟩ → ∀z y = ⟨D, R⟩)
39	37	pm3.27i 261	. . . . . . . . . . . . 13 ⊢ (y = ⟨D, R⟩ → ∀w y = ⟨D, R⟩)
40	35, 36, 5, 11, 16, 4	xpmapenlem2 3392	. . . . . . . . . . . . . . . . 17 ⊢ ((y = ⟨D, R⟩ ∧ z ∈ C) → ((∪dom {y} ‘z) = ∪dom {(x ‘z)} ∧ (∪ran {y} ‘z) = ∪ran {(x ‘z)}))
41	40	pm3.26d 258	. . . . . . . . . . . . . . . 16 ⊢ ((y = ⟨D, R⟩ ∧ z ∈ C) → (∪dom {y} ‘z) = ∪dom {(x ‘z)})
42	41	cleq2d 1112	. . . . . . . . . . . . . . 15 ⊢ ((y = ⟨D, R⟩ ∧ z ∈ C) → (w = (∪dom {y} ‘z) ↔ w = ∪dom {(x ‘z)}))
43	42	exp 291	. . . . . . . . . . . . . 14 ⊢ (y = ⟨D, R⟩ → (z ∈ C → (w = (∪dom {y} ‘z) ↔ w = ∪dom {(x ‘z)})))
44	43	pm5.32d 491	. . . . . . . . . . . . 13 ⊢ (y = ⟨D, R⟩ → ((z ∈ C ∧ w = (∪dom {y} ‘z)) ↔ (z ∈ C ∧ w = ∪dom {(x ‘z)})))
45	38, 39, 44	biopabd 2101	. . . . . . . . . . . 12 ⊢ (y = ⟨D, R⟩ → {⟨z, w⟩∣(z ∈ C ∧ w = (∪dom {y} ‘z))} = {⟨z, w⟩∣(z ∈ C ∧ w = ∪dom {(x ‘z)})})
46	45, 11	syl6eqr 1142	. . . . . . . . . . 11 ⊢ (y = ⟨D, R⟩ → {⟨z, w⟩∣(z ∈ C ∧ w = (∪dom {y} ‘z))} = D)
47	34, 46	eqtr4d 1131	. . . . . . . . . 10 ⊢ (y = ⟨D, R⟩ → ∪dom {y} = {⟨z, w⟩∣(z ∈ C ∧ w = (∪dom {y} ‘z))})
48	30	rneqd 2557	. . . . . . . . . . . . 13 ⊢ (y = ⟨D, R⟩ → ran {y} = ran {⟨D, R⟩})
49	48	unieqd 1929	. . . . . . . . . . . 12 ⊢ (y = ⟨D, R⟩ → ∪ran {y} = ∪ran {⟨D, R⟩})
50	15, 20	op2nda 2639	. . . . . . . . . . . 12 ⊢ ∪ran {⟨D, R⟩} = R
51	49, 50	syl6eq 1140	. . . . . . . . . . 11 ⊢ (y = ⟨D, R⟩ → ∪ran {y} = R)
52	40	pm3.27d 262	. . . . . . . . . . . . . . . 16 ⊢ ((y = ⟨D, R⟩ ∧ z ∈ C) → (∪ran {y} ‘z) = ∪ran {(x ‘z)})
53	52	cleq2d 1112	. . . . . . . . . . . . . . 15 ⊢ ((y = ⟨D, R⟩ ∧ z ∈ C) → (w = (∪ran {y} ‘z) ↔ w = ∪ran {(x ‘z)}))
54	53	exp 291	. . . . . . . . . . . . . 14 ⊢ (y = ⟨D, R⟩ → (z ∈ C → (w = (∪ran {y} ‘z) ↔ w = ∪ran {(x ‘z)})))
55	54	pm5.32d 491	. . . . . . . . . . . . 13 ⊢ (y = ⟨D, R⟩ → ((z ∈ C ∧ w = (∪ran {y} ‘z)) ↔ (z ∈ C ∧ w = ∪ran {(x ‘z)})))
56	38, 39, 55	biopabd 2101	. . . . . . . . . . . 12 ⊢ (y = ⟨D, R⟩ → {⟨z, w⟩∣(z ∈ C ∧ w = (∪ran {y} ‘z))} = {⟨z, w⟩∣(z ∈ C ∧ w = ∪ran {(x ‘z)})})
57	56, 16	syl6eqr 1142	. . . . . . . . . . 11 ⊢ (y = ⟨D, R⟩ → {⟨z, w⟩∣(z ∈ C ∧ w = (∪ran {y} ‘z))} = R)
58	51, 57	eqtr4d 1131	. . . . . . . . . 10 ⊢ (y = ⟨D, R⟩ → ∪ran {y} = {⟨z, w⟩∣(z ∈ C ∧ w = (∪ran {y} ‘z))})
59	47, 58	jca 236	. . . . . . . . 9 ⊢ (y = ⟨D, R⟩ → (∪dom {y} = {⟨z, w⟩∣(z ∈ C ∧ w = (∪dom {y} ‘z))} ∧ ∪ran {y} = {⟨z, w⟩∣(z ∈ C ∧ w = (∪ran {y} ‘z))}))
60	59	adantl 305	. . . . . . . 8 ⊢ ((x:C–→(A × B) ∧ y = ⟨D, R⟩) → (∪dom {y} = {⟨z, w⟩∣(z ∈ C ∧ w = (∪dom {y} ‘z))} ∧ ∪ran {y} = {⟨z, w⟩∣(z ∈ C ∧ w = (∪ran {y} ‘z))}))
61		ffvrn 2890	. . . . . . . . . . . 12 ⊢ ((x:C–→(A × B) ∧ z ∈ C) → (x ‘z) ∈ (A × B))
62	61	exp 291	. . . . . . . . . . 11 ⊢ (x:C–→(A × B) → (z ∈ C → (x ‘z) ∈ (A × B)))
63	62	r19.21aiv 1259	. . . . . . . . . 10 ⊢ (x:C–→(A × B) → ∀z ∈ C (x ‘z) ∈ (A × B))
64	63	adantr 306	. . . . . . . . 9 ⊢ ((x:C–→(A × B) ∧ y = ⟨D, R⟩) → ∀z ∈ C (x ‘z) ∈ (A × B))
65		ax-17 925	. . . . . . . . . . . 12 ⊢ (x:C–→(A × B) → ∀z x:C–→(A × B))
66	65, 38	hban 704	. . . . . . . . . . 11 ⊢ ((x:C–→(A × B) ∧ y = ⟨D, R⟩) → ∀z(x:C–→(A × B) ∧ y = ⟨D, R⟩))
67	35, 36, 5, 11, 16, 4	xpmapenlem3 3393	. . . . . . . . . . . . . . 15 ⊢ ((x:C–→(A × B) ∧ y = ⟨D, R⟩) → x = S)
68	67	fveq1d 2834	. . . . . . . . . . . . . 14 ⊢ ((x:C–→(A × B) ∧ y = ⟨D, R⟩) → (x ‘z) = (S ‘z))
69		opex 1893	. . . . . . . . . . . . . . . 16 ⊢ ⟨(∪dom {y} ‘z), (∪ran {y} ‘z)⟩ ∈ V
70		fvopab2 2878	. . . . . . . . . . . . . . . 16 ⊢ ((z ∈ C ∧ ⟨(∪dom {y} ‘z), (∪ran {y} ‘z)⟩ ∈ V) → ({⟨z, w⟩∣(z ∈ C ∧ w = ⟨(∪dom {y} ‘z), (∪ran {y} ‘z)⟩)} ‘z) = ⟨(∪dom {y} ‘z), (∪ran {y} ‘z)⟩)
71	69, 70	mpan2 519	. . . . . . . . . . . . . . 15 ⊢ (z ∈ C → ({⟨z, w⟩∣(z ∈ C ∧ w = ⟨(∪dom {y} ‘z), (∪ran {y} ‘z)⟩)} ‘z) = ⟨(∪dom {y} ‘z), (∪ran {y} ‘z)⟩)
72	4	fveq1i 2833	. . . . . . . . . . . . . . 15 ⊢ (S ‘z) = ({⟨z, w⟩∣(z ∈ C ∧ w = ⟨(∪dom {y} ‘z), (∪ran {y} ‘z)⟩)} ‘z)
73	71, 72	syl5eq 1136	. . . . . . . . . . . . . 14 ⊢ (z ∈ C → (S ‘z) = ⟨(∪dom {y} ‘z), (∪ran {y} ‘z)⟩)
74	68, 73	sylan9eq 1144	. . . . . . . . . . . . 13 ⊢ (((x:C–→(A × B) ∧ y = ⟨D, R⟩) ∧ z ∈ C) → (x ‘z) = ⟨(∪dom {y} ‘z), (∪ran {y} ‘z)⟩)
75	74	eleq1d 1155	. . . . . . . . . . . 12 ⊢ (((x:C–→(A × B) ∧ y = ⟨D, R⟩) ∧ z ∈ C) → ((x ‘z) ∈ (A × B) ↔ ⟨(∪dom {y} ‘z), (∪ran {y} ‘z)⟩ ∈ (A × B)))
76		fvex 2838	. . . . . . . . . . . . 13 ⊢ (∪ran {y} ‘z) ∈ V
77	76	opelxp 2452	. . . . . . . . . . . 12 ⊢ (⟨(∪dom {y} ‘z), (∪ran {y} ‘z)⟩ ∈ (A × B) ↔ ((∪dom {y} ‘z) ∈ A ∧ (∪ran {y} ‘z) ∈ B))
78	75, 77	syl6bb 414	. . . . . . . . . . 11 ⊢ (((x:C–→(A × B) ∧ y = ⟨D, R⟩) ∧ z ∈ C) → ((x ‘z) ∈ (A × B) ↔ ((∪dom {y} ‘z) ∈ A ∧ (∪ran {y} ‘z) ∈ B)))
79	66, 78	biralda 1213	. . . . . . . . . 10 ⊢ ((x:C–→(A × B) ∧ y = ⟨D, R⟩) → (∀z ∈ C (x ‘z) ∈ (A × B) ↔ ∀z ∈ C ((∪dom {y} ‘z) ∈ A ∧ (∪ran {y} ‘z) ∈ B)))
80		r19.26 1289	. . . . . . . . . 10 ⊢ (∀z ∈ C ((∪dom {y} ‘z) ∈ A ∧ (∪ran {y} ‘z) ∈ B) ↔ (∀z ∈ C (∪dom {y} ‘z) ∈ A ∧ ∀z ∈ C (∪ran {y} ‘z) ∈ B))
81	79, 80	syl6bb 414	. . . . . . . . 9 ⊢ ((x:C–→(A × B) ∧ y = ⟨D, R⟩) → (∀z ∈ C (x ‘z) ∈ (A × B) ↔ (∀z ∈ C (∪dom {y} ‘z) ∈ A ∧ ∀z ∈ C (∪ran {y} ‘z) ∈ B)))
82	64, 81	mpbid 170	. . . . . . . 8 ⊢ ((x:C–→(A × B) ∧ y = ⟨D, R⟩) → (∀z ∈ C (∪dom {y} ‘z) ∈ A ∧ ∀z ∈ C (∪ran {y} ‘z) ∈ B))
83	60, 82	jca 236	. . . . . . 7 ⊢ ((x:C–→(A × B) ∧ y = ⟨D, R⟩) → ((∪dom {y} = {⟨z, w⟩∣(z ∈ C ∧ w = (∪dom {y} ‘z))} ∧ ∪ran {y} = {⟨z, w⟩∣(z ∈ C ∧ w = (∪ran {y} ‘z))}) ∧ (∀z ∈ C (∪dom {y} ‘z) ∈ A ∧ ∀z ∈ C (∪ran {y} ‘z) ∈ B)))
84		an4 388	. . . . . . . 8 ⊢ (((∪dom {y} = {⟨z, w⟩∣(z ∈ C ∧ w = (∪dom {y} ‘z))} ∧ ∪ran {y} = {⟨z, w⟩∣(z ∈ C ∧ w = (∪ran {y} ‘z))}) ∧ (∀z ∈ C (∪dom {y} ‘z) ∈ A ∧ ∀z ∈ C (∪ran {y} ‘z) ∈ B)) ↔ ((∪dom {y} = {⟨z, w⟩∣(z ∈ C ∧ w = (∪dom {y} ‘z))} ∧ ∀z ∈ C (∪dom {y} ‘z) ∈ A) ∧ (∪ran {y} = {⟨z, w⟩∣(z ∈ C ∧ w = (∪ran {y} ‘z))} ∧ ∀z ∈ C (∪ran {y} ‘z) ∈ B)))
85		fopabfv 2894	. . . . . . . . 9 ⊢ (∪dom {y}:C–→A ↔ (∪dom {y} = {⟨z, w⟩∣(z ∈ C ∧ w = (∪dom {y} ‘z))} ∧ ∀z ∈ C (∪dom {y} ‘z) ∈ A))
86		fopabfv 2894	. . . . . . . . 9 ⊢ (∪ran {y}:C–→B ↔ (∪ran {y} = {⟨z, w⟩∣(z ∈ C ∧ w = (∪ran {y} ‘z))} ∧ ∀z ∈ C (∪ran {y} ‘z) ∈ B))
87	85, 86	anbi12i 369	. . . . . . . 8 ⊢ ((∪dom {y}:C–→A ∧ ∪ran {y}:C–→B) ↔ ((∪dom {y} = {⟨z, w⟩∣(z ∈ C ∧ w = (∪dom {y} ‘z))} ∧ ∀z ∈ C (∪dom {y} ‘z) ∈ A) ∧ (∪ran {y} = {⟨z, w⟩∣(z ∈ C ∧ w = (∪ran {y} ‘z))} ∧ ∀z ∈ C (∪ran {y} ‘z) ∈ B)))
88	84, 87	bitr4 154	. . . . . . 7 ⊢ (((∪dom {y} = {⟨z, w⟩∣(z ∈ C ∧ w = (∪dom {y} ‘z))} ∧ ∪ran {y} = {⟨z, w⟩∣(z ∈ C ∧ w = (∪ran {y} ‘z))}) ∧ (∀z ∈ C (∪dom {y} ‘z) ∈ A ∧ ∀z ∈ C (∪ran {y} ‘z) ∈ B)) ↔ (∪dom {y}:C–→A ∧ ∪ran {y}:C–→B))
89	83, 88	sylib 173	. . . . . 6 ⊢ ((x:C–→(A × B) ∧ y = ⟨D, R⟩) → (∪dom {y}:C–→A ∧ ∪ran {y}:C–→B))
90	29, 89	jca 236	. . . . 5 ⊢ ((x:C–→(A × B) ∧ y = ⟨D, R⟩) → (y = ⟨∪dom {y}, ∪ran {y}⟩ ∧ (∪dom {y}:C–→A ∧ ∪ran {y}:C–→B)))
91	90, 67	jca 236	. . . 4 ⊢ ((x:C–→(A × B) ∧ y = ⟨D, R⟩) → ((y = ⟨∪dom {y}, ∪ran {y}⟩ ∧ (∪dom {y}:C–→A ∧ ∪ran {y}:C–→B)) ∧ x = S))
92	35, 36, 5, 11, 16, 4	xpmapenlem4 3394	. . . 4 ⊢ (((y = ⟨∪dom {y}, ∪ran {y}⟩ ∧ (∪dom {y}:C–→A ∧ ∪ran {y}:C–→B)) ∧ x = S) → (x:C–→(A × B) ∧ y = ⟨D, R⟩))
93	91, 92	impbi 139	. . 3 ⊢ ((x:C–→(A × B) ∧ y = ⟨D, R⟩) ↔ ((y = ⟨∪dom {y}, ∪ran {y}⟩ ∧ (∪dom {y}:C–→A ∧ ∪ran {y}:C–→B)) ∧ x = S))
94	35, 36	xpex 2488	. . . . 5 ⊢ (A × B) ∈ V
95	94, 5	elmap 3265	. . . 4 ⊢ (x ∈ ((A × B) ↑m C) ↔ x:C–→(A × B))
96	95	anbi1i 368	. . 3 ⊢ ((x ∈ ((A × B) ↑m C) ∧ y = ⟨D, R⟩) ↔ (x:C–→(A × B) ∧ y = ⟨D, R⟩))
97		elxp4 2640	. . . . 5 ⊢ (y ∈ ((A ↑m C) × (B ↑m C)) ↔ (y = ⟨∪dom {y}, ∪ran {y}⟩ ∧ (∪dom {y} ∈ (A ↑m C) ∧ ∪ran {y} ∈ (B ↑m C))))
98	35, 5	elmap 3265	. . . . . . 7 ⊢ (∪dom {y} ∈ (A ↑m C) ↔ ∪dom {y}:C–→A)
99	36, 5	elmap 3265	. . . . . . 7 ⊢ (∪ran {y} ∈ (B ↑m C) ↔ ∪ran {y}:C–→B)
100	98, 99	anbi12i 369	. . . . . 6 ⊢ ((∪dom {y} ∈ (A ↑m C) ∧ ∪ran {y} ∈ (B ↑m C)) ↔ (∪dom {y}:C–→A ∧ ∪ran {y}:C–→B))
101	100	anbi2i 367	. . . . 5 ⊢ ((y = ⟨∪dom {y}, ∪ran {y}⟩ ∧ (∪dom {y} ∈ (A ↑m C) ∧ ∪ran {y} ∈ (B ↑m C))) ↔ (y = ⟨∪dom {y}, ∪ran {y}⟩ ∧ (∪dom {y}:C–→A ∧ ∪ran {y}:C–→B)))
102	97, 101	bitr 151	. . . 4 ⊢ (y ∈ ((A ↑m C) × (B ↑m C)) ↔ (y = ⟨∪dom {y}, ∪ran {y}⟩ ∧ (∪dom {y}:C–→A ∧ ∪ran {y}:C–→B)))
103	102	anbi1i 368	. . 3 ⊢ ((y ∈ ((A ↑m C) × (B ↑m C)) ∧ x = S) ↔ ((y = ⟨∪dom {y}, ∪ran {y}⟩ ∧ (∪dom {y}:C–→A ∧ ∪ran {y}:C–→B)) ∧ x = S))
104	93, 96, 103	3bitr4 158	. 2 ⊢ ((x ∈ ((A × B) ↑m C) ∧ y = ⟨D, R⟩) ↔ (y ∈ ((A ↑m C) × (B ↑m C)) ∧ x = S))
105	1, 3, 10, 104	en2 3305	1 ⊢ ((A × B) ↑m C) ≈ ((A ↑m C) × (B ↑m C))

Syntax hints:   → wi 2   ↔ wb 127   ∧ wa 196  ∀wal 672  ∃*wmo 1008   = wceq 1091   ∈ wcel 1092  ∀wral 1201  Vcvv 1348  {csn 1808  ⟨cop 1810  ∪cuni 1919   class class class wbr 2054  {copab 2055   × cxp 2408  dom cdm 2410  ran crn 2411  –→wf 2418   ‘cfv 2422  (class class class)co 3001   ↑_m cm 3258   ≈ cen 3271

This theorem is referenced by:  xpmapen 3396

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-un 1076  ax-pow 1077

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-3an 583  df-ex 679  df-sb 853  df-eu 1009  df-mo 1010  df-clab 1093  df-cleq 1097  df-clel 1099  df-ral 1205  df-rex 1206  df-v 1349  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-nul 1708  df-pw 1799  df-sn 1811  df-pr 1812  df-op 1815  df-uni 1920  df-br 2063  df-opab 2098  df-id 2125  df-xp 2424  df-rel 2425  df-cnv 2426  df-co 2427  df-dm 2428  df-rn 2429  df-res 2430  df-ima 2431  df-fun 2432  df-fn 2433  df-f 2434  df-f1 2435  df-fo 2436  df-f1o 2437  df-fv 2438  df-opr 3003  df-oprab 3004  df-map 3259  df-en 3274

metamath.org