Theorem fmpt2x 5745

Description: Functionality, domain and codomain of a class given by the "maps to" notation, where B(x) is not constant but depends on x. (Contributed by NM, 29-Dec-2014.)

Hypothesis

Ref	Expression
fmpt2x.1	⊢ 𝐹 = (x ∈ A, y ∈ B ↦ 𝐶)

Assertion

Ref	Expression
fmpt2x	⊢ (∀x ∈ A ∀y ∈ B 𝐶 ∈ 𝐷 ↔ 𝐹:∪ x ∈ A ({x} × B)⟶𝐷)

Distinct variable groups:   x,y,A   y,B   x,𝐷,y

Allowed substitution hints:   B(x)   𝐶(x,y)   𝐹(x,y)

Proof of Theorem fmpt2x

Dummy variables v w z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 2534	. . . . . . . 8 ⊢ z ∈ V
2		vex 2534	. . . . . . . 8 ⊢ w ∈ V
3	1, 2	op1std 5694	. . . . . . 7 ⊢ (v = ⟨z, w⟩ → (1st ‘v) = z)
4	3	csbeq1d 2831	. . . . . 6 ⊢ (v = ⟨z, w⟩ → ⦋(1st ‘v) / x⦌⦋(2nd ‘v) / y⦌𝐶 = ⦋z / x⦌⦋(2nd ‘v) / y⦌𝐶)
5	1, 2	op2ndd 5695	. . . . . . . 8 ⊢ (v = ⟨z, w⟩ → (2nd ‘v) = w)
6	5	csbeq1d 2831	. . . . . . 7 ⊢ (v = ⟨z, w⟩ → ⦋(2nd ‘v) / y⦌𝐶 = ⦋w / y⦌𝐶)
7	6	csbeq2dv 2848	. . . . . 6 ⊢ (v = ⟨z, w⟩ → ⦋z / x⦌⦋(2nd ‘v) / y⦌𝐶 = ⦋z / x⦌⦋w / y⦌𝐶)
8	4, 7	eqtrd 2050	. . . . 5 ⊢ (v = ⟨z, w⟩ → ⦋(1st ‘v) / x⦌⦋(2nd ‘v) / y⦌𝐶 = ⦋z / x⦌⦋w / y⦌𝐶)
9	8	eleq1d 2084	. . . 4 ⊢ (v = ⟨z, w⟩ → (⦋(1st ‘v) / x⦌⦋(2nd ‘v) / y⦌𝐶 ∈ 𝐷 ↔ ⦋z / x⦌⦋w / y⦌𝐶 ∈ 𝐷))
10	9	raliunxp 4400	. . 3 ⊢ (∀v ∈ ∪ z ∈ A ({z} × ⦋z / x⦌B)⦋(1st ‘v) / x⦌⦋(2nd ‘v) / y⦌𝐶 ∈ 𝐷 ↔ ∀z ∈ A ∀w ∈ ⦋ z / x⦌B⦋z / x⦌⦋w / y⦌𝐶 ∈ 𝐷)
11		nfv 1398	. . . . . . 7 ⊢ Ⅎz((x ∈ A ∧ y ∈ B) ∧ v = 𝐶)
12		nfv 1398	. . . . . . 7 ⊢ Ⅎw((x ∈ A ∧ y ∈ B) ∧ v = 𝐶)
13		nfv 1398	. . . . . . . . 9 ⊢ Ⅎx z ∈ A
14		nfcsb1v 2855	. . . . . . . . . 10 ⊢ Ⅎx⦋z / x⦌B
15	14	nfcri 2150	. . . . . . . . 9 ⊢ Ⅎx w ∈ ⦋z / x⦌B
16	13, 15	nfan 1435	. . . . . . . 8 ⊢ Ⅎx(z ∈ A ∧ w ∈ ⦋z / x⦌B)
17		nfcsb1v 2855	. . . . . . . . 9 ⊢ Ⅎx⦋z / x⦌⦋w / y⦌𝐶
18	17	nfeq2 2167	. . . . . . . 8 ⊢ Ⅎx v = ⦋z / x⦌⦋w / y⦌𝐶
19	16, 18	nfan 1435	. . . . . . 7 ⊢ Ⅎx((z ∈ A ∧ w ∈ ⦋z / x⦌B) ∧ v = ⦋z / x⦌⦋w / y⦌𝐶)
20		nfv 1398	. . . . . . . 8 ⊢ Ⅎy(z ∈ A ∧ w ∈ ⦋z / x⦌B)
21		nfcv 2156	. . . . . . . . . 10 ⊢ Ⅎyz
22		nfcsb1v 2855	. . . . . . . . . 10 ⊢ Ⅎy⦋w / y⦌𝐶
23	21, 22	nfcsb 2857	. . . . . . . . 9 ⊢ Ⅎy⦋z / x⦌⦋w / y⦌𝐶
24	23	nfeq2 2167	. . . . . . . 8 ⊢ Ⅎy v = ⦋z / x⦌⦋w / y⦌𝐶
25	20, 24	nfan 1435	. . . . . . 7 ⊢ Ⅎy((z ∈ A ∧ w ∈ ⦋z / x⦌B) ∧ v = ⦋z / x⦌⦋w / y⦌𝐶)
26		eleq1 2078	. . . . . . . . . 10 ⊢ (x = z → (x ∈ A ↔ z ∈ A))
27	26	adantr 261	. . . . . . . . 9 ⊢ ((x = z ∧ y = w) → (x ∈ A ↔ z ∈ A))
28		eleq1 2078	. . . . . . . . . 10 ⊢ (y = w → (y ∈ B ↔ w ∈ B))
29		csbeq1a 2833	. . . . . . . . . . 11 ⊢ (x = z → B = ⦋z / x⦌B)
30	29	eleq2d 2085	. . . . . . . . . 10 ⊢ (x = z → (w ∈ B ↔ w ∈ ⦋z / x⦌B))
31	28, 30	sylan9bbr 439	. . . . . . . . 9 ⊢ ((x = z ∧ y = w) → (y ∈ B ↔ w ∈ ⦋z / x⦌B))
32	27, 31	anbi12d 445	. . . . . . . 8 ⊢ ((x = z ∧ y = w) → ((x ∈ A ∧ y ∈ B) ↔ (z ∈ A ∧ w ∈ ⦋z / x⦌B)))
33		csbeq1a 2833	. . . . . . . . . 10 ⊢ (y = w → 𝐶 = ⦋w / y⦌𝐶)
34		csbeq1a 2833	. . . . . . . . . 10 ⊢ (x = z → ⦋w / y⦌𝐶 = ⦋z / x⦌⦋w / y⦌𝐶)
35	33, 34	sylan9eqr 2072	. . . . . . . . 9 ⊢ ((x = z ∧ y = w) → 𝐶 = ⦋z / x⦌⦋w / y⦌𝐶)
36	35	eqeq2d 2029	. . . . . . . 8 ⊢ ((x = z ∧ y = w) → (v = 𝐶 ↔ v = ⦋z / x⦌⦋w / y⦌𝐶))
37	32, 36	anbi12d 445	. . . . . . 7 ⊢ ((x = z ∧ y = w) → (((x ∈ A ∧ y ∈ B) ∧ v = 𝐶) ↔ ((z ∈ A ∧ w ∈ ⦋z / x⦌B) ∧ v = ⦋z / x⦌⦋w / y⦌𝐶)))
38	11, 12, 19, 25, 37	cbvoprab12 5497	. . . . . 6 ⊢ {⟨⟨x, y⟩, v⟩ ∣ ((x ∈ A ∧ y ∈ B) ∧ v = 𝐶)} = {⟨⟨z, w⟩, v⟩ ∣ ((z ∈ A ∧ w ∈ ⦋z / x⦌B) ∧ v = ⦋z / x⦌⦋w / y⦌𝐶)}
39		df-mpt2 5437	. . . . . 6 ⊢ (x ∈ A, y ∈ B ↦ 𝐶) = {⟨⟨x, y⟩, v⟩ ∣ ((x ∈ A ∧ y ∈ B) ∧ v = 𝐶)}
40		df-mpt2 5437	. . . . . 6 ⊢ (z ∈ A, w ∈ ⦋z / x⦌B ↦ ⦋z / x⦌⦋w / y⦌𝐶) = {⟨⟨z, w⟩, v⟩ ∣ ((z ∈ A ∧ w ∈ ⦋z / x⦌B) ∧ v = ⦋z / x⦌⦋w / y⦌𝐶)}
41	38, 39, 40	3eqtr4i 2048	. . . . 5 ⊢ (x ∈ A, y ∈ B ↦ 𝐶) = (z ∈ A, w ∈ ⦋z / x⦌B ↦ ⦋z / x⦌⦋w / y⦌𝐶)
42		fmpt2x.1	. . . . 5 ⊢ 𝐹 = (x ∈ A, y ∈ B ↦ 𝐶)
43	8	mpt2mptx 5514	. . . . 5 ⊢ (v ∈ ∪ z ∈ A ({z} × ⦋z / x⦌B) ↦ ⦋(1st ‘v) / x⦌⦋(2nd ‘v) / y⦌𝐶) = (z ∈ A, w ∈ ⦋z / x⦌B ↦ ⦋z / x⦌⦋w / y⦌𝐶)
44	41, 42, 43	3eqtr4i 2048	. . . 4 ⊢ 𝐹 = (v ∈ ∪ z ∈ A ({z} × ⦋z / x⦌B) ↦ ⦋(1st ‘v) / x⦌⦋(2nd ‘v) / y⦌𝐶)
45	44	fmpt 5240	. . 3 ⊢ (∀v ∈ ∪ z ∈ A ({z} × ⦋z / x⦌B)⦋(1st ‘v) / x⦌⦋(2nd ‘v) / y⦌𝐶 ∈ 𝐷 ↔ 𝐹:∪ z ∈ A ({z} × ⦋z / x⦌B)⟶𝐷)
46	10, 45	bitr3i 175	. 2 ⊢ (∀z ∈ A ∀w ∈ ⦋ z / x⦌B⦋z / x⦌⦋w / y⦌𝐶 ∈ 𝐷 ↔ 𝐹:∪ z ∈ A ({z} × ⦋z / x⦌B)⟶𝐷)
47		nfv 1398	. . 3 ⊢ Ⅎz∀y ∈ B 𝐶 ∈ 𝐷
48	17	nfel1 2166	. . . 4 ⊢ Ⅎx⦋z / x⦌⦋w / y⦌𝐶 ∈ 𝐷
49	14, 48	nfralxy 2334	. . 3 ⊢ Ⅎx∀w ∈ ⦋ z / x⦌B⦋z / x⦌⦋w / y⦌𝐶 ∈ 𝐷
50		nfv 1398	. . . . 5 ⊢ Ⅎw 𝐶 ∈ 𝐷
51	22	nfel1 2166	. . . . 5 ⊢ Ⅎy⦋w / y⦌𝐶 ∈ 𝐷
52	33	eleq1d 2084	. . . . 5 ⊢ (y = w → (𝐶 ∈ 𝐷 ↔ ⦋w / y⦌𝐶 ∈ 𝐷))
53	50, 51, 52	cbvral 2503	. . . 4 ⊢ (∀y ∈ B 𝐶 ∈ 𝐷 ↔ ∀w ∈ B ⦋w / y⦌𝐶 ∈ 𝐷)
54	34	eleq1d 2084	. . . . 5 ⊢ (x = z → (⦋w / y⦌𝐶 ∈ 𝐷 ↔ ⦋z / x⦌⦋w / y⦌𝐶 ∈ 𝐷))
55	29, 54	raleqbidv 2491	. . . 4 ⊢ (x = z → (∀w ∈ B ⦋w / y⦌𝐶 ∈ 𝐷 ↔ ∀w ∈ ⦋ z / x⦌B⦋z / x⦌⦋w / y⦌𝐶 ∈ 𝐷))
56	53, 55	syl5bb 181	. . 3 ⊢ (x = z → (∀y ∈ B 𝐶 ∈ 𝐷 ↔ ∀w ∈ ⦋ z / x⦌B⦋z / x⦌⦋w / y⦌𝐶 ∈ 𝐷))
57	47, 49, 56	cbvral 2503	. 2 ⊢ (∀x ∈ A ∀y ∈ B 𝐶 ∈ 𝐷 ↔ ∀z ∈ A ∀w ∈ ⦋ z / x⦌B⦋z / x⦌⦋w / y⦌𝐶 ∈ 𝐷)
58		nfcv 2156	. . . 4 ⊢ Ⅎz({x} × B)
59		nfcv 2156	. . . . 5 ⊢ Ⅎx{z}
60	59, 14	nfxp 4294	. . . 4 ⊢ Ⅎx({z} × ⦋z / x⦌B)
61		sneq 3357	. . . . 5 ⊢ (x = z → {x} = {z})
62	61, 29	xpeq12d 4293	. . . 4 ⊢ (x = z → ({x} × B) = ({z} × ⦋z / x⦌B))
63	58, 60, 62	cbviun 3664	. . 3 ⊢ ∪ x ∈ A ({x} × B) = ∪ z ∈ A ({z} × ⦋z / x⦌B)
64	63	feq2i 4962	. 2 ⊢ (𝐹:∪ x ∈ A ({x} × B)⟶𝐷 ↔ 𝐹:∪ z ∈ A ({z} × ⦋z / x⦌B)⟶𝐷)
65	46, 57, 64	3bitr4i 201	1 ⊢ (∀x ∈ A ∀y ∈ B 𝐶 ∈ 𝐷 ↔ 𝐹:∪ x ∈ A ({x} × B)⟶𝐷)

