Metamath Proof Explorer

Theorem el2mpocsbcl

Description: If the operation value of the operation value of two nested maps-to notation is not empty, all involved arguments belong to the corresponding base classes of the maps-to notations. (Contributed by AV, 21-May-2021)

Ref Expression
Hypothesis el2mpocsbcl.o ⊢ O = x ∈ A , y ∈ B ⟼ s ∈ C , t ∈ D ⟼ E
Assertion el2mpocsbcl ⊢ ∀ x ∈ A ∀ y ∈ B C ∈ U ∧ D ∈ V → W ∈ S X O Y T → X ∈ A ∧ Y ∈ B ∧ S ∈ ⦋ X / x⦌ ⦋ Y / y⦌ C ∧ T ∈ ⦋ X / x⦌ ⦋ Y / y⦌ D

Proof

Step Hyp Ref Expression
1 el2mpocsbcl.o ⊢ O = x ∈ A , y ∈ B ⟼ s ∈ C , t ∈ D ⟼ E
2 simpl ⊢ X ∈ A ∧ Y ∈ B ∧ ∀ x ∈ A ∀ y ∈ B C ∈ U ∧ D ∈ V ∧ W ∈ S X O Y T → X ∈ A ∧ Y ∈ B
3 nfcv ⊢ Ⅎ _ a s ∈ C , t ∈ D ⟼ E
4 nfcv ⊢ Ⅎ _ b s ∈ C , t ∈ D ⟼ E
5 nfcsb1v ⊢ Ⅎ _ x ⦋ a / x⦌ ⦋ b / y⦌ C
6 nfcsb1v ⊢ Ⅎ _ x ⦋ a / x⦌ ⦋ b / y⦌ D
7 nfcsb1v ⊢ Ⅎ _ x ⦋ a / x⦌ ⦋ b / y⦌ E
8 5 6 7 nfmpo ⊢ Ⅎ _ x s ∈ ⦋ a / x⦌ ⦋ b / y⦌ C , t ∈ ⦋ a / x⦌ ⦋ b / y⦌ D ⟼ ⦋ a / x⦌ ⦋ b / y⦌ E
9 nfcv ⊢ Ⅎ _ y a
10 nfcsb1v ⊢ Ⅎ _ y ⦋ b / y⦌ C
11 9 10 nfcsbw ⊢ Ⅎ _ y ⦋ a / x⦌ ⦋ b / y⦌ C
12 nfcsb1v ⊢ Ⅎ _ y ⦋ b / y⦌ D
13 9 12 nfcsbw ⊢ Ⅎ _ y ⦋ a / x⦌ ⦋ b / y⦌ D
14 nfcsb1v ⊢ Ⅎ _ y ⦋ b / y⦌ E
15 9 14 nfcsbw ⊢ Ⅎ _ y ⦋ a / x⦌ ⦋ b / y⦌ E
16 11 13 15 nfmpo ⊢ Ⅎ _ y s ∈ ⦋ a / x⦌ ⦋ b / y⦌ C , t ∈ ⦋ a / x⦌ ⦋ b / y⦌ D ⟼ ⦋ a / x⦌ ⦋ b / y⦌ E
17 csbeq1a ⊢ x = a → C = ⦋ a / x⦌ C
18 csbeq1a ⊢ y = b → C = ⦋ b / y⦌ C
19 18 csbeq2dv ⊢ y = b → ⦋ a / x⦌ C = ⦋ a / x⦌ ⦋ b / y⦌ C
20 17 19 sylan9eq ⊢ x = a ∧ y = b → C = ⦋ a / x⦌ ⦋ b / y⦌ C
21 csbeq1a ⊢ x = a → D = ⦋ a / x⦌ D
22 csbeq1a ⊢ y = b → D = ⦋ b / y⦌ D
23 22 csbeq2dv ⊢ y = b → ⦋ a / x⦌ D = ⦋ a / x⦌ ⦋ b / y⦌ D
24 21 23 sylan9eq ⊢ x = a ∧ y = b → D = ⦋ a / x⦌ ⦋ b / y⦌ D
25 csbeq1a ⊢ x = a → E = ⦋ a / x⦌ E
26 csbeq1a ⊢ y = b → E = ⦋ b / y⦌ E
27 26 csbeq2dv ⊢ y = b → ⦋ a / x⦌ E = ⦋ a / x⦌ ⦋ b / y⦌ E
28 25 27 sylan9eq ⊢ x = a ∧ y = b → E = ⦋ a / x⦌ ⦋ b / y⦌ E
29 20 24 28 mpoeq123dv ⊢ x = a ∧ y = b → s ∈ C , t ∈ D ⟼ E = s ∈ ⦋ a / x⦌ ⦋ b / y⦌ C , t ∈ ⦋ a / x⦌ ⦋ b / y⦌ D ⟼ ⦋ a / x⦌ ⦋ b / y⦌ E
30 3 4 8 16 29 cbvmpo ⊢ x ∈ A , y ∈ B ⟼ s ∈ C , t ∈ D ⟼ E = a ∈ A , b ∈ B ⟼ s ∈ ⦋ a / x⦌ ⦋ b / y⦌ C , t ∈ ⦋ a / x⦌ ⦋ b / y⦌ D ⟼ ⦋ a / x⦌ ⦋ b / y⦌ E
31 1 30 eqtri ⊢ O = a ∈ A , b ∈ B ⟼ s ∈ ⦋ a / x⦌ ⦋ b / y⦌ C , t ∈ ⦋ a / x⦌ ⦋ b / y⦌ D ⟼ ⦋ a / x⦌ ⦋ b / y⦌ E
32 31 a1i ⊢ ∀ x ∈ A ∀ y ∈ B C ∈ U ∧ D ∈ V ∧ X ∈ A ∧ Y ∈ B → O = a ∈ A , b ∈ B ⟼ s ∈ ⦋ a / x⦌ ⦋ b / y⦌ C , t ∈ ⦋ a / x⦌ ⦋ b / y⦌ D ⟼ ⦋ a / x⦌ ⦋ b / y⦌ E
33 csbeq1 ⊢ a = X → ⦋ a / x⦌ ⦋ b / y⦌ C = ⦋ X / x⦌ ⦋ b / y⦌ C
34 33 adantr ⊢ a = X ∧ b = Y → ⦋ a / x⦌ ⦋ b / y⦌ C = ⦋ X / x⦌ ⦋ b / y⦌ C
35 csbeq1 ⊢ b = Y → ⦋ b / y⦌ C = ⦋ Y / y⦌ C
36 35 adantl ⊢ a = X ∧ b = Y → ⦋ b / y⦌ C = ⦋ Y / y⦌ C
37 36 csbeq2dv ⊢ a = X ∧ b = Y → ⦋ X / x⦌ ⦋ b / y⦌ C = ⦋ X / x⦌ ⦋ Y / y⦌ C
38 34 37 eqtrd ⊢ a = X ∧ b = Y → ⦋ a / x⦌ ⦋ b / y⦌ C = ⦋ X / x⦌ ⦋ Y / y⦌ C
39 csbeq1 ⊢ a = X → ⦋ a / x⦌ ⦋ b / y⦌ D = ⦋ X / x⦌ ⦋ b / y⦌ D
40 39 adantr ⊢ a = X ∧ b = Y → ⦋ a / x⦌ ⦋ b / y⦌ D = ⦋ X / x⦌ ⦋ b / y⦌ D
41 csbeq1 ⊢ b = Y → ⦋ b / y⦌ D = ⦋ Y / y⦌ D
42 41 adantl ⊢ a = X ∧ b = Y → ⦋ b / y⦌ D = ⦋ Y / y⦌ D
43 42 csbeq2dv ⊢ a = X ∧ b = Y → ⦋ X / x⦌ ⦋ b / y⦌ D = ⦋ X / x⦌ ⦋ Y / y⦌ D
44 40 43 eqtrd ⊢ a = X ∧ b = Y → ⦋ a / x⦌ ⦋ b / y⦌ D = ⦋ X / x⦌ ⦋ Y / y⦌ D
45 csbeq1 ⊢ a = X → ⦋ a / x⦌ ⦋ b / y⦌ E = ⦋ X / x⦌ ⦋ b / y⦌ E
46 45 adantr ⊢ a = X ∧ b = Y → ⦋ a / x⦌ ⦋ b / y⦌ E = ⦋ X / x⦌ ⦋ b / y⦌ E
47 csbeq1 ⊢ b = Y → ⦋ b / y⦌ E = ⦋ Y / y⦌ E
48 47 adantl ⊢ a = X ∧ b = Y → ⦋ b / y⦌ E = ⦋ Y / y⦌ E
49 48 csbeq2dv ⊢ a = X ∧ b = Y → ⦋ X / x⦌ ⦋ b / y⦌ E = ⦋ X / x⦌ ⦋ Y / y⦌ E
50 46 49 eqtrd ⊢ a = X ∧ b = Y → ⦋ a / x⦌ ⦋ b / y⦌ E = ⦋ X / x⦌ ⦋ Y / y⦌ E
51 38 44 50 mpoeq123dv ⊢ a = X ∧ b = Y → s ∈ ⦋ a / x⦌ ⦋ b / y⦌ C , t ∈ ⦋ a / x⦌ ⦋ b / y⦌ D ⟼ ⦋ a / x⦌ ⦋ b / y⦌ E = s ∈ ⦋ X / x⦌ ⦋ Y / y⦌ C , t ∈ ⦋ X / x⦌ ⦋ Y / y⦌ D ⟼ ⦋ X / x⦌ ⦋ Y / y⦌ E
52 51 adantl ⊢ ∀ x ∈ A ∀ y ∈ B C ∈ U ∧ D ∈ V ∧ X ∈ A ∧ Y ∈ B ∧ a = X ∧ b = Y → s ∈ ⦋ a / x⦌ ⦋ b / y⦌ C , t ∈ ⦋ a / x⦌ ⦋ b / y⦌ D ⟼ ⦋ a / x⦌ ⦋ b / y⦌ E = s ∈ ⦋ X / x⦌ ⦋ Y / y⦌ C , t ∈ ⦋ X / x⦌ ⦋ Y / y⦌ D ⟼ ⦋ X / x⦌ ⦋ Y / y⦌ E
53 simpl ⊢ X ∈ A ∧ Y ∈ B → X ∈ A
54 53 adantl ⊢ ∀ x ∈ A ∀ y ∈ B C ∈ U ∧ D ∈ V ∧ X ∈ A ∧ Y ∈ B → X ∈ A
55 simpr ⊢ X ∈ A ∧ Y ∈ B → Y ∈ B
56 55 adantl ⊢ ∀ x ∈ A ∀ y ∈ B C ∈ U ∧ D ∈ V ∧ X ∈ A ∧ Y ∈ B → Y ∈ B
57 simpl ⊢ C ∈ U ∧ D ∈ V → C ∈ U
58 57 ralimi ⊢ ∀ y ∈ B C ∈ U ∧ D ∈ V → ∀ y ∈ B C ∈ U
59 rspcsbela ⊢ Y ∈ B ∧ ∀ y ∈ B C ∈ U → ⦋ Y / y⦌ C ∈ U
60 55 58 59 syl2an ⊢ X ∈ A ∧ Y ∈ B ∧ ∀ y ∈ B C ∈ U ∧ D ∈ V → ⦋ Y / y⦌ C ∈ U
61 60 ex ⊢ X ∈ A ∧ Y ∈ B → ∀ y ∈ B C ∈ U ∧ D ∈ V → ⦋ Y / y⦌ C ∈ U
62 61 ralimdv ⊢ X ∈ A ∧ Y ∈ B → ∀ x ∈ A ∀ y ∈ B C ∈ U ∧ D ∈ V → ∀ x ∈ A ⦋ Y / y⦌ C ∈ U
63 62 impcom ⊢ ∀ x ∈ A ∀ y ∈ B C ∈ U ∧ D ∈ V ∧ X ∈ A ∧ Y ∈ B → ∀ x ∈ A ⦋ Y / y⦌ C ∈ U
64 rspcsbela ⊢ X ∈ A ∧ ∀ x ∈ A ⦋ Y / y⦌ C ∈ U → ⦋ X / x⦌ ⦋ Y / y⦌ C ∈ U
65 54 63 64 syl2anc ⊢ ∀ x ∈ A ∀ y ∈ B C ∈ U ∧ D ∈ V ∧ X ∈ A ∧ Y ∈ B → ⦋ X / x⦌ ⦋ Y / y⦌ C ∈ U
66 simpr ⊢ C ∈ U ∧ D ∈ V → D ∈ V
67 66 ralimi ⊢ ∀ y ∈ B C ∈ U ∧ D ∈ V → ∀ y ∈ B D ∈ V
68 rspcsbela ⊢ Y ∈ B ∧ ∀ y ∈ B D ∈ V → ⦋ Y / y⦌ D ∈ V
69 55 67 68 syl2an ⊢ X ∈ A ∧ Y ∈ B ∧ ∀ y ∈ B C ∈ U ∧ D ∈ V → ⦋ Y / y⦌ D ∈ V
70 69 ex ⊢ X ∈ A ∧ Y ∈ B → ∀ y ∈ B C ∈ U ∧ D ∈ V → ⦋ Y / y⦌ D ∈ V
71 70 ralimdv ⊢ X ∈ A ∧ Y ∈ B → ∀ x ∈ A ∀ y ∈ B C ∈ U ∧ D ∈ V → ∀ x ∈ A ⦋ Y / y⦌ D ∈ V
72 71 impcom ⊢ ∀ x ∈ A ∀ y ∈ B C ∈ U ∧ D ∈ V ∧ X ∈ A ∧ Y ∈ B → ∀ x ∈ A ⦋ Y / y⦌ D ∈ V
73 rspcsbela ⊢ X ∈ A ∧ ∀ x ∈ A ⦋ Y / y⦌ D ∈ V → ⦋ X / x⦌ ⦋ Y / y⦌ D ∈ V
74 54 72 73 syl2anc ⊢ ∀ x ∈ A ∀ y ∈ B C ∈ U ∧ D ∈ V ∧ X ∈ A ∧ Y ∈ B → ⦋ X / x⦌ ⦋ Y / y⦌ D ∈ V
75 mpoexga ⊢ ⦋ X / x⦌ ⦋ Y / y⦌ C ∈ U ∧ ⦋ X / x⦌ ⦋ Y / y⦌ D ∈ V → s ∈ ⦋ X / x⦌ ⦋ Y / y⦌ C , t ∈ ⦋ X / x⦌ ⦋ Y / y⦌ D ⟼ ⦋ X / x⦌ ⦋ Y / y⦌ E ∈ V
76 65 74 75 syl2anc ⊢ ∀ x ∈ A ∀ y ∈ B C ∈ U ∧ D ∈ V ∧ X ∈ A ∧ Y ∈ B → s ∈ ⦋ X / x⦌ ⦋ Y / y⦌ C , t ∈ ⦋ X / x⦌ ⦋ Y / y⦌ D ⟼ ⦋ X / x⦌ ⦋ Y / y⦌ E ∈ V
77 32 52 54 56 76 ovmpod ⊢ ∀ x ∈ A ∀ y ∈ B C ∈ U ∧ D ∈ V ∧ X ∈ A ∧ Y ∈ B → X O Y = s ∈ ⦋ X / x⦌ ⦋ Y / y⦌ C , t ∈ ⦋ X / x⦌ ⦋ Y / y⦌ D ⟼ ⦋ X / x⦌ ⦋ Y / y⦌ E
78 77 oveqd ⊢ ∀ x ∈ A ∀ y ∈ B C ∈ U ∧ D ∈ V ∧ X ∈ A ∧ Y ∈ B → S X O Y T = S s ∈ ⦋ X / x⦌ ⦋ Y / y⦌ C , t ∈ ⦋ X / x⦌ ⦋ Y / y⦌ D ⟼ ⦋ X / x⦌ ⦋ Y / y⦌ E T
79 78 eleq2d ⊢ ∀ x ∈ A ∀ y ∈ B C ∈ U ∧ D ∈ V ∧ X ∈ A ∧ Y ∈ B → W ∈ S X O Y T ↔ W ∈ S s ∈ ⦋ X / x⦌ ⦋ Y / y⦌ C , t ∈ ⦋ X / x⦌ ⦋ Y / y⦌ D ⟼ ⦋ X / x⦌ ⦋ Y / y⦌ E T
80 eqid ⊢ s ∈ ⦋ X / x⦌ ⦋ Y / y⦌ C , t ∈ ⦋ X / x⦌ ⦋ Y / y⦌ D ⟼ ⦋ X / x⦌ ⦋ Y / y⦌ E = s ∈ ⦋ X / x⦌ ⦋ Y / y⦌ C , t ∈ ⦋ X / x⦌ ⦋ Y / y⦌ D ⟼ ⦋ X / x⦌ ⦋ Y / y⦌ E
81 80 elmpocl ⊢ W ∈ S s ∈ ⦋ X / x⦌ ⦋ Y / y⦌ C , t ∈ ⦋ X / x⦌ ⦋ Y / y⦌ D ⟼ ⦋ X / x⦌ ⦋ Y / y⦌ E T → S ∈ ⦋ X / x⦌ ⦋ Y / y⦌ C ∧ T ∈ ⦋ X / x⦌ ⦋ Y / y⦌ D
82 79 81 syl6bi ⊢ ∀ x ∈ A ∀ y ∈ B C ∈ U ∧ D ∈ V ∧ X ∈ A ∧ Y ∈ B → W ∈ S X O Y T → S ∈ ⦋ X / x⦌ ⦋ Y / y⦌ C ∧ T ∈ ⦋ X / x⦌ ⦋ Y / y⦌ D
83 82 impancom ⊢ ∀ x ∈ A ∀ y ∈ B C ∈ U ∧ D ∈ V ∧ W ∈ S X O Y T → X ∈ A ∧ Y ∈ B → S ∈ ⦋ X / x⦌ ⦋ Y / y⦌ C ∧ T ∈ ⦋ X / x⦌ ⦋ Y / y⦌ D
84 83 impcom ⊢ X ∈ A ∧ Y ∈ B ∧ ∀ x ∈ A ∀ y ∈ B C ∈ U ∧ D ∈ V ∧ W ∈ S X O Y T → S ∈ ⦋ X / x⦌ ⦋ Y / y⦌ C ∧ T ∈ ⦋ X / x⦌ ⦋ Y / y⦌ D
85 2 84 jca ⊢ X ∈ A ∧ Y ∈ B ∧ ∀ x ∈ A ∀ y ∈ B C ∈ U ∧ D ∈ V ∧ W ∈ S X O Y T → X ∈ A ∧ Y ∈ B ∧ S ∈ ⦋ X / x⦌ ⦋ Y / y⦌ C ∧ T ∈ ⦋ X / x⦌ ⦋ Y / y⦌ D
86 85 ex ⊢ X ∈ A ∧ Y ∈ B → ∀ x ∈ A ∀ y ∈ B C ∈ U ∧ D ∈ V ∧ W ∈ S X O Y T → X ∈ A ∧ Y ∈ B ∧ S ∈ ⦋ X / x⦌ ⦋ Y / y⦌ C ∧ T ∈ ⦋ X / x⦌ ⦋ Y / y⦌ D
87 1 mpondm0 ⊢ ¬ X ∈ A ∧ Y ∈ B → X O Y = ∅
88 87 oveqd ⊢ ¬ X ∈ A ∧ Y ∈ B → S X O Y T = S ∅ T
89 88 eleq2d ⊢ ¬ X ∈ A ∧ Y ∈ B → W ∈ S X O Y T ↔ W ∈ S ∅ T
90 noel ⊢ ¬ W ∈ ∅
91 90 pm2.21i ⊢ W ∈ ∅ → X ∈ A ∧ Y ∈ B ∧ S ∈ ⦋ X / x⦌ ⦋ Y / y⦌ C ∧ T ∈ ⦋ X / x⦌ ⦋ Y / y⦌ D
92 0ov ⊢ S ∅ T = ∅
93 91 92 eleq2s ⊢ W ∈ S ∅ T → X ∈ A ∧ Y ∈ B ∧ S ∈ ⦋ X / x⦌ ⦋ Y / y⦌ C ∧ T ∈ ⦋ X / x⦌ ⦋ Y / y⦌ D
94 89 93 syl6bi ⊢ ¬ X ∈ A ∧ Y ∈ B → W ∈ S X O Y T → X ∈ A ∧ Y ∈ B ∧ S ∈ ⦋ X / x⦌ ⦋ Y / y⦌ C ∧ T ∈ ⦋ X / x⦌ ⦋ Y / y⦌ D
95 94 adantld ⊢ ¬ X ∈ A ∧ Y ∈ B → ∀ x ∈ A ∀ y ∈ B C ∈ U ∧ D ∈ V ∧ W ∈ S X O Y T → X ∈ A ∧ Y ∈ B ∧ S ∈ ⦋ X / x⦌ ⦋ Y / y⦌ C ∧ T ∈ ⦋ X / x⦌ ⦋ Y / y⦌ D
96 86 95 pm2.61i ⊢ ∀ x ∈ A ∀ y ∈ B C ∈ U ∧ D ∈ V ∧ W ∈ S X O Y T → X ∈ A ∧ Y ∈ B ∧ S ∈ ⦋ X / x⦌ ⦋ Y / y⦌ C ∧ T ∈ ⦋ X / x⦌ ⦋ Y / y⦌ D
97 96 ex ⊢ ∀ x ∈ A ∀ y ∈ B C ∈ U ∧ D ∈ V → W ∈ S X O Y T → X ∈ A ∧ Y ∈ B ∧ S ∈ ⦋ X / x⦌ ⦋ Y / y⦌ C ∧ T ∈ ⦋ X / x⦌ ⦋ Y / y⦌ D