Theorem xpmapenlem5 4506

Description: Lemma for xpmapen 4507.

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 groups:   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 3989	. 2 ⊢ ((A × B) ↑m C) ∈ V
2		opex 2788	. . 3 ⊢ ⟨D, R⟩ ∈ V
3	2	a1i 8	. 2 ⊢ (x ∈ ((A × B) ↑m C) → ⟨D, R⟩ ∈ V)
4		xpmapen.3	. . . 4 ⊢ C ∈ V
5		xpmapenlem.6	. . . 4 ⊢ S = {⟨z, w⟩∣(z ∈ C ⋀ w = ⟨(∪dom { y} ‘z), (∪ran { y} ‘z)⟩)}
6	4, 5	fopabex2 3618	. . 3 ⊢ S ∈ V
7	6	a1i 8	. 2 ⊢ (y ∈ ((A ↑m C) × (B ↑m C)) → S ∈ V)
8		xpmapenlem.5	. . . . . . . . . . . 12 ⊢ R = {⟨z, w⟩∣(z ∈ C ⋀ w = ∪ran {(x ‘z)})}
9	4, 8	fopabex2 3618	. . . . . . . . . . 11 ⊢ R ∈ V
10	9	opelxp 3220	. . . . . . . . . 10 ⊢ (⟨D, R⟩ ∈ (V × V) ↔ (D ∈ V ⋀ R ∈ V))
11		xpmapenlem.4	. . . . . . . . . . 11 ⊢ D = {⟨z, w⟩∣(z ∈ C ⋀ w = ∪dom {(x ‘z)})}
12	4, 11	fopabex2 3618	. . . . . . . . . 10 ⊢ D ∈ V
13	10, 12, 9	mpbir2an 732	. . . . . . . . 9 ⊢ ⟨D, R⟩ ∈ (V × V)
14		eleq1 1537	. . . . . . . . 9 ⊢ (y = ⟨D, R⟩ → (y ∈ (V × V) ↔ ⟨D, R⟩ ∈ (V × V)))
15	13, 14	mpbiri 194	. . . . . . . 8 ⊢ (y = ⟨D, R⟩ → y ∈ (V × V))
16	15	adantl 390	. . . . . . 7 ⊢ ((x:C–→(A × B) ⋀ y = ⟨D, R⟩) → y ∈ (V × V))
17		elxp4 3459	. . . . . . . 8 ⊢ (y ∈ (V × V) ↔ (y = ⟨∪dom { y}, ∪ran { y}⟩ ⋀ (∪dom { y} ∈ V ⋀ ∪ran { y} ∈ V)))
18	17	pm3.26bi 322	. . . . . . 7 ⊢ (y ∈ (V × V) → y = ⟨∪dom { y}, ∪ran { y}⟩)
19	16, 18	syl 10	. . . . . 6 ⊢ ((x:C–→(A × B) ⋀ y = ⟨D, R⟩) → y = ⟨∪dom { y}, ∪ran { y}⟩)
20	12	op1sta 3454	. . . . . . . . . . 11 ⊢ ∪dom {⟨D, R⟩} = D
21		sneq 2421	. . . . . . . . . . . . 13 ⊢ (y = ⟨D, R⟩ → {y} = {⟨D, R⟩})
22	21	dmeqd 3319	. . . . . . . . . . . 12 ⊢ (y = ⟨D, R⟩ → dom { y} = dom {⟨D, R⟩})
23	22	unieqd 2516	. . . . . . . . . . 11 ⊢ (y = ⟨D, R⟩ → ∪dom { y} = ∪dom {⟨D, R⟩})
24		xpmapen.1	. . . . . . . . . . . . . . 15 ⊢ A ∈ V
25		xpmapen.2	. . . . . . . . . . . . . . 15 ⊢ B ∈ V
26	24, 25, 4, 11, 8, 5	xpmapenlem1 4502	. . . . . . . . . . . . . 14 ⊢ ((y = ⟨D, R⟩ → ∀z y = ⟨D, R⟩) ⋀ (y = ⟨D, R⟩ → ∀w y = ⟨D, R⟩))
27	26	pm3.26i 320	. . . . . . . . . . . . 13 ⊢ (y = ⟨D, R⟩ → ∀z y = ⟨D, R⟩)
28	26	pm3.27i 324	. . . . . . . . . . . . 13 ⊢ (y = ⟨D, R⟩ → ∀w y = ⟨D, R⟩)
29	24, 25, 4, 11, 8, 5	xpmapenlem2 4503	. . . . . . . . . . . . . . . 16 ⊢ ((y = ⟨D, R⟩ ⋀ z ∈ C) → ((∪dom { y} ‘z) = ∪dom {(x ‘z)} ⋀ (∪ran { y} ‘z) = ∪ran {(x ‘z)}))
30	29	pm3.26d 321	. . . . . . . . . . . . . . 15 ⊢ ((y = ⟨D, R⟩ ⋀ z ∈ C) → (∪dom { y} ‘z) = ∪dom {(x ‘z)})
31	30	eqeq2d 1489	. . . . . . . . . . . . . 14 ⊢ ((y = ⟨D, R⟩ ⋀ z ∈ C) → (w = (∪dom { y} ‘z) ↔ w = ∪dom {(x ‘z)}))
32	31	pm5.32da 651	. . . . . . . . . . . . 13 ⊢ (y = ⟨D, R⟩ → ((z ∈ C ⋀ w = (∪dom { y} ‘z)) ↔ (z ∈ C ⋀ w = ∪dom {(x ‘z)})))
33	27, 28, 32	opabbid 2674	. . . . . . . . . . . 12 ⊢ (y = ⟨D, R⟩ → {⟨z, w⟩∣(z ∈ C ⋀ w = (∪dom { y} ‘z))} = {⟨z, w⟩∣(z ∈ C ⋀ w = ∪dom {(x ‘z)})})
34	33, 11	syl6eqr 1528	. . . . . . . . . . 11 ⊢ (y = ⟨D, R⟩ → {⟨z, w⟩∣(z ∈ C ⋀ w = (∪dom { y} ‘z))} = D)
35	20, 23, 34	3eqtr4a 1535	. . . . . . . . . 10 ⊢ (y = ⟨D, R⟩ → ∪dom { y} = {⟨z, w⟩∣(z ∈ C ⋀ w = (∪dom { y} ‘z))})
36	12, 9	op2nda 3458	. . . . . . . . . . 11 ⊢ ∪ran {⟨D, R⟩} = R
37	21	rneqd 3347	. . . . . . . . . . . 12 ⊢ (y = ⟨D, R⟩ → ran { y} = ran {⟨D, R⟩})
38	37	unieqd 2516	. . . . . . . . . . 11 ⊢ (y = ⟨D, R⟩ → ∪ran { y} = ∪ran {⟨D, R⟩})
39	29	pm3.27d 325	. . . . . . . . . . . . . . 15 ⊢ ((y = ⟨D, R⟩ ⋀ z ∈ C) → (∪ran { y} ‘z) = ∪ran {(x ‘z)})
40	39	eqeq2d 1489	. . . . . . . . . . . . . 14 ⊢ ((y = ⟨D, R⟩ ⋀ z ∈ C) → (w = (∪ran { y} ‘z) ↔ w = ∪ran {(x ‘z)}))
41	40	pm5.32da 651	. . . . . . . . . . . . 13 ⊢ (y = ⟨D, R⟩ → ((z ∈ C ⋀ w = (∪ran { y} ‘z)) ↔ (z ∈ C ⋀ w = ∪ran {(x ‘z)})))
42	27, 28, 41	opabbid 2674	. . . . . . . . . . . 12 ⊢ (y = ⟨D, R⟩ → {⟨z, w⟩∣(z ∈ C ⋀ w = (∪ran { y} ‘z))} = {⟨z, w⟩∣(z ∈ C ⋀ w = ∪ran {(x ‘z)})})
43	42, 8	syl6eqr 1528	. . . . . . . . . . 11 ⊢ (y = ⟨D, R⟩ → {⟨z, w⟩∣(z ∈ C ⋀ w = (∪ran { y} ‘z))} = R)
44	36, 38, 43	3eqtr4a 1535	. . . . . . . . . 10 ⊢ (y = ⟨D, R⟩ → ∪ran { y} = {⟨z, w⟩∣(z ∈ C ⋀ w = (∪ran { y} ‘z))})
45	35, 44	jca 288	. . . . . . . . 9 ⊢ (y = ⟨D, R⟩ → (∪dom { y} = {⟨z, w⟩∣(z ∈ C ⋀ w = (∪dom { y} ‘z))} ⋀ ∪ran { y} = {⟨z, w⟩∣(z ∈ C ⋀ w = (∪ran { y} ‘z))}))
46	45	adantl 390	. . . . . . . 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))}))
47		ffvelrn 3820	. . . . . . . . . . 11 ⊢ ((x:C–→(A × B) ⋀ z ∈ C) → (x ‘z) ∈ (A × B))
48	47	r19.21aiva 1717	. . . . . . . . . 10 ⊢ (x:C–→(A × B) → ∀z ∈ C (x ‘z) ∈ (A × B))
49	48	adantr 391	. . . . . . . . 9 ⊢ ((x:C–→(A × B) ⋀ y = ⟨D, R⟩) → ∀z ∈ C (x ‘z) ∈ (A × B))
50		ax-17 973	. . . . . . . . . . . 12 ⊢ (x:C–→(A × B) → ∀z x:C–→(A × B))
51	50, 27	hban 1011	. . . . . . . . . . 11 ⊢ ((x:C–→(A × B) ⋀ y = ⟨D, R⟩) → ∀z(x:C–→(A × B) ⋀ y = ⟨D, R⟩))
52	24, 25, 4, 11, 8, 5	xpmapenlem3 4504	. . . . . . . . . . . . . . 15 ⊢ ((x:C–→(A × B) ⋀ y = ⟨D, R⟩) → x = S)
53	52	fveq1d 3732	. . . . . . . . . . . . . 14 ⊢ ((x:C–→(A × B) ⋀ y = ⟨D, R⟩) → (x ‘z) = (S ‘z))
54		opex 2788	. . . . . . . . . . . . . . . 16 ⊢ ⟨(∪dom { y} ‘z), (∪ran { y} ‘z)⟩ ∈ V
55		fvopab2 3797	. . . . . . . . . . . . . . . 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)⟩)
56	54, 55	mpan2 698	. . . . . . . . . . . . . . 15 ⊢ (z ∈ C → ({⟨z, w⟩∣(z ∈ C ⋀ w = ⟨(∪dom { y} ‘z), (∪ran { y} ‘z)⟩)} ‘z) = ⟨(∪dom { y} ‘z), (∪ran { y} ‘z)⟩)
57	5	fveq1i 3731	. . . . . . . . . . . . . . 15 ⊢ (S ‘z) = ({⟨z, w⟩∣(z ∈ C ⋀ w = ⟨(∪dom { y} ‘z), (∪ran { y} ‘z)⟩)} ‘z)
58	56, 57	syl5eq 1522	. . . . . . . . . . . . . 14 ⊢ (z ∈ C → (S ‘z) = ⟨(∪dom { y} ‘z), (∪ran { y} ‘z)⟩)
59	53, 58	sylan9eq 1530	. . . . . . . . . . . . 13 ⊢ (((x:C–→(A × B) ⋀ y = ⟨D, R⟩) ⋀ z ∈ C) → (x ‘z) = ⟨(∪dom { y} ‘z), (∪ran { y} ‘z)⟩)
60	59	eleq1d 1543	. . . . . . . . . . . 12 ⊢ (((x:C–→(A × B) ⋀ y = ⟨D, R⟩) ⋀ z ∈ C) → ((x ‘z) ∈ (A × B) ↔ ⟨(∪dom { y} ‘z), (∪ran { y} ‘z)⟩ ∈ (A × B)))
61		fvex 3738	. . . . . . . . . . . . 13 ⊢ (∪ran { y} ‘z) ∈ V
62	61	opelxp 3220	. . . . . . . . . . . 12 ⊢ (⟨(∪dom { y} ‘z), (∪ran { y} ‘z)⟩ ∈ (A × B) ↔ ((∪dom { y} ‘z) ∈ A ⋀ (∪ran { y} ‘z) ∈ B))
63	60, 62	syl6bb 538	. . . . . . . . . . 11 ⊢ (((x:C–→(A × B) ⋀ y = ⟨D, R⟩) ⋀ z ∈ C) → ((x ‘z) ∈ (A × B) ↔ ((∪dom { y} ‘z) ∈ A ⋀ (∪ran { y} ‘z) ∈ B)))
64	51, 63	ralbida 1660	. . . . . . . . . 10 ⊢ ((x:C–→(A × B) ⋀ y = ⟨D, R⟩) → (∀z ∈ C (x ‘z) ∈ (A × B) ↔ ∀z ∈ C ((∪dom { y} ‘z) ∈ A ⋀ (∪ran { y} ‘z) ∈ B)))
65		r19.26 1753	. . . . . . . . . 10 ⊢ (∀z ∈ C ((∪dom { y} ‘z) ∈ A ⋀ (∪ran { y} ‘z) ∈ B) ↔ (∀z ∈ C (∪dom { y} ‘z) ∈ A ⋀ ∀z ∈ C (∪ran { y} ‘z) ∈ B))
66	64, 65	syl6bb 538	. . . . . . . . 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)))
67	49, 66	mpbid 195	. . . . . . . 8 ⊢ ((x:C–→(A × B) ⋀ y = ⟨D, R⟩) → (∀z ∈ C (∪dom { y} ‘z) ∈ A ⋀ ∀z ∈ C (∪ran { y} ‘z) ∈ B))
68	46, 67	jca 288	. . . . . . 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)))
69		an4 508	. . . . . . . 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)))
70		fopabfv 3837	. . . . . . . . 9 ⊢ (∪dom { y}:C–→A ↔ (∪dom { y} = {⟨z, w⟩∣(z ∈ C ⋀ w = (∪dom { y} ‘z))} ⋀ ∀z ∈ C (∪dom { y} ‘z) ∈ A))
71		fopabfv 3837	. . . . . . . . 9 ⊢ (∪ran { y}:C–→B ↔ (∪ran { y} = {⟨z, w⟩∣(z ∈ C ⋀ w = (∪ran { y} ‘z))} ⋀ ∀z ∈ C (∪ran { y} ‘z) ∈ B))
72	70, 71	anbi12i 484	. . . . . . . 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)))
73	69, 72	bitr4 176	. . . . . . 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))
74	68, 73	sylib 198	. . . . . 6 ⊢ ((x:C–→(A × B) ⋀ y = ⟨D, R⟩) → (∪dom { y}:C–→A ⋀ ∪ran { y}:C–→B))
75	19, 74	jca 288	. . . . 5 ⊢ ((x:C–→(A × B) ⋀ y = ⟨D, R⟩) → (y = ⟨∪dom { y}, ∪ran { y}⟩ ⋀ (∪dom { y}:C–→A ⋀ ∪ran { y}:C–→B)))
76	75, 52	jca 288	. . . 4 ⊢ ((x:C–→(A × B) ⋀ y = ⟨D, R⟩) → ((y = ⟨∪dom { y}, ∪ran { y}⟩ ⋀ (∪dom { y}:C–→A ⋀ ∪ran { y}:C–→B)) ⋀ x = S))
77	24, 25, 4, 11, 8, 5	xpmapenlem4 4505	. . . 4 ⊢ (((y = ⟨∪dom { y}, ∪ran { y}⟩ ⋀ (∪dom { y}:C–→A ⋀ ∪ran { y}:C–→B)) ⋀ x = S) → (x:C–→(A × B) ⋀ y = ⟨D, R⟩))
78	76, 77	impbi 157	. . 3 ⊢ ((x:C–→(A × B) ⋀ y = ⟨D, R⟩) ↔ ((y = ⟨∪dom { y}, ∪ran { y}⟩ ⋀ (∪dom { y}:C–→A ⋀ ∪ran { y}:C–→B)) ⋀ x = S))
79	24, 25	xpex 3266	. . . . 5 ⊢ (A × B) ∈ V
80	79, 4	elmap 4340	. . . 4 ⊢ (x ∈ ((A × B) ↑m C) ↔ x:C–→(A × B))
81	80	anbi1i 483	. . 3 ⊢ ((x ∈ ((A × B) ↑m C) ⋀ y = ⟨D, R⟩) ↔ (x:C–→(A × B) ⋀ y = ⟨D, R⟩))
82		elxp4 3459	. . . . 5 ⊢ (y ∈ ((A ↑m C) × (B ↑m C)) ↔ (y = ⟨∪dom { y}, ∪ran { y}⟩ ⋀ (∪dom { y} ∈ (A ↑m C) ⋀ ∪ran { y} ∈ (B ↑m C))))
83	24, 4	elmap 4340	. . . . . . 7 ⊢ (∪dom { y} ∈ (A ↑m C) ↔ ∪dom { y}:C–→A)
84	25, 4	elmap 4340	. . . . . . 7 ⊢ (∪ran { y} ∈ (B ↑m C) ↔ ∪ran { y}:C–→B)
85	83, 84	anbi12i 484	. . . . . 6 ⊢ ((∪dom { y} ∈ (A ↑m C) ⋀ ∪ran { y} ∈ (B ↑m C)) ↔ (∪dom { y}:C–→A ⋀ ∪ran { y}:C–→B))
86	85	anbi2i 482	. . . . 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)))
87	82, 86	bitr 173	. . . 4 ⊢ (y ∈ ((A ↑m C) × (B ↑m C)) ↔ (y = ⟨∪dom { y}, ∪ran { y}⟩ ⋀ (∪dom { y}:C–→A ⋀ ∪ran { y}:C–→B)))
88	87	anbi1i 483	. . 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))
89	78, 81, 88	3bitr4 183	. 2 ⊢ ((x ∈ ((A × B) ↑m C) ⋀ y = ⟨D, R⟩) ↔ (y ∈ ((A ↑m C) × (B ↑m C)) ⋀ x = S))
90	1, 3, 7, 89	en2 4408	1 ⊢ ((A × B) ↑m C) ≈ ((A ↑m C) × (B ↑m C))

