Theorem mapxpen 3390

Description: Equinumerosity law for double set exponentiation. Proposition 10.45 of [TakeutiZaring] p. 96.

Hypotheses

Ref	Expression
mapxpen.1	⊢ A ∈ V
mapxpen.2	⊢ B ∈ V
mapxpen.3	⊢ C ∈ V

Assertion

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

Proof of Theorem mapxpen

Step	Hyp	Ref	Expression
1		oprex 3018	. 2 ⊢ ((A ↑m B) ↑m C) ∈ V
2		mapxpen.2	. . . 4 ⊢ B ∈ V
3		mapxpen.3	. . . 4 ⊢ C ∈ V
4		cleqid 1102	. . . 4 ⊢ {⟨⟨z, w⟩, v⟩∣((z ∈ B ∧ w ∈ C) ∧ v = ((x ‘w) ‘z))} = {⟨⟨z, w⟩, v⟩∣((z ∈ B ∧ w ∈ C) ∧ v = ((x ‘w) ‘z))}
5	2, 3, 4	oprabex2 3045	. . 3 ⊢ {⟨⟨z, w⟩, v⟩∣((z ∈ B ∧ w ∈ C) ∧ v = ((x ‘w) ‘z))} ∈ V
6	5	a1i 7	. 2 ⊢ (x ∈ ((A ↑m B) ↑m C) → {⟨⟨z, w⟩, v⟩∣((z ∈ B ∧ w ∈ C) ∧ v = ((x ‘w) ‘z))} ∈ V)
7		moeq 1431	. . . . 5 ⊢ ∃*f f = {⟨z, g⟩∣(z ∈ B ∧ g = (zyw))}
8	7	a1i 7	. . . 4 ⊢ (w ∈ C → ∃*f f = {⟨z, g⟩∣(z ∈ B ∧ g = (zyw))})
9	3, 8	funopabex 2742	. . 3 ⊢ {⟨w, f⟩∣(w ∈ C ∧ f = {⟨z, g⟩∣(z ∈ B ∧ g = (zyw))})} ∈ V
10	9	a1i 7	. 2 ⊢ (y ∈ (A ↑m (B × C)) → {⟨w, f⟩∣(w ∈ C ∧ f = {⟨z, g⟩∣(z ∈ B ∧ g = (zyw))})} ∈ V)
11		fvex 2838	. . . . . . . . 9 ⊢ ((x ‘w) ‘z) ∈ V
12	11, 4	fnoprab2 3039	. . . . . . . 8 ⊢ {⟨⟨z, w⟩, v⟩∣((z ∈ B ∧ w ∈ C) ∧ v = ((x ‘w) ‘z))} Fn (B × C)
13		fneq1 2718	. . . . . . . 8 ⊢ (y = {⟨⟨z, w⟩, v⟩∣((z ∈ B ∧ w ∈ C) ∧ v = ((x ‘w) ‘z))} → (y Fn (B × C) ↔ {⟨⟨z, w⟩, v⟩∣((z ∈ B ∧ w ∈ C) ∧ v = ((x ‘w) ‘z))} Fn (B × C)))
14	12, 13	mpbiri 169	. . . . . . 7 ⊢ (y = {⟨⟨z, w⟩, v⟩∣((z ∈ B ∧ w ∈ C) ∧ v = ((x ‘w) ‘z))} → y Fn (B × C))
15	14	adantl 305	. . . . . 6 ⊢ ((x ∈ ((A ↑m B) ↑m C) ∧ y = {⟨⟨z, w⟩, v⟩∣((z ∈ B ∧ w ∈ C) ∧ v = ((x ‘w) ‘z))}) → y Fn (B × C))
16		ax-17 925	. . . . . . . 8 ⊢ (x ∈ ((A ↑m B) ↑m C) → ∀z x ∈ ((A ↑m B) ↑m C))
17		hboprab1 3023	. . . . . . . . 9 ⊢ (y ∈ {⟨⟨z, w⟩, v⟩∣((z ∈ B ∧ w ∈ C) ∧ v = ((x ‘w) ‘z))} → ∀z y ∈ {⟨⟨z, w⟩, v⟩∣((z ∈ B ∧ w ∈ C) ∧ v = ((x ‘w) ‘z))})
18	17	hbeleq 1173	. . . . . . . 8 ⊢ (y = {⟨⟨z, w⟩, v⟩∣((z ∈ B ∧ w ∈ C) ∧ v = ((x ‘w) ‘z))} → ∀z y = {⟨⟨z, w⟩, v⟩∣((z ∈ B ∧ w ∈ C) ∧ v = ((x ‘w) ‘z))})
19	16, 18	hban 704	. . . . . . 7 ⊢ ((x ∈ ((A ↑m B) ↑m C) ∧ y = {⟨⟨z, w⟩, v⟩∣((z ∈ B ∧ w ∈ C) ∧ v = ((x ‘w) ‘z))}) → ∀z(x ∈ ((A ↑m B) ↑m C) ∧ y = {⟨⟨z, w⟩, v⟩∣((z ∈ B ∧ w ∈ C) ∧ v = ((x ‘w) ‘z))}))
20		ax-17 925	. . . . . . . . 9 ⊢ (x ∈ ((A ↑m B) ↑m C) → ∀w x ∈ ((A ↑m B) ↑m C))
21		hboprab2 3024	. . . . . . . . . 10 ⊢ (y ∈ {⟨⟨z, w⟩, v⟩∣((z ∈ B ∧ w ∈ C) ∧ v = ((x ‘w) ‘z))} → ∀w y ∈ {⟨⟨z, w⟩, v⟩∣((z ∈ B ∧ w ∈ C) ∧ v = ((x ‘w) ‘z))})
22	21	hbeleq 1173	. . . . . . . . 9 ⊢ (y = {⟨⟨z, w⟩, v⟩∣((z ∈ B ∧ w ∈ C) ∧ v = ((x ‘w) ‘z))} → ∀w y = {⟨⟨z, w⟩, v⟩∣((z ∈ B ∧ w ∈ C) ∧ v = ((x ‘w) ‘z))})
23	20, 22	hban 704	. . . . . . . 8 ⊢ ((x ∈ ((A ↑m B) ↑m C) ∧ y = {⟨⟨z, w⟩, v⟩∣((z ∈ B ∧ w ∈ C) ∧ v = ((x ‘w) ‘z))}) → ∀w(x ∈ ((A ↑m B) ↑m C) ∧ y = {⟨⟨z, w⟩, v⟩∣((z ∈ B ∧ w ∈ C) ∧ v = ((x ‘w) ‘z))}))
24		ax-17 925	. . . . . . . 8 ⊢ (z ∈ B → ∀w z ∈ B)
25		ffvrn 2890	. . . . . . . . . . . . . . 15 ⊢ (((x ‘w):B–→A ∧ z ∈ B) → ((x ‘w) ‘z) ∈ A)
26		mapxpen.1	. . . . . . . . . . . . . . . 16 ⊢ A ∈ V
27	26, 2	elmap 3265	. . . . . . . . . . . . . . 15 ⊢ ((x ‘w) ∈ (A ↑m B) ↔ (x ‘w):B–→A)
28	25, 27	sylanb 344	. . . . . . . . . . . . . 14 ⊢ (((x ‘w) ∈ (A ↑m B) ∧ z ∈ B) → ((x ‘w) ‘z) ∈ A)
29		ffvrn 2890	. . . . . . . . . . . . . . 15 ⊢ ((x:C–→(A ↑m B) ∧ w ∈ C) → (x ‘w) ∈ (A ↑m B))
30		oprex 3018	. . . . . . . . . . . . . . . 16 ⊢ (A ↑m B) ∈ V
31	30, 3	elmap 3265	. . . . . . . . . . . . . . 15 ⊢ (x ∈ ((A ↑m B) ↑m C) ↔ x:C–→(A ↑m B))
32	29, 31	sylanb 344	. . . . . . . . . . . . . 14 ⊢ ((x ∈ ((A ↑m B) ↑m C) ∧ w ∈ C) → (x ‘w) ∈ (A ↑m B))
33	28, 32	sylan 343	. . . . . . . . . . . . 13 ⊢ (((x ∈ ((A ↑m B) ↑m C) ∧ w ∈ C) ∧ z ∈ B) → ((x ‘w) ‘z) ∈ A)
34	33	an1rs 373	. . . . . . . . . . . 12 ⊢ (((x ∈ ((A ↑m B) ↑m C) ∧ z ∈ B) ∧ w ∈ C) → ((x ‘w) ‘z) ∈ A)
35	34	anasss 337	. . . . . . . . . . 11 ⊢ ((x ∈ ((A ↑m B) ↑m C) ∧ (z ∈ B ∧ w ∈ C)) → ((x ‘w) ‘z) ∈ A)
36	35	adantlr 310	. . . . . . . . . 10 ⊢ (((x ∈ ((A ↑m B) ↑m C) ∧ y = {⟨⟨z, w⟩, v⟩∣((z ∈ B ∧ w ∈ C) ∧ v = ((x ‘w) ‘z))}) ∧ (z ∈ B ∧ w ∈ C)) → ((x ‘w) ‘z) ∈ A)
37		opreq 3005	. . . . . . . . . . . . 13 ⊢ (y = {⟨⟨z, w⟩, v⟩∣((z ∈ B ∧ w ∈ C) ∧ v = ((x ‘w) ‘z))} → (zyw) = (z{⟨⟨z, w⟩, v⟩∣((z ∈ B ∧ w ∈ C) ∧ v = ((x ‘w) ‘z))}w))
38	4	oprabval4g 3053	. . . . . . . . . . . . . 14 ⊢ ((z ∈ B ∧ w ∈ C ∧ ((x ‘w) ‘z) ∈ V) → (z{⟨⟨z, w⟩, v⟩∣((z ∈ B ∧ w ∈ C) ∧ v = ((x ‘w) ‘z))}w) = ((x ‘w) ‘z))
39	11, 38	mp3an3 641	. . . . . . . . . . . . 13 ⊢ ((z ∈ B ∧ w ∈ C) → (z{⟨⟨z, w⟩, v⟩∣((z ∈ B ∧ w ∈ C) ∧ v = ((x ‘w) ‘z))}w) = ((x ‘w) ‘z))
40	37, 39	sylan9eq 1144	. . . . . . . . . . . 12 ⊢ ((y = {⟨⟨z, w⟩, v⟩∣((z ∈ B ∧ w ∈ C) ∧ v = ((x ‘w) ‘z))} ∧ (z ∈ B ∧ w ∈ C)) → (zyw) = ((x ‘w) ‘z))
41	40	eleq1d 1155	. . . . . . . . . . 11 ⊢ ((y = {⟨⟨z, w⟩, v⟩∣((z ∈ B ∧ w ∈ C) ∧ v = ((x ‘w) ‘z))} ∧ (z ∈ B ∧ w ∈ C)) → ((zyw) ∈ A ↔ ((x ‘w) ‘z) ∈ A))
42	41	adantll 309	. . . . . . . . . 10 ⊢ (((x ∈ ((A ↑m B) ↑m C) ∧ y = {⟨⟨z, w⟩, v⟩∣((z ∈ B ∧ w ∈ C) ∧ v = ((x ‘w) ‘z))}) ∧ (z ∈ B ∧ w ∈ C)) → ((zyw) ∈ A ↔ ((x ‘w) ‘z) ∈ A))
43	36, 42	mpbird 171	. . . . . . . . 9 ⊢ (((x ∈ ((A ↑m B) ↑m C) ∧ y = {⟨⟨z, w⟩, v⟩∣((z ∈ B ∧ w ∈ C) ∧ v = ((x ‘w) ‘z))}) ∧ (z ∈ B ∧ w ∈ C)) → (zyw) ∈ A)
44	43	exp32 294	. . . . . . . 8 ⊢ ((x ∈ ((A ↑m B) ↑m C) ∧ y = {⟨⟨z, w⟩, v⟩∣((z ∈ B ∧ w ∈ C) ∧ v = ((x ‘w) ‘z))}) → (z ∈ B → (w ∈ C → (zyw) ∈ A)))
45	23, 24, 44	r19.21ad 1261	. . . . . . 7 ⊢ ((x ∈ ((A ↑m B) ↑m C) ∧ y = {⟨⟨z, w⟩, v⟩∣((z ∈ B ∧ w ∈ C) ∧ v = ((x ‘w) ‘z))}) → (z ∈ B → ∀w ∈ C (zyw) ∈ A))
46	19, 45	r19.21ai 1258	. . . . . 6 ⊢ ((x ∈ ((A ↑m B) ↑m C) ∧ y = {⟨⟨z, w⟩, v⟩∣((z ∈ B ∧ w ∈ C) ∧ v = ((x ‘w) ‘z))}) → ∀z ∈ B ∀w ∈ C (zyw) ∈ A)
47	15, 46	jca 236	. . . . 5 ⊢ ((x ∈ ((A ↑m B) ↑m C) ∧ y = {⟨⟨z, w⟩, v⟩∣((z ∈ B ∧ w ∈ C) ∧ v = ((x ‘w) ‘z))}) → (y Fn (B × C) ∧ ∀z ∈ B ∀w ∈ C (zyw) ∈ A))
48	2, 3	xpex 2488	. . . . . . 7 ⊢ (B × C) ∈ V
49	26, 48	elmap 3265	. . . . . 6 ⊢ (y ∈ (A ↑m (B × C)) ↔ y:(B × C)–→A)
50		ffnoprval 3041	. . . . . 6 ⊢ (y:(B × C)–→A ↔ (y Fn (B × C) ∧ ∀z ∈ B ∀w ∈ C (zyw) ∈ A))
51	49, 50	bitr 151	. . . . 5 ⊢ (y ∈ (A ↑m (B × C)) ↔ (y Fn (B × C) ∧ ∀z ∈ B ∀w ∈ C (zyw) ∈ A))
52	47, 51	sylibr 175	. . . 4 ⊢ ((x ∈ ((A ↑m B) ↑m C) ∧ y = {⟨⟨z, w⟩, v⟩∣((z ∈ B ∧ w ∈ C) ∧ v = ((x ‘w) ‘z))}) → y ∈ (A ↑m (B × C)))
53		fopabfv 2894	. . . . . . . 8 ⊢ (x:C–→(A ↑m B) ↔ (x = {⟨w, f⟩∣(w ∈ C ∧ f = (x ‘w))} ∧ ∀w ∈ C (x ‘w) ∈ (A ↑m B)))
54	53	pm3.26bd 259	. . . . . . 7 ⊢ (x:C–→(A ↑m B) → x = {⟨w, f⟩∣(w ∈ C ∧ f = (x ‘w))})
55	31, 54	sylbi 174	. . . . . 6 ⊢ (x ∈ ((A ↑m B) ↑m C) → x = {⟨w, f⟩∣(w ∈ C ∧ f = (x ‘w))})
56	55	adantr 306	. . . . 5 ⊢ ((x ∈ ((A ↑m B) ↑m C) ∧ y = {⟨⟨z, w⟩, v⟩∣((z ∈ B ∧ w ∈ C) ∧ v = ((x ‘w) ‘z))}) → x = {⟨w, f⟩∣(w ∈ C ∧ f = (x ‘w))})
57		ax-17 925	. . . . . 6 ⊢ ((x ∈ ((A ↑m B) ↑m C) ∧ y = {⟨⟨z, w⟩, v⟩∣((z ∈ B ∧ w ∈ C) ∧ v = ((x ‘w) ‘z))}) → ∀f(x ∈ ((A ↑m B) ↑m C) ∧ y = {⟨⟨z, w⟩, v⟩∣((z ∈ B ∧ w ∈ C) ∧ v = ((x ‘w) ‘z))}))
58	32	adantlr 310	. . . . . . . . . 10 ⊢ (((x ∈ ((A ↑m B) ↑m C) ∧ y = {⟨⟨z, w⟩, v⟩∣((z ∈ B ∧ w ∈ C) ∧ v = ((x ‘w) ‘z))}) ∧ w ∈ C) → (x ‘w) ∈ (A ↑m B))
59		ax-17 925	. . . . . . . . . . . . . . 15 ⊢ (w ∈ C → ∀z w ∈ C)
60	18, 59	hban 704	. . . . . . . . . . . . . 14 ⊢ ((y = {⟨⟨z, w⟩, v⟩∣((z ∈ B ∧ w ∈ C) ∧ v = ((x ‘w) ‘z))} ∧ w ∈ C) → ∀z(y = {⟨⟨z, w⟩, v⟩∣((z ∈ B ∧ w ∈ C) ∧ v = ((x ‘w) ‘z))} ∧ w ∈ C))
61		ax-17 925	. . . . . . . . . . . . . 14 ⊢ ((y = {⟨⟨z, w⟩, v⟩∣((z ∈ B ∧ w ∈ C) ∧ v = ((x ‘w) ‘z))} ∧ w ∈ C) → ∀g(y = {⟨⟨z, w⟩, v⟩∣((z ∈ B ∧ w ∈ C) ∧ v = ((x ‘w) ‘z))} ∧ w ∈ C))
62	40	anassrs 338	. . . . . . . . . . . . . . . . . 18 ⊢ (((y = {⟨⟨z, w⟩, v⟩∣((z ∈ B ∧ w ∈ C) ∧ v = ((x ‘w) ‘z))} ∧ z ∈ B) ∧ w ∈ C) → (zyw) = ((x ‘w) ‘z))
63	62	an1rs 373	. . . . . . . . . . . . . . . . 17 ⊢ (((y = {⟨⟨z, w⟩, v⟩∣((z ∈ B ∧ w ∈ C) ∧ v = ((x ‘w) ‘z))} ∧ w ∈ C) ∧ z ∈ B) → (zyw) = ((x ‘w) ‘z))
64	63	cleq2d 1112	. . . . . . . . . . . . . . . 16 ⊢ (((y = {⟨⟨z, w⟩, v⟩∣((z ∈ B ∧ w ∈ C) ∧ v = ((x ‘w) ‘z))} ∧ w ∈ C) ∧ z ∈ B) → (g = (zyw) ↔ g = ((x ‘w) ‘z)))
65	64	exp 291	. . . . . . . . . . . . . . 15 ⊢ ((y = {⟨⟨z, w⟩, v⟩∣((z ∈ B ∧ w ∈ C) ∧ v = ((x ‘w) ‘z))} ∧ w ∈ C) → (z ∈ B → (g = (zyw) ↔ g = ((x ‘w) ‘z))))
66	65	pm5.32d 491	. . . . . . . . . . . . . 14 ⊢ ((y = {⟨⟨z, w⟩, v⟩∣((z ∈ B ∧ w ∈ C) ∧ v = ((x ‘w) ‘z))} ∧ w ∈ C) → ((z ∈ B ∧ g = (zyw)) ↔ (z ∈ B ∧ g = ((x ‘w) ‘z))))
67	60, 61, 66	biopabd 2101	. . . . . . . . . . . . 13 ⊢ ((y = {⟨⟨z, w⟩, v⟩∣((z ∈ B ∧ w ∈ C) ∧ v = ((x ‘w) ‘z))} ∧ w ∈ C) → {⟨z, g⟩∣(z ∈ B ∧ g = (zyw))} = {⟨z, g⟩∣(z ∈ B ∧ g = ((x ‘w) ‘z))})
68	67	cleq2d 1112	. . . . . . . . . . . 12 ⊢ ((y = {⟨⟨z, w⟩, v⟩∣((z ∈ B ∧ w ∈ C) ∧ v = ((x ‘w) ‘z))} ∧ w ∈ C) → ((x ‘w) = {⟨z, g⟩∣(z ∈ B ∧ g = (zyw))} ↔ (x ‘w) = {⟨z, g⟩∣(z ∈ B ∧ g = ((x ‘w) ‘z))}))
69		fopabfv 2894	. . . . . . . . . . . . . 14 ⊢ ((x ‘w):B–→A ↔ ((x ‘w) = {⟨z, g⟩∣(z ∈ B ∧ g = ((x ‘w) ‘z))} ∧ ∀z ∈ B ((x ‘w) ‘z) ∈ A))
70	69	pm3.26bd 259	. . . . . . . . . . . . 13 ⊢ ((x ‘w):B–→A → (x ‘w) = {⟨z, g⟩∣(z ∈ B ∧ g = ((x ‘w) ‘z))})
71	27, 70	sylbi 174	. . . . . . . . . . . 12 ⊢ ((x ‘w) ∈ (A ↑m B) → (x ‘w) = {⟨z, g⟩∣(z ∈ B ∧ g = ((x ‘w) ‘z))})
72	68, 71	syl5bir 184	. . . . . . . . . . 11 ⊢ ((y = {⟨⟨z, w⟩, v⟩∣((z ∈ B ∧ w ∈ C) ∧ v = ((x ‘w) ‘z))} ∧ w ∈ C) → ((x ‘w) ∈ (A ↑m B) → (x ‘w) = {⟨z, g⟩∣(z ∈ B ∧ g = (zyw))}))
73	72	adantll 309	. . . . . . . . . 10 ⊢ (((x ∈ ((A ↑m B) ↑m C) ∧ y = {⟨⟨z, w⟩, v⟩∣((z ∈ B ∧ w ∈ C) ∧ v = ((x ‘w) ‘z))}) ∧ w ∈ C) → ((x ‘w) ∈ (A ↑m B) → (x ‘w) = {⟨z, g⟩∣(z ∈ B ∧ g = (zyw))}))
74	58, 73	mpd 46	. . . . . . . . 9 ⊢ (((x ∈ ((A ↑m B) ↑m C) ∧ y = {⟨⟨z, w⟩, v⟩∣((z ∈ B ∧ w ∈ C) ∧ v = ((x ‘w) ‘z))}) ∧ w ∈ C) → (x ‘w) = {⟨z, g⟩∣(z ∈ B ∧ g = (zyw))})
75	74	cleq2d 1112	. . . . . . . 8 ⊢ (((x ∈ ((A ↑m B) ↑m C) ∧ y = {⟨⟨z, w⟩, v⟩∣((z ∈ B ∧ w ∈ C) ∧ v = ((x ‘w) ‘z))}) ∧ w ∈ C) → (f = (x ‘w) ↔ f = {⟨z, g⟩∣(z ∈ B ∧ g = (zyw))}))
76	75	exp 291	. . . . . . 7 ⊢ ((x ∈ ((A ↑m B) ↑m C) ∧ y = {⟨⟨z, w⟩, v⟩∣((z ∈ B ∧ w ∈ C) ∧ v = ((x ‘w) ‘z))}) → (w ∈ C → (f = (x ‘w) ↔ f = {⟨z, g⟩∣(z ∈ B ∧ g = (zyw))})))
77	76	pm5.32d 491	. . . . . 6 ⊢ ((x ∈ ((A ↑m B) ↑m C) ∧ y = {⟨⟨z, w⟩, v⟩∣((z ∈ B ∧ w ∈ C) ∧ v = ((x ‘w) ‘z))}) → ((w ∈ C ∧ f = (x ‘w)) ↔ (w ∈ C ∧ f = {⟨z, g⟩∣(z ∈ B ∧ g = (zyw))})))
78	23, 57, 77	biopabd 2101	. . . . 5 ⊢ ((x ∈ ((A ↑m B) ↑m C) ∧ y = {⟨⟨z, w⟩, v⟩∣((z ∈ B ∧ w ∈ C) ∧ v = ((x ‘w) ‘z))}) → {⟨w, f⟩∣(w ∈ C ∧ f = (x ‘w))} = {⟨w, f⟩∣(w ∈ C ∧ f = {⟨z, g⟩∣(z ∈ B ∧ g = (zyw))})})
79	56, 78	eqtrd 1128	. . . 4 ⊢ ((x ∈ ((A ↑m B) ↑m C) ∧ y = {⟨⟨z, w⟩, v⟩∣((z ∈ B ∧ w ∈ C) ∧ v = ((x ‘w) ‘z))}) → x = {⟨w, f⟩∣(w ∈ C ∧ f = {⟨z, g⟩∣(z ∈ B ∧ g = (zyw))})})
80	52, 79	jca 236	. . 3 ⊢ ((x ∈ ((A ↑m B) ↑m C) ∧ y = {⟨⟨z, w⟩, v⟩∣((z ∈ B ∧ w ∈ C) ∧ v = ((x ‘w) ‘z))}) → (y ∈ (A ↑m (B × C)) ∧ x = {⟨w, f⟩∣(w ∈ C ∧ f = {⟨z, g⟩∣(z ∈ B ∧ g = (zyw))})}))
81		hbopab1 2112	. . . . . . . . . . . . . . 15 ⊢ (f ∈ {⟨z, g⟩∣(z ∈ B ∧ g = (zyw))} → ∀z f ∈ {⟨z, g⟩∣(z ∈ B ∧ g = (zyw))})
82	81	hbeleq 1173	. . . . . . . . . . . . . 14 ⊢ (f = {⟨z, g⟩∣(z ∈ B ∧ g = (zyw))} → ∀z f = {⟨z, g⟩∣(z ∈ B ∧ g = (zyw))})
83	59, 82	hban 704	. . . . . . . . . . . . 13 ⊢ ((w ∈ C ∧ f = {⟨z, g⟩∣(z ∈ B ∧ g = (zyw))}) → ∀z(w ∈ C ∧ f = {⟨z, g⟩∣(z ∈ B ∧ g = (zyw))}))
84	83	hbopab 2111	. . . . . . . . . . . 12 ⊢ (x ∈ {⟨w, f⟩∣(w ∈ C ∧ f = {⟨z, g⟩∣(z ∈ B ∧ g = (zyw))})} → ∀z x ∈ {⟨w, f⟩∣(w ∈ C ∧ f = {⟨z, g⟩∣(z ∈ B ∧ g = (zyw))})})
85	84	hbeleq 1173	. . . . . . . . . . 11 ⊢ (x = {⟨w, f⟩∣(w ∈ C ∧ f = {⟨z, g⟩∣(z ∈ B ∧ g = (zyw))})} → ∀z x = {⟨w, f⟩∣(w ∈ C ∧ f = {⟨z, g⟩∣(z ∈ B ∧ g = (zyw))})})
86		hbopab1 2112	. . . . . . . . . . . 12 ⊢ (x ∈ {⟨w, f⟩∣(w ∈ C ∧ f = {⟨z, g⟩∣(z ∈ B ∧ g = (zyw))})} → ∀w x ∈ {⟨w, f⟩∣(w ∈ C ∧ f = {⟨z, g⟩∣(z ∈ B ∧ g = (zyw))})})
87	86	hbeleq 1173	. . . . . . . . . . 11 ⊢ (x = {⟨w, f⟩∣(w ∈ C ∧ f = {⟨z, g⟩∣(z ∈ B ∧ g = (zyw))})} → ∀w x = {⟨w, f⟩∣(w ∈ C ∧ f = {⟨z, g⟩∣(z ∈ B ∧ g = (zyw))})})
88		ax-17 925	. . . . . . . . . . 11 ⊢ (x = {⟨w, f⟩∣(w ∈ C ∧ f = {⟨z, g⟩∣(z ∈ B ∧ g = (zyw))})} → ∀v x = {⟨w, f⟩∣(w ∈ C ∧ f = {⟨z, g⟩∣(z ∈ B ∧ g = (zyw))})})
89		fveq1 2831	. . . . . . . . . . . . . . . . . . 19 ⊢ (x = {⟨w, f⟩∣(w ∈ C ∧ f = {⟨z, g⟩∣(z ∈ B ∧ g = (zyw))})} → (x ‘w) = ({⟨w, f⟩∣(w ∈ C ∧ f = {⟨z, g⟩∣(z ∈ B ∧ g = (zyw))})} ‘w))
90		moeq 1431	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ∃*g g = (zyw)
91	90	a1i 7	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (z ∈ B → ∃*g g = (zyw))
92	2, 91	funopabex 2742	. . . . . . . . . . . . . . . . . . . 20 ⊢ {⟨z, g⟩∣(z ∈ B ∧ g = (zyw))} ∈ V
93		fvopab2 2878	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((w ∈ C ∧ {⟨z, g⟩∣(z ∈ B ∧ g = (zyw))} ∈ V) → ({⟨w, f⟩∣(w ∈ C ∧ f = {⟨z, g⟩∣(z ∈ B ∧ g = (zyw))})} ‘w) = {⟨z, g⟩∣(z ∈ B ∧ g = (zyw))})
94	92, 93	mpan2 519	. . . . . . . . . . . . . . . . . . 19 ⊢ (w ∈ C → ({⟨w, f⟩∣(w ∈ C ∧ f = {⟨z, g⟩∣(z ∈ B ∧ g = (zyw))})} ‘w) = {⟨z, g⟩∣(z ∈ B ∧ g = (zyw))})
95	89, 94	sylan9eq 1144	. . . . . . . . . . . . . . . . . 18 ⊢ ((x = {⟨w, f⟩∣(w ∈ C ∧ f = {⟨z, g⟩∣(z ∈ B ∧ g = (zyw))})} ∧ w ∈ C) → (x ‘w) = {⟨z, g⟩∣(z ∈ B ∧ g = (zyw))})
96	95	fveq1d 2834	. . . . . . . . . . . . . . . . 17 ⊢ ((x = {⟨w, f⟩∣(w ∈ C ∧ f = {⟨z, g⟩∣(z ∈ B ∧ g = (zyw))})} ∧ w ∈ C) → ((x ‘w) ‘z) = ({⟨z, g⟩∣(z ∈ B ∧ g = (zyw))} ‘z))
97		oprex 3018	. . . . . . . . . . . . . . . . . 18 ⊢ (zyw) ∈ V
98		fvopab2 2878	. . . . . . . . . . . . . . . . . 18 ⊢ ((z ∈ B ∧ (zyw) ∈ V) → ({⟨z, g⟩∣(z ∈ B ∧ g = (zyw))} ‘z) = (zyw))
99	97, 98	mpan2 519	. . . . . . . . . . . . . . . . 17 ⊢ (z ∈ B → ({⟨z, g⟩∣(z ∈ B ∧ g = (zyw))} ‘z) = (zyw))
100	96, 99	sylan9eq 1144	. . . . . . . . . . . . . . . 16 ⊢ (((x = {⟨w, f⟩∣(w ∈ C ∧ f = {⟨z, g⟩∣(z ∈ B ∧ g = (zyw))})} ∧ w ∈ C) ∧ z ∈ B) → ((x ‘w) ‘z) = (zyw))
101	100	an1rs 373	. . . . . . . . . . . . . . 15 ⊢ (((x = {⟨w, f⟩∣(w ∈ C ∧ f = {⟨z, g⟩∣(z ∈ B ∧ g = (zyw))})} ∧ z ∈ B) ∧ w ∈ C) → ((x ‘w) ‘z) = (zyw))
102	101	anasss 337	. . . . . . . . . . . . . 14 ⊢ ((x = {⟨w, f⟩∣(w ∈ C ∧ f = {⟨z, g⟩∣(z ∈ B ∧ g = (zyw))})} ∧ (z ∈ B ∧ w ∈ C)) → ((x ‘w) ‘z) = (zyw))
103	102	cleq2d 1112	. . . . . . . . . . . . 13 ⊢ ((x = {⟨w, f⟩∣(w ∈ C ∧ f = {⟨z, g⟩∣(z ∈ B ∧ g = (zyw))})} ∧ (z ∈ B ∧ w ∈ C)) → (v = ((x ‘w) ‘z) ↔ v = (zyw)))
104	103	exp 291	. . . . . . . . . . . 12 ⊢ (x = {⟨w, f⟩∣(w ∈ C ∧ f = {⟨z, g⟩∣(z ∈ B ∧ g = (zyw))})} → ((z ∈ B ∧ w ∈ C) → (v = ((x ‘w) ‘z) ↔ v = (zyw))))
105	104	pm5.32d 491	. . . . . . . . . . 11 ⊢ (x = {⟨w, f⟩∣(w ∈ C ∧ f = {⟨z, g⟩∣(z ∈ B ∧ g = (zyw))})} → (((z ∈ B ∧ w ∈ C) ∧ v = ((x ‘w) ‘z)) ↔ ((z ∈ B ∧ w ∈ C) ∧ v = (zyw))))
106	85, 87, 88, 105	bioprabd 3025	. . . . . . . . . 10 ⊢ (x = {⟨w, f⟩∣(w ∈ C ∧ f = {⟨z, g⟩∣(z ∈ B ∧ g = (zyw))})} → {⟨⟨z, w⟩, v⟩∣((z ∈ B ∧ w ∈ C) ∧ v = ((x ‘w) ‘z))} = {⟨⟨z, w⟩, v⟩∣((z ∈ B ∧ w ∈ C) ∧ v = (zyw))})
107	106	cleq2d 1112	. . . . . . . . 9 ⊢ (x = {⟨w, f⟩∣(w ∈ C ∧ f = {⟨z, g⟩∣(z ∈ B ∧ g = (zyw))})} → (y = {⟨⟨z, w⟩, v⟩∣((z ∈ B ∧ w ∈ C) ∧ v = ((x ‘w) ‘z))} ↔ y = {⟨⟨z, w⟩, v⟩∣((z ∈ B ∧ w ∈ C) ∧ v = (zyw))}))
108		fnoprval 3042	. . . . . . . . 9 ⊢ (y Fn (B × C) ↔ y = {⟨⟨z, w⟩, v⟩∣((z ∈ B ∧ w ∈ C) ∧ v = (zyw))})
109	107, 108	syl6bbr 416	. . . . . . . 8 ⊢ (x = {⟨w, f⟩∣(w ∈ C ∧ f = {⟨z, g⟩∣(z ∈ B ∧ g = (zyw))})} → (y = {⟨⟨z, w⟩, v⟩∣((z ∈ B ∧ w ∈ C) ∧ v = ((x ‘w) ‘z))} ↔ y Fn (B × C)))
110	109	anbi1d 469	. . . . . . 7 ⊢ (x = {⟨w, f⟩∣(w ∈ C ∧ f = {⟨z, g⟩∣(z ∈ B ∧ g = (zyw))})} → ((y = {⟨⟨z, w⟩, v⟩∣((z ∈ B ∧ w ∈ C) ∧ v = ((x ‘w) ‘z))} ∧ ∀z ∈ B ∀w ∈ C (zyw) ∈ A) ↔ (y Fn (B × C) ∧ ∀z ∈ B ∀w ∈ C (zyw) ∈ A)))
111	110, 51	syl6bbr 416	. . . . . 6 ⊢ (x = {⟨w, f⟩∣(w ∈ C ∧ f = {⟨z, g⟩∣(z ∈ B ∧ g = (zyw))})} → ((y = {⟨⟨z, w⟩, v⟩∣((z ∈ B ∧ w ∈ C) ∧ v = ((