Syntax hints:   ∧ wa 97   ↔ wb 98   = wceq 1226   ∈ wcel 1370  ∀wral 2280  ⦋csb 2825  {csn 3346  ⟨cop 3349  ∪ ciun 3627   ↦ cmpt 3788   × cxp 4266  ⟶wf 4821  ‘cfv 4825  {coprab 5433   ↦ cmpt2 5434  1^st c1st 5684  2^nd c2nd 5685

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 617  ax-5 1312  ax-7 1313  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-8 1372  ax-10 1373  ax-11 1374  ax-i12 1375  ax-bnd 1376  ax-4 1377  ax-13 1381  ax-14 1382  ax-17 1396  ax-i9 1400  ax-ial 1405  ax-i5r 1406  ax-ext 2000  ax-sep 3845  ax-pow 3897  ax-pr 3914  ax-un 4116

This theorem depends on definitions:  df-bi 110  df-3an 873  df-tru 1229  df-nf 1326  df-sb 1624  df-eu 1881  df-mo 1882  df-clab 2005  df-cleq 2011  df-clel 2014  df-nfc 2145  df-ral 2285  df-rex 2286  df-rab 2289  df-v 2533  df-sbc 2738  df-csb 2826  df-un 2895  df-in 2897  df-ss 2904  df-pw 3332  df-sn 3352  df-pr 3353  df-op 3355  df-uni 3551  df-iun 3629  df-br 3735  df-opab 3789  df-mpt 3790  df-id 4000  df-xp 4274  df-rel 4275  df-cnv 4276  df-co 4277  df-dm 4278  df-rn 4279  df-res 4280  df-ima 4281  df-iota 4790  df-fun 4827  df-fn 4828  df-f 4829  df-fv 4833  df-oprab 5436  df-mpt2 5437  df-1st 5686  df-2nd 5687

This theorem is referenced by:  fmpt2  5746