Syntax hints:   → wi 3   ⋀ wa 223  ∀wal 956   = wceq 958   ∈ wcel 960  ∀wral 1648  Vcvv 1814  {csn 2413  ⟨cop 2415  ∪cuni 2507   class class class wbr 2624  {copab 2671   × cxp 3174  dom cdm 3176  ran crn 3177  –→wf 3184   ‘cfv 3188  (class class class)co 3969   ↑_m cm 4328   ≈ cen 4370

This theorem is referenced by:  xpmapen 4507

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-9 967  ax-10 968  ax-11 969  ax-12 970  ax-13 971  ax-14 972  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462  ax-rep 2698  ax-sep 2708  ax-nul 2715  ax-pow 2748  ax-pr 2785  ax-un 2872

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3an 779  df-ex 983  df-sb 1174  df-eu 1384  df-mo 1385  df-clab 1467  df-cleq 1472  df-clel 1475  df-ne 1590  df-ral 1652  df-rex 1653  df-v 1815  df-sbc 1945  df-csb 2005  df-dif 2052  df-un 2053  df-in 2054  df-ss 2056  df-nul 2284  df-pw 2406  df-sn 2416  df-pr 2417  df-op 2420  df-uni 2508  df-br 2625  df-opab 2672  df-id 2841  df-xp 3190  df-rel 3191  df-cnv 3192  df-co 3193  df-dm 3194  df-rn 3195  df-res 3196  df-ima 3197  df-fun 3198  df-fn 3199  df-f 3200  df-f1 3201  df-fo 3202  df-f1o 3203  df-fv 3204  df-opr 3971  df-oprab 3972  df-map 4330  df-en 4374

Copyright terms: Public domain