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 ∈ B C ∈ D ↔ F : ⋃ x ∈ A x × 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 = z w → 1 st ⁡ v = z
5 4 csbeq1d ⊢ v = z w → ⦋ 1 st ⁡ v / x⦌ ⦋ 2 nd ⁡ v / y⦌ C = ⦋ z / x⦌ ⦋ 2 nd ⁡ v / y⦌ C
6 2 3 op2ndd ⊢ v = z w → 2 nd ⁡ v = w
7 6 csbeq1d ⊢ v = z w → ⦋ 2 nd ⁡ v / y⦌ C = ⦋ w / y⦌ C
8 7 csbeq2dv ⊢ v = z w → ⦋ z / x⦌ ⦋ 2 nd ⁡ v / y⦌ C = ⦋ z / x⦌ ⦋ w / y⦌ C
9 5 8 eqtrd ⊢ v = z w → ⦋ 1 st ⁡ v / x⦌ ⦋ 2 nd ⁡ v / y⦌ C = ⦋ z / x⦌ ⦋ w / y⦌ C
10 9 eleq1d ⊢ v = z w → ⦋ 1 st ⁡ v / x⦌ ⦋ 2 nd ⁡ v / y⦌ C ∈ D ↔ ⦋ z / x⦌ ⦋ w / y⦌ C ∈ D
11 10 raliunxp ⊢ ∀ v ∈ ⋃ z ∈ A z × ⦋ z / x⦌ B ⦋ 1 st ⁡ v / x⦌ ⦋ 2 nd ⁡ v / y⦌ C ∈ D ↔ ∀ z ∈ A ∀ w ∈ ⦋ z / x⦌ B ⦋ z / x⦌ ⦋ w / y⦌ C ∈ D
12 nfv ⊢ Ⅎ z x ∈ A ∧ y ∈ B ∧ v = C
13 nfv ⊢ Ⅎ w x ∈ A ∧ y ∈ B ∧ v = C
14 nfv ⊢ Ⅎ x z ∈ A
15 nfcsb1v ⊢ Ⅎ _ x ⦋ z / x⦌ B
16 15 nfcri ⊢ Ⅎ x w ∈ ⦋ z / x⦌ B
17 14 16 nfan ⊢ Ⅎ x z ∈ A ∧ w ∈ ⦋ z / x⦌ B
18 nfcsb1v ⊢ Ⅎ _ x ⦋ z / x⦌ ⦋ w / y⦌ C
19 18 nfeq2 ⊢ Ⅎ x v = ⦋ z / x⦌ ⦋ w / y⦌ C
20 17 19 nfan ⊢ Ⅎ x z ∈ A ∧ w ∈ ⦋ z / x⦌ B ∧ v = ⦋ z / x⦌ ⦋ w / y⦌ C
21 nfv ⊢ Ⅎ y z ∈ A ∧ w ∈ ⦋ z / x⦌ B
22 nfcv ⊢ Ⅎ _ y z
23 nfcsb1v ⊢ Ⅎ _ y ⦋ w / y⦌ C
24 22 23 nfcsbw ⊢ Ⅎ _ y ⦋ z / x⦌ ⦋ w / y⦌ C
25 24 nfeq2 ⊢ Ⅎ y v = ⦋ z / x⦌ ⦋ w / y⦌ C
26 21 25 nfan ⊢ Ⅎ y z ∈ 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 ⊢ x y v | x ∈ A ∧ y ∈ B ∧ v = C = z w v | z ∈ A ∧ w ∈ ⦋ z / x⦌ B ∧ v = ⦋ z / x⦌ ⦋ w / y⦌ C
40 df-mpo ⊢ x ∈ A , y ∈ B ⟼ C = x y v | x ∈ A ∧ y ∈ B ∧ v = C
41 df-mpo ⊢ z ∈ A , w ∈ ⦋ z / x⦌ B ⟼ ⦋ z / x⦌ ⦋ w / y⦌ C = z w v | 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 ∈ A z × ⦋ z / x⦌ B ⟼ ⦋ 1 st ⁡ v / x⦌ ⦋ 2 nd ⁡ v / y⦌ C = z ∈ A , w ∈ ⦋ z / x⦌ B ⟼ ⦋ z / x⦌ ⦋ w / y⦌ C
44 42 1 43 3eqtr4i ⊢ F = v ∈ ⋃ z ∈ A z × ⦋ z / x⦌ B ⟼ ⦋ 1 st ⁡ v / x⦌ ⦋ 2 nd ⁡ v / y⦌ C
45 44 fmpt ⊢ ∀ v ∈ ⋃ z ∈ A z × ⦋ z / x⦌ B ⦋ 1 st ⁡ v / x⦌ ⦋ 2 nd ⁡ v / y⦌ C ∈ D ↔ F : ⋃ z ∈ A z × ⦋ z / x⦌ B ⟶ D
46 11 45 bitr3i ⊢ ∀ z ∈ A ∀ w ∈ ⦋ z / x⦌ B ⦋ z / x⦌ ⦋ w / y⦌ C ∈ D ↔ F : ⋃ z ∈ A z × ⦋ z / x⦌ B ⟶ D
47 nfv ⊢ Ⅎ z ∀ y ∈ B C ∈ 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 ⊢ Ⅎ w C ∈ 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 ∈ B C ∈ 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 syl5bb ⊢ x = z → ∀ y ∈ B C ∈ D ↔ ∀ w ∈ ⦋ z / x⦌ B ⦋ z / x⦌ ⦋ w / y⦌ C ∈ D
57 47 49 56 cbvralw ⊢ ∀ x ∈ A ∀ y ∈ B C ∈ D ↔ ∀ z ∈ A ∀ w ∈ ⦋ z / x⦌ B ⦋ z / x⦌ ⦋ w / y⦌ C ∈ D
58 nfcv ⊢ Ⅎ _ z x × B
59 nfcv ⊢ Ⅎ _ x z
60 59 15 nfxp ⊢ Ⅎ _ x z × ⦋ 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 ∈ A x × B = ⋃ z ∈ A z × ⦋ z / x⦌ B
64 63 feq2i ⊢ F : ⋃ x ∈ A x × B ⟶ D ↔ F : ⋃ z ∈ A z × ⦋ z / x⦌ B ⟶ D
65 46 57 64 3bitr4i ⊢ ∀ x ∈ A ∀ y ∈ B C ∈ D ↔ F : ⋃ x ∈ A x × B ⟶ D