Metamath Proof Explorer

Theorem fmpox

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)

Ref Expression
Hypothesis fmpox.1 ⊢F=x∈A,y∈B⟼C
Assertion fmpox ⊢∀x∈A∀y∈BC∈D↔F:⋃x∈Ax×B⟶D

Proof

Step Hyp Ref Expression
1 fmpox.1 ⊢F=x∈A,y∈B⟼C
2 vex ⊢z∈V
3 vex ⊢w∈V
4 2 3 op1std ⊢v=zw→1st⁡v=z
5 4 csbeq1d ⊢v=zw→⦋1st⁡v/x⦌⦋2nd⁡v/y⦌C=⦋z/x⦌⦋2nd⁡v/y⦌C
6 2 3 op2ndd ⊢v=zw→2nd⁡v=w
7 6 csbeq1d ⊢v=zw→⦋2nd⁡v/y⦌C=⦋w/y⦌C
8 7 csbeq2dv ⊢v=zw→⦋z/x⦌⦋2nd⁡v/y⦌C=⦋z/x⦌⦋w/y⦌C
9 5 8 eqtrd ⊢v=zw→⦋1st⁡v/x⦌⦋2nd⁡v/y⦌C=⦋z/x⦌⦋w/y⦌C
10 9 eleq1d ⊢v=zw→⦋1st⁡v/x⦌⦋2nd⁡v/y⦌C∈D↔⦋z/x⦌⦋w/y⦌C∈D
11 10 raliunxp ⊢∀v∈⋃z∈Az×⦋z/x⦌B⦋1st⁡v/x⦌⦋2nd⁡v/y⦌C∈D↔∀z∈A∀w∈⦋z/x⦌B⦋z/x⦌⦋w/y⦌C∈D
12 nfv ⊢Ⅎzx∈A∧y∈B∧v=C
13 nfv ⊢Ⅎwx∈A∧y∈B∧v=C
14 nfv ⊢Ⅎxz∈A
15 nfcsb1v ⊢Ⅎ_x⦋z/x⦌B
16 15 nfcri ⊢Ⅎxw∈⦋z/x⦌B
17 14 16 nfan ⊢Ⅎxz∈A∧w∈⦋z/x⦌B
18 nfcsb1v ⊢Ⅎ_x⦋z/x⦌⦋w/y⦌C
19 18 nfeq2 ⊢Ⅎxv=⦋z/x⦌⦋w/y⦌C
20 17 19 nfan ⊢Ⅎxz∈A∧w∈⦋z/x⦌B∧v=⦋z/x⦌⦋w/y⦌C
21 nfv ⊢Ⅎyz∈A∧w∈⦋z/x⦌B
22 nfcv ⊢Ⅎ_yz
23 nfcsb1v ⊢Ⅎ_y⦋w/y⦌C
24 22 23 nfcsbw ⊢Ⅎ_y⦋z/x⦌⦋w/y⦌C
25 24 nfeq2 ⊢Ⅎyv=⦋z/x⦌⦋w/y⦌C
26 21 25 nfan ⊢Ⅎyz∈A∧w∈⦋z/x⦌B∧v=⦋z/x⦌⦋w/y⦌C
27 eleq1w ⊢x=z→x∈A↔z∈A
28 27 adantr ⊢x=z∧y=w→x∈A↔z∈A
29 eleq1w ⊢y=w→y∈B↔w∈B
30 csbeq1a ⊢x=z→B=⦋z/x⦌B
31 30 eleq2d ⊢x=z→w∈B↔w∈⦋z/x⦌B
32 29 31 sylan9bbr ⊢x=z∧y=w→y∈B↔w∈⦋z/x⦌B
33 28 32 anbi12d ⊢x=z∧y=w→x∈A∧y∈B↔z∈A∧w∈⦋z/x⦌B
34 csbeq1a ⊢y=w→C=⦋w/y⦌C
35 csbeq1a ⊢x=z→⦋w/y⦌C=⦋z/x⦌⦋w/y⦌C
36 34 35 sylan9eqr ⊢x=z∧y=w→C=⦋z/x⦌⦋w/y⦌C
37 36 eqeq2d ⊢x=z∧y=w→v=C↔v=⦋z/x⦌⦋w/y⦌C
38 33 37 anbi12d ⊢x=z∧y=w→x∈A∧y∈B∧v=C↔z∈A∧w∈⦋z/x⦌B∧v=⦋z/x⦌⦋w/y⦌C
39 12 13 20 26 38 cbvoprab12 ⊢xyv|x∈A∧y∈B∧v=C=zwv|z∈A∧w∈⦋z/x⦌B∧v=⦋z/x⦌⦋w/y⦌C
40 df-mpo ⊢x∈A,y∈B⟼C=xyv|x∈A∧y∈B∧v=C
41 df-mpo ⊢z∈A,w∈⦋z/x⦌B⟼⦋z/x⦌⦋w/y⦌C=zwv|z∈A∧w∈⦋z/x⦌B∧v=⦋z/x⦌⦋w/y⦌C
42 39 40 41 3eqtr4i ⊢x∈A,y∈B⟼C=z∈A,w∈⦋z/x⦌B⟼⦋z/x⦌⦋w/y⦌C
43 9 mpomptx ⊢v∈⋃z∈Az×⦋z/x⦌B⟼⦋1st⁡v/x⦌⦋2nd⁡v/y⦌C=z∈A,w∈⦋z/x⦌B⟼⦋z/x⦌⦋w/y⦌C
44 42 1 43 3eqtr4i ⊢F=v∈⋃z∈Az×⦋z/x⦌B⟼⦋1st⁡v/x⦌⦋2nd⁡v/y⦌C
45 44 fmpt ⊢∀v∈⋃z∈Az×⦋z/x⦌B⦋1st⁡v/x⦌⦋2nd⁡v/y⦌C∈D↔F:⋃z∈Az×⦋z/x⦌B⟶D
46 11 45 bitr3i ⊢∀z∈A∀w∈⦋z/x⦌B⦋z/x⦌⦋w/y⦌C∈D↔F:⋃z∈Az×⦋z/x⦌B⟶D
47 nfv ⊢Ⅎz∀y∈BC∈D
48 18 nfel1 ⊢Ⅎx⦋z/x⦌⦋w/y⦌C∈D
49 15 48 nfralw ⊢Ⅎx∀w∈⦋z/x⦌B⦋z/x⦌⦋w/y⦌C∈D
50 nfv ⊢ℲwC∈D
51 23 nfel1 ⊢Ⅎy⦋w/y⦌C∈D
52 34 eleq1d ⊢y=w→C∈D↔⦋w/y⦌C∈D
53 50 51 52 cbvralw ⊢∀y∈BC∈D↔∀w∈B⦋w/y⦌C∈D
54 35 eleq1d ⊢x=z→⦋w/y⦌C∈D↔⦋z/x⦌⦋w/y⦌C∈D
55 30 54 raleqbidv ⊢x=z→∀w∈B⦋w/y⦌C∈D↔∀w∈⦋z/x⦌B⦋z/x⦌⦋w/y⦌C∈D
56 53 55 bitrid ⊢x=z→∀y∈BC∈D↔∀w∈⦋z/x⦌B⦋z/x⦌⦋w/y⦌C∈D
57 47 49 56 cbvralw ⊢∀x∈A∀y∈BC∈D↔∀z∈A∀w∈⦋z/x⦌B⦋z/x⦌⦋w/y⦌C∈D
58 nfcv ⊢Ⅎ_zx×B
59 nfcv ⊢Ⅎ_xz
60 59 15 nfxp ⊢Ⅎ_xz×⦋z/x⦌B
61 sneq ⊢x=z→x=z
62 61 30 xpeq12d ⊢x=z→x×B=z×⦋z/x⦌B
63 58 60 62 cbviun ⊢⋃x∈Ax×B=⋃z∈Az×⦋z/x⦌B
64 63 feq2i ⊢F:⋃x∈Ax×B⟶D↔F:⋃z∈Az×⦋z/x⦌B⟶D
65 46 57 64 3bitr4i ⊢∀x∈A∀y∈BC∈D↔F:⋃x∈Ax×B⟶D