Theorem xpmapenlem4 3394

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
xpmapenlem4	⊢ (((y = ⟨∪dom {y}, ∪ran {y}⟩ ∧ (∪dom {y}:C–→A ∧ ∪ran {y}:C–→B)) ∧ x = S) → (x:C–→(A × B) ∧ y = ⟨D, R⟩))

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 xpmapenlem4

Step	Hyp	Ref	Expression
1		xpmapenlem.6	. . . . . . 7 ⊢ S = {⟨z, w⟩∣(z ∈ C ∧ w = ⟨(∪dom {y} ‘z), (∪ran {y} ‘z)⟩)}
2		cleqtr 1118	. . . . . . . 8 ⊢ ((x = S ∧ S = {⟨z, w⟩∣(z ∈ C ∧ w = ⟨(∪dom {y} ‘z), (∪ran {y} ‘z)⟩)}) → x = {⟨z, w⟩∣(z ∈ C ∧ w = ⟨(∪dom {y} ‘z), (∪ran {y} ‘z)⟩)})
3		feq1 2748	. . . . . . . 8 ⊢ (x = {⟨z, w⟩∣(z ∈ C ∧ w = ⟨(∪dom {y} ‘z), (∪ran {y} ‘z)⟩)} → (x:C–→(A × B) ↔ {⟨z, w⟩∣(z ∈ C ∧ w = ⟨(∪dom {y} ‘z), (∪ran {y} ‘z)⟩)}:C–→(A × B)))
4	2, 3	syl 12	. . . . . . 7 ⊢ ((x = S ∧ S = {⟨z, w⟩∣(z ∈ C ∧ w = ⟨(∪dom {y} ‘z), (∪ran {y} ‘z)⟩)}) → (x:C–→(A × B) ↔ {⟨z, w⟩∣(z ∈ C ∧ w = ⟨(∪dom {y} ‘z), (∪ran {y} ‘z)⟩)}:C–→(A × B)))
5	1, 4	mpan2 519	. . . . . 6 ⊢ (x = S → (x:C–→(A × B) ↔ {⟨z, w⟩∣(z ∈ C ∧ w = ⟨(∪dom {y} ‘z), (∪ran {y} ‘z)⟩)}:C–→(A × B)))
6		fvex 2838	. . . . . . . . 9 ⊢ (∪ran {y} ‘z) ∈ V
7	6	opelxp 2452	. . . . . . . 8 ⊢ (⟨(∪dom {y} ‘z), (∪ran {y} ‘z)⟩ ∈ (A × B) ↔ ((∪dom {y} ‘z) ∈ A ∧ (∪ran {y} ‘z) ∈ B))
8	7	biral 1223	. . . . . . 7 ⊢ (∀z ∈ C ⟨(∪dom {y} ‘z), (∪ran {y} ‘z)⟩ ∈ (A × B) ↔ ∀z ∈ C ((∪dom {y} ‘z) ∈ A ∧ (∪ran {y} ‘z) ∈ B))
9		cleqid 1102	. . . . . . . 8 ⊢ {⟨z, w⟩∣(z ∈ C ∧ w = ⟨(∪dom {y} ‘z), (∪ran {y} ‘z)⟩)} = {⟨z, w⟩∣(z ∈ C ∧ w = ⟨(∪dom {y} ‘z), (∪ran {y} ‘z)⟩)}
10	9	fopab2 2891	. . . . . . 7 ⊢ (∀z ∈ C ⟨(∪dom {y} ‘z), (∪ran {y} ‘z)⟩ ∈ (A × B) ↔ {⟨z, w⟩∣(z ∈ C ∧ w = ⟨(∪dom {y} ‘z), (∪ran {y} ‘z)⟩)}:C–→(A × B))
11		r19.26 1289	. . . . . . 7 ⊢ (∀z ∈ C ((∪dom {y} ‘z) ∈ A ∧ (∪ran {y} ‘z) ∈ B) ↔ (∀z ∈ C (∪dom {y} ‘z) ∈ A ∧ ∀z ∈ C (∪ran {y} ‘z) ∈ B))
12	8, 10, 11	3bitr3r 157	. . . . . 6 ⊢ ((∀z ∈ C (∪dom {y} ‘z) ∈ A ∧ ∀z ∈ C (∪ran {y} ‘z) ∈ B) ↔ {⟨z, w⟩∣(z ∈ C ∧ w = ⟨(∪dom {y} ‘z), (∪ran {y} ‘z)⟩)}:C–→(A × B))
13	5, 12	syl6rbbr 417	. . . . 5 ⊢ (x = S → ((∀z ∈ C (∪dom {y} ‘z) ∈ A ∧ ∀z ∈ C (∪ran {y} ‘z) ∈ B) ↔ x:C–→(A × B)))
14	13	biimpac 326	. . . 4 ⊢ (((∀z ∈ C (∪dom {y} ‘z) ∈ A ∧ ∀z ∈ C (∪ran {y} ‘z) ∈ B) ∧ x = S) → x:C–→(A × B))
15		ffvrn 2890	. . . . . . 7 ⊢ ((∪dom {y}:C–→A ∧ z ∈ C) → (∪dom {y} ‘z) ∈ A)
16	15	exp 291	. . . . . 6 ⊢ (∪dom {y}:C–→A → (z ∈ C → (∪dom {y} ‘z) ∈ A))
17	16	r19.21aiv 1259	. . . . 5 ⊢ (∪dom {y}:C–→A → ∀z ∈ C (∪dom {y} ‘z) ∈ A)
18		ffvrn 2890	. . . . . . 7 ⊢ ((∪ran {y}:C–→B ∧ z ∈ C) → (∪ran {y} ‘z) ∈ B)
19	18	exp 291	. . . . . 6 ⊢ (∪ran {y}:C–→B → (z ∈ C → (∪ran {y} ‘z) ∈ B))
20	19	r19.21aiv 1259	. . . . 5 ⊢ (∪ran {y}:C–→B → ∀z ∈ C (∪ran {y} ‘z) ∈ B)
21	17, 20	anim12i 268	. . . 4 ⊢ ((∪dom {y}:C–→A ∧ ∪ran {y}:C–→B) → (∀z ∈ C (∪dom {y} ‘z) ∈ A ∧ ∀z ∈ C (∪ran {y} ‘z) ∈ B))
22	14, 21	sylan 343	. . 3 ⊢ (((∪dom {y}:C–→A ∧ ∪ran {y}:C–→B) ∧ x = S) → x:C–→(A × B))
23	22	adantll 309	. 2 ⊢ (((y = ⟨∪dom {y}, ∪ran {y}⟩ ∧ (∪dom {y}:C–→A ∧ ∪ran {y}:C–→B)) ∧ x = S) → x:C–→(A × B))
24		cleq1 1107	. . . . 5 ⊢ (y = ⟨∪dom {y}, ∪ran {y}⟩ → (y = ⟨D, R⟩ ↔ ⟨∪dom {y}, ∪ran {y}⟩ = ⟨D, R⟩))
25		fopabfv 2894	. . . . . . . . . 10 ⊢ (∪dom {y}:C–→A ↔ (∪dom {y} = {⟨z, w⟩∣(z ∈ C ∧ w = (∪dom {y} ‘z))} ∧ ∀z ∈ C (∪dom {y} ‘z) ∈ A))
26	25	pm3.26bd 259	. . . . . . . . 9 ⊢ (∪dom {y}:C–→A → ∪dom {y} = {⟨z, w⟩∣(z ∈ C ∧ w = (∪dom {y} ‘z))})
27		hbopab1 2112	. . . . . . . . . . . . 13 ⊢ (x ∈ {⟨z, w⟩∣(z ∈ C ∧ w = ⟨(∪dom {y} ‘z), (∪ran {y} ‘z)⟩)} → ∀z x ∈ {⟨z, w⟩∣(z ∈ C ∧ w = ⟨(∪dom {y} ‘z), (∪ran {y} ‘z)⟩)})
28	1	eleq2i 1153	. . . . . . . . . . . . 13 ⊢ (x ∈ S ↔ x ∈ {⟨z, w⟩∣(z ∈ C ∧ w = ⟨(∪dom {y} ‘z), (∪ran {y} ‘z)⟩)})
29	28	bial 695	. . . . . . . . . . . . 13 ⊢ (∀z x ∈ S ↔ ∀z x ∈ {⟨z, w⟩∣(z ∈ C ∧ w = ⟨(∪dom {y} ‘z), (∪ran {y} ‘z)⟩)})
30	27, 28, 29	3imtr4 192	. . . . . . . . . . . 12 ⊢ (x ∈ S → ∀z x ∈ S)
31	30	hbeleq 1173	. . . . . . . . . . 11 ⊢ (x = S → ∀z x = S)
32		hbopab2 2113	. . . . . . . . . . . . 13 ⊢ (x ∈ {⟨z, w⟩∣(z ∈ C ∧ w = ⟨(∪dom {y} ‘z), (∪ran {y} ‘z)⟩)} → ∀w x ∈ {⟨z, w⟩∣(z ∈ C ∧ w = ⟨(∪dom {y} ‘z), (∪ran {y} ‘z)⟩)})
33	28	bial 695	. . . . . . . . . . . . 13 ⊢ (∀w x ∈ S ↔ ∀w x ∈ {⟨z, w⟩∣(z ∈ C ∧ w = ⟨(∪dom {y} ‘z), (∪ran {y} ‘z)⟩)})
34	32, 28, 33	3imtr4 192	. . . . . . . . . . . 12 ⊢ (x ∈ S → ∀w x ∈ S)
35	34	hbeleq 1173	. . . . . . . . . . 11 ⊢ (x = S → ∀w x = S)
36	1, 2	mpan2 519	. . . . . . . . . . . . . . . . . . . 20 ⊢ (x = S → x = {⟨z, w⟩∣(z ∈ C ∧ w = ⟨(∪dom {y} ‘z), (∪ran {y} ‘z)⟩)})
37	36	fveq1d 2834	. . . . . . . . . . . . . . . . . . 19 ⊢ (x = S → (x ‘z) = ({⟨z, w⟩∣(z ∈ C ∧ w = ⟨(∪dom {y} ‘z), (∪ran {y} ‘z)⟩)} ‘z))
38		opex 1893	. . . . . . . . . . . . . . . . . . . 20 ⊢ ⟨(∪dom {y} ‘z), (∪ran {y} ‘z)⟩ ∈ V
39		fvopab2 2878	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((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)⟩)
40	38, 39	mpan2 519	. . . . . . . . . . . . . . . . . . 19 ⊢ (z ∈ C → ({⟨z, w⟩∣(z ∈ C ∧ w = ⟨(∪dom {y} ‘z), (∪ran {y} ‘z)⟩)} ‘z) = ⟨(∪dom {y} ‘z), (∪ran {y} ‘z)⟩)
41	37, 40	sylan9eq 1144	. . . . . . . . . . . . . . . . . 18 ⊢ ((x = S ∧ z ∈ C) → (x ‘z) = ⟨(∪dom {y} ‘z), (∪ran {y} ‘z)⟩)
42	41	sneqd 1818	. . . . . . . . . . . . . . . . 17 ⊢ ((x = S ∧ z ∈ C) → {(x ‘z)} = {⟨(∪dom {y} ‘z), (∪ran {y} ‘z)⟩})
43	42	dmeqd 2533	. . . . . . . . . . . . . . . 16 ⊢ ((x = S ∧ z ∈ C) → dom {(x ‘z)} = dom {⟨(∪dom {y} ‘z), (∪ran {y} ‘z)⟩})
44	43	unieqd 1929	. . . . . . . . . . . . . . 15 ⊢ ((x = S ∧ z ∈ C) → ∪dom {(x ‘z)} = ∪dom {⟨(∪dom {y} ‘z), (∪ran {y} ‘z)⟩})
45		fvex 2838	. . . . . . . . . . . . . . . 16 ⊢ (∪dom {y} ‘z) ∈ V
46	45	op1sta 2635	. . . . . . . . . . . . . . 15 ⊢ ∪dom {⟨(∪dom {y} ‘z), (∪ran {y} ‘z)⟩} = (∪dom {y} ‘z)
47	44, 46	syl6eq 1140	. . . . . . . . . . . . . 14 ⊢ ((x = S ∧ z ∈ C) → ∪dom {(x ‘z)} = (∪dom {y} ‘z))
48	47	cleq2d 1112	. . . . . . . . . . . . 13 ⊢ ((x = S ∧ z ∈ C) → (w = ∪dom {(x ‘z)} ↔ w = (∪dom {y} ‘z)))
49	48	exp 291	. . . . . . . . . . . 12 ⊢ (x = S → (z ∈ C → (w = ∪dom {(x ‘z)} ↔ w = (∪dom {y} ‘z))))
50	49	pm5.32d 491	. . . . . . . . . . 11 ⊢ (x = S → ((z ∈ C ∧ w = ∪dom {(x ‘z)}) ↔ (z ∈ C ∧ w = (∪dom {y} ‘z))))
51	31, 35, 50	biopabd 2101	. . . . . . . . . 10 ⊢ (x = S → {⟨z, w⟩∣(z ∈ C ∧ w = ∪dom {(x ‘z)})} = {⟨z, w⟩∣(z ∈ C ∧ w = (∪dom {y} ‘z))})
52		xpmapenlem.4	. . . . . . . . . 10 ⊢ D = {⟨z, w⟩∣(z ∈ C ∧ w = ∪dom {(x ‘z)})}
53	51, 52	syl5req 1137	. . . . . . . . 9 ⊢ (x = S → {⟨z, w⟩∣(z ∈ C ∧ w = (∪dom {y} ‘z))} = D)
54	26, 53	sylan9eq 1144	. . . . . . . 8 ⊢ ((∪dom {y}:C–→A ∧ x = S) → ∪dom {y} = D)
55	54	adantlr 310	. . . . . . 7 ⊢ (((∪dom {y}:C–→A ∧ ∪ran {y}:C–→B) ∧ x = S) → ∪dom {y} = D)
56		fopabfv 2894	. . . . . . . . . 10 ⊢ (∪ran {y}:C–→B ↔ (∪ran {y} = {⟨z, w⟩∣(z ∈ C ∧ w = (∪ran {y} ‘z))} ∧ ∀z ∈ C (∪ran {y} ‘z) ∈ B))
57	56	pm3.26bd 259	. . . . . . . . 9 ⊢ (∪ran {y}:C–→B → ∪ran {y} = {⟨z, w⟩∣(z ∈ C ∧ w = (∪ran {y} ‘z))})
58	42	rneqd 2557	. . . . . . . . . . . . . . . 16 ⊢ ((x = S ∧ z ∈ C) → ran {(x ‘z)} = ran {⟨(∪dom {y} ‘z), (∪ran {y} ‘z)⟩})
59	58	unieqd 1929	. . . . . . . . . . . . . . 15 ⊢ ((x = S ∧ z ∈ C) → ∪ran {(x ‘z)} = ∪ran {⟨(∪dom {y} ‘z), (∪ran {y} ‘z)⟩})
60	45, 6	op2nda 2639	. . . . . . . . . . . . . . 15 ⊢ ∪ran {⟨(∪dom {y} ‘z), (∪ran {y} ‘z)⟩} = (∪ran {y} ‘z)
61	59, 60	syl6eq 1140	. . . . . . . . . . . . . 14 ⊢ ((x = S ∧ z ∈ C) → ∪ran {(x ‘z)} = (∪ran {y} ‘z))
62	61	cleq2d 1112	. . . . . . . . . . . . 13 ⊢ ((x = S ∧ z ∈ C) → (w = ∪ran {(x ‘z)} ↔ w = (∪ran {y} ‘z)))
63	62	exp 291	. . . . . . . . . . . 12 ⊢ (x = S → (z ∈ C → (w = ∪ran {(x ‘z)} ↔ w = (∪ran {y} ‘z))))
64	63	pm5.32d 491	. . . . . . . . . . 11 ⊢ (x = S → ((z ∈ C ∧ w = ∪ran {(x ‘z)}) ↔ (z ∈ C ∧ w = (∪ran {y} ‘z))))
65	31, 35, 64	biopabd 2101	. . . . . . . . . 10 ⊢ (x = S → {⟨z, w⟩∣(z ∈ C ∧ w = ∪ran {(x ‘z)})} = {⟨z, w⟩∣(z ∈ C ∧ w = (∪ran {y} ‘z))})
66		xpmapenlem.5	. . . . . . . . . 10 ⊢ R = {⟨z, w⟩∣(z ∈ C ∧ w = ∪ran {(x ‘z)})}
67	65, 66	syl5req 1137	. . . . . . . . 9 ⊢ (x = S → {⟨z, w⟩∣(z ∈ C ∧ w = (∪ran {y} ‘z))} = R)
68	57, 67	sylan9eq 1144	. . . . . . . 8 ⊢ ((∪ran {y}:C–→B ∧ x = S) → ∪ran {y} = R)
69	68	adantll 309	. . . . . . 7 ⊢ (((∪dom {y}:C–→A ∧ ∪ran {y}:C–→B) ∧ x = S) → ∪ran {y} = R)
70	55, 69	jca 236	. . . . . 6 ⊢ (((∪dom {y}:C–→A ∧ ∪ran {y}:C–→B) ∧ x = S) → (∪dom {y} = D ∧ ∪ran {y} = R))
71		snex 1859	. . . . . . . . 9 ⊢ {y} ∈ V
72		dmexg 2551	. . . . . . . . 9 ⊢ ({y} ∈ V → dom {y} ∈ V)
73	71, 72	ax-mp 6	. . . . . . . 8 ⊢ dom {y} ∈ V
74	73	uniex 1947	. . . . . . 7 ⊢ ∪dom {y} ∈ V
75		rnexg 2569	. . . . . . . . 9 ⊢ ({y} ∈ V → ran {y} ∈ V)
76	71, 75	ax-mp 6	. . . . . . . 8 ⊢ ran {y} ∈ V
77	76	uniex 1947	. . . . . . 7 ⊢ ∪ran {y} ∈ V
78		xpmapen.3	. . . . . . . . 9 ⊢ C ∈ V
79		moeq 1431	. . . . . . . . . 10 ⊢ ∃*w w = ∪ran {(x ‘z)}
80	79	a1i 7	. . . . . . . . 9 ⊢ (z ∈ C → ∃*w w = ∪ran {(x ‘z)})
81	78, 80	funopabex 2742	. . . . . . . 8 ⊢ {⟨z, w⟩∣(z ∈ C ∧ w = ∪ran {(x ‘z)})} ∈ V
82	66, 81	eqeltr 1159	. . . . . . 7 ⊢ R ∈ V
83	74, 77, 82	opth 1898	. . . . . 6 ⊢ (⟨∪dom {y}, ∪ran {y}⟩ = ⟨D, R⟩ ↔ (∪dom {y} = D ∧ ∪ran {y} = R))
84	70, 83	sylibr 175	. . . . 5 ⊢ (((∪dom {y}:C–→A ∧ ∪ran {y}:C–→B) ∧ x = S) → ⟨∪dom {y}, ∪ran {y}⟩ = ⟨D, R⟩)
85	24, 84	syl5bir 184	. . . 4 ⊢ (y = ⟨∪dom {y}, ∪ran {y}⟩ → (((∪dom {y}:C–→A ∧ ∪ran {y}:C–→B) ∧ x = S) → y = ⟨D, R⟩))
86	85	exp3a 292	. . 3 ⊢ (y = ⟨∪dom {y}, ∪ran {y}⟩ → ((∪dom {y}:C–→A ∧ ∪ran {y}:C–→B) → (x = S → y = ⟨D, R⟩)))
87	86	imp31 280	. 2 ⊢ (((y = ⟨∪dom {y}, ∪ran {y}⟩ ∧ (∪dom {y}:C–→A ∧ ∪ran {y}:C–→B)) ∧ x = S) → y = ⟨D, R⟩)
88	23, 87	jca 236	1 ⊢ (((y = ⟨∪dom {y}, ∪ran {y}⟩ ∧ (∪dom {y}:C–→A ∧ ∪ran {y}:C–→B)) ∧ x = S) → (x:C–→(A × B) ∧ y = ⟨D, R⟩))

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  {copab 2055   × cxp 2408  dom cdm 2410  ran crn 2411  –→wf 2418   ‘cfv 2422

This theorem is referenced by:  xpmapenlem5 3395

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-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-fv 2438

metamath.org