Theorem fmpt2x 5768

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 2554	. . . . . . . 8 ⊢ z ∈ V
2		vex 2554	. . . . . . . 8 ⊢ w ∈ V
3	1, 2	op1std 5717	. . . . . . 7 ⊢ (v = ⟨z, w⟩ → (1st ‘v) = z)
4	3	csbeq1d 2852	. . . . . 6 ⊢ (v = ⟨z, w⟩ → ⦋(1st ‘v) / x⦌⦋(2nd ‘v) / y⦌𝐶 = ⦋z / x⦌⦋(2nd ‘v) / y⦌𝐶)
5	1, 2	op2ndd 5718	. . . . . . . 8 ⊢ (v = ⟨z, w⟩ → (2nd ‘v) = w)
6	5	csbeq1d 2852	. . . . . . 7 ⊢ (v = ⟨z, w⟩ → ⦋(2nd ‘v) / y⦌𝐶 = ⦋w / y⦌𝐶)
7	6	csbeq2dv 2869	. . . . . 6 ⊢ (v = ⟨z, w⟩ → ⦋z / x⦌⦋(2nd ‘v) / y⦌𝐶 = ⦋z / x⦌⦋w / y⦌𝐶)
8	4, 7	eqtrd 2069	. . . . 5 ⊢ (v = ⟨z, w⟩ → ⦋(1st ‘v) / x⦌⦋(2nd ‘v) / y⦌𝐶 = ⦋z / x⦌⦋w / y⦌𝐶)
9	8	eleq1d 2103	. . . 4 ⊢ (v = ⟨z, w⟩ → (⦋(1st ‘v) / x⦌⦋(2nd ‘v) / y⦌𝐶 ∈ 𝐷 ↔ ⦋z / x⦌⦋w / y⦌𝐶 ∈ 𝐷))
10	9	raliunxp 4420	. . 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 1418	. . . . . . 7 ⊢ Ⅎz((x ∈ A ∧ y ∈ B) ∧ v = 𝐶)
12		nfv 1418	. . . . . . 7 ⊢ Ⅎw((x ∈ A ∧ y ∈ B) ∧ v = 𝐶)
13		nfv 1418	. . . . . . . . 9 ⊢ Ⅎx z ∈ A
14		nfcsb1v 2876	. . . . . . . . . 10 ⊢ Ⅎx⦋z / x⦌B
15	14	nfcri 2169	. . . . . . . . 9 ⊢ Ⅎx w ∈ ⦋z / x⦌B
16	13, 15	nfan 1454	. . . . . . . 8 ⊢ Ⅎx(z ∈ A ∧ w ∈ ⦋z / x⦌B)
17		nfcsb1v 2876	. . . . . . . . 9 ⊢ Ⅎx⦋z / x⦌⦋w / y⦌𝐶
18	17	nfeq2 2186	. . . . . . . 8 ⊢ Ⅎx v = ⦋z / x⦌⦋w / y⦌𝐶
19	16, 18	nfan 1454	. . . . . . 7 ⊢ Ⅎx((z ∈ A ∧ w ∈ ⦋z / x⦌B) ∧ v = ⦋z / x⦌⦋w / y⦌𝐶)
20		nfv 1418	. . . . . . . 8 ⊢ Ⅎy(z ∈ A ∧ w ∈ ⦋z / x⦌B)
21		nfcv 2175	. . . . . . . . . 10 ⊢ Ⅎyz
22		nfcsb1v 2876	. . . . . . . . . 10 ⊢ Ⅎy⦋w / y⦌𝐶
23	21, 22	nfcsb 2878	. . . . . . . . 9 ⊢ Ⅎy⦋z / x⦌⦋w / y⦌𝐶
24	23	nfeq2 2186	. . . . . . . 8 ⊢ Ⅎy v = ⦋z / x⦌⦋w / y⦌𝐶
25	20, 24	nfan 1454	. . . . . . 7 ⊢ Ⅎy((z ∈ A ∧ w ∈ ⦋z / x⦌B) ∧ v = ⦋z / x⦌⦋w / y⦌𝐶)
26		eleq1 2097	. . . . . . . . . 10 ⊢ (x = z → (x ∈ A ↔ z ∈ A))
27	26	adantr 261	. . . . . . . . 9 ⊢ ((x = z ∧ y = w) → (x ∈ A ↔ z ∈ A))
28		eleq1 2097	. . . . . . . . . 10 ⊢ (y = w → (y ∈ B ↔ w ∈ B))
29		csbeq1a 2854	. . . . . . . . . . 11 ⊢ (x = z → B = ⦋z / x⦌B)
30	29	eleq2d 2104	. . . . . . . . . 10 ⊢ (x = z → (w ∈ B ↔ w ∈ ⦋z / x⦌B))
31	28, 30	sylan9bbr 436	. . . . . . . . 9 ⊢ ((x = z ∧ y = w) → (y ∈ B ↔ w ∈ ⦋z / x⦌B))
32	27, 31	anbi12d 442	. . . . . . . 8 ⊢ ((x = z ∧ y = w) → ((x ∈ A ∧ y ∈ B) ↔ (z ∈ A ∧ w ∈ ⦋z / x⦌B)))
33		csbeq1a 2854	. . . . . . . . . 10 ⊢ (y = w → 𝐶 = ⦋w / y⦌𝐶)
34		csbeq1a 2854	. . . . . . . . . 10 ⊢ (x = z → ⦋w / y⦌𝐶 = ⦋z / x⦌⦋w / y⦌𝐶)
35	33, 34	sylan9eqr 2091	. . . . . . . . 9 ⊢ ((x = z ∧ y = w) → 𝐶 = ⦋z / x⦌⦋w / y⦌𝐶)
36	35	eqeq2d 2048	. . . . . . . 8 ⊢ ((x = z ∧ y = w) → (v = 𝐶 ↔ v = ⦋z / x⦌⦋w / y⦌𝐶))
37	32, 36	anbi12d 442	. . . . . . 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 5520	. . . . . 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 5460	. . . . . 6 ⊢ (x ∈ A, y ∈ B ↦ 𝐶) = {⟨⟨x, y⟩, v⟩ ∣ ((x ∈ A ∧ y ∈ B) ∧ v = 𝐶)}
40		df-mpt2 5460	. . . . . 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 2067	. . . . 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 5537	. . . . 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 2067	. . . 4 ⊢ 𝐹 = (v ∈ ∪ z ∈ A ({z} × ⦋z / x⦌B) ↦ ⦋(1st ‘v) / x⦌⦋(2nd ‘v) / y⦌𝐶)
45	44	fmpt 5262	. . 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 1418	. . 3 ⊢ Ⅎz∀y ∈ B 𝐶 ∈ 𝐷
48	17	nfel1 2185	. . . 4 ⊢ Ⅎx⦋z / x⦌⦋w / y⦌𝐶 ∈ 𝐷
49	14, 48	nfralxy 2354	. . 3 ⊢ Ⅎx∀w ∈ ⦋ z / x⦌B⦋z / x⦌⦋w / y⦌𝐶 ∈ 𝐷
50		nfv 1418	. . . . 5 ⊢ Ⅎw 𝐶 ∈ 𝐷
51	22	nfel1 2185	. . . . 5 ⊢ Ⅎy⦋w / y⦌𝐶 ∈ 𝐷
52	33	eleq1d 2103	. . . . 5 ⊢ (y = w → (𝐶 ∈ 𝐷 ↔ ⦋w / y⦌𝐶 ∈ 𝐷))
53	50, 51, 52	cbvral 2523	. . . 4 ⊢ (∀y ∈ B 𝐶 ∈ 𝐷 ↔ ∀w ∈ B ⦋w / y⦌𝐶 ∈ 𝐷)
54	34	eleq1d 2103	. . . . 5 ⊢ (x = z → (⦋w / y⦌𝐶 ∈ 𝐷 ↔ ⦋z / x⦌⦋w / y⦌𝐶 ∈ 𝐷))
55	29, 54	raleqbidv 2511	. . . 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 2523	. 2 ⊢ (∀x ∈ A ∀y ∈ B 𝐶 ∈ 𝐷 ↔ ∀z ∈ A ∀w ∈ ⦋ z / x⦌B⦋z / x⦌⦋w / y⦌𝐶 ∈ 𝐷)
58		nfcv 2175	. . . 4 ⊢ Ⅎz({x} × B)
59		nfcv 2175	. . . . 5 ⊢ Ⅎx{z}
60	59, 14	nfxp 4314	. . . 4 ⊢ Ⅎx({z} × ⦋z / x⦌B)
61		sneq 3378	. . . . 5 ⊢ (x = z → {x} = {z})
62	61, 29	xpeq12d 4313	. . . 4 ⊢ (x = z → ({x} × B) = ({z} × ⦋z / x⦌B))
63	58, 60, 62	cbviun 3685	. . 3 ⊢ ∪ x ∈ A ({x} × B) = ∪ z ∈ A ({z} × ⦋z / x⦌B)
64	63	feq2i 4983	. 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 1242   ∈ wcel 1390  ∀wral 2300  ⦋csb 2846  {csn 3367  ⟨cop 3370  ∪ ciun 3648   ↦ cmpt 3809   × cxp 4286  ⟶wf 4841  ‘cfv 4845  {coprab 5456   ↦ cmpt2 5457  1^st c1st 5707  2^nd c2nd 5708

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 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-13 1401  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935  ax-un 4136

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-rab 2309  df-v 2553  df-sbc 2759  df-csb 2847  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-iun 3650  df-br 3756  df-opab 3810  df-mpt 3811  df-id 4021  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-rn 4299  df-res 4300  df-ima 4301  df-iota 4810  df-fun 4847  df-fn 4848  df-f 4849  df-fv 4853  df-oprab 5459  df-mpt2 5460  df-1st 5709  df-2nd 5710

This theorem is referenced by:  fmpt2  5769