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∈BC∈U∧D∈V→W∈SXOYT→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∈BC∈U∧D∈V∧W∈SXOYT→X∈A∧Y∈B
3 nfcv ⊢Ⅎ_as∈C,t∈D⟼E
4 nfcv ⊢Ⅎ_bs∈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 ⊢Ⅎ_xs∈⦋a/x⦌⦋b/y⦌C,t∈⦋a/x⦌⦋b/y⦌D⟼⦋a/x⦌⦋b/y⦌E
9 nfcv ⊢Ⅎ_ya
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 ⊢Ⅎ_ys∈⦋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∈BC∈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∈BC∈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∈BC∈U∧D∈V∧X∈A∧Y∈B→X∈A
55 simpr ⊢X∈A∧Y∈B→Y∈B
56 55 adantl ⊢∀x∈A∀y∈BC∈U∧D∈V∧X∈A∧Y∈B→Y∈B
57 simpl ⊢C∈U∧D∈V→C∈U
58 57 ralimi ⊢∀y∈BC∈U∧D∈V→∀y∈BC∈U
59 rspcsbela ⊢Y∈B∧∀y∈BC∈U→⦋Y/y⦌C∈U
60 55 58 59 syl2an ⊢X∈A∧Y∈B∧∀y∈BC∈U∧D∈V→⦋Y/y⦌C∈U
61 60 ex ⊢X∈A∧Y∈B→∀y∈BC∈U∧D∈V→⦋Y/y⦌C∈U
62 61 ralimdv ⊢X∈A∧Y∈B→∀x∈A∀y∈BC∈U∧D∈V→∀x∈A⦋Y/y⦌C∈U
63 62 impcom ⊢∀x∈A∀y∈BC∈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∈BC∈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∈BC∈U∧D∈V→∀y∈BD∈V
68 rspcsbela ⊢Y∈B∧∀y∈BD∈V→⦋Y/y⦌D∈V
69 55 67 68 syl2an ⊢X∈A∧Y∈B∧∀y∈BC∈U∧D∈V→⦋Y/y⦌D∈V
70 69 ex ⊢X∈A∧Y∈B→∀y∈BC∈U∧D∈V→⦋Y/y⦌D∈V
71 70 ralimdv ⊢X∈A∧Y∈B→∀x∈A∀y∈BC∈U∧D∈V→∀x∈A⦋Y/y⦌D∈V
72 71 impcom ⊢∀x∈A∀y∈BC∈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∈BC∈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∈BC∈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∈BC∈U∧D∈V∧X∈A∧Y∈B→XOY=s∈⦋X/x⦌⦋Y/y⦌C,t∈⦋X/x⦌⦋Y/y⦌D⟼⦋X/x⦌⦋Y/y⦌E
78 77 oveqd ⊢∀x∈A∀y∈BC∈U∧D∈V∧X∈A∧Y∈B→SXOYT=Ss∈⦋X/x⦌⦋Y/y⦌C,t∈⦋X/x⦌⦋Y/y⦌D⟼⦋X/x⦌⦋Y/y⦌ET
79 78 eleq2d ⊢∀x∈A∀y∈BC∈U∧D∈V∧X∈A∧Y∈B→W∈SXOYT↔W∈Ss∈⦋X/x⦌⦋Y/y⦌C,t∈⦋X/x⦌⦋Y/y⦌D⟼⦋X/x⦌⦋Y/y⦌ET
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∈Ss∈⦋X/x⦌⦋Y/y⦌C,t∈⦋X/x⦌⦋Y/y⦌D⟼⦋X/x⦌⦋Y/y⦌ET→S∈⦋X/x⦌⦋Y/y⦌C∧T∈⦋X/x⦌⦋Y/y⦌D
82 79 81 syl6bi ⊢∀x∈A∀y∈BC∈U∧D∈V∧X∈A∧Y∈B→W∈SXOYT→S∈⦋X/x⦌⦋Y/y⦌C∧T∈⦋X/x⦌⦋Y/y⦌D
83 82 impancom ⊢∀x∈A∀y∈BC∈U∧D∈V∧W∈SXOYT→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∈BC∈U∧D∈V∧W∈SXOYT→S∈⦋X/x⦌⦋Y/y⦌C∧T∈⦋X/x⦌⦋Y/y⦌D
85 2 84 jca ⊢X∈A∧Y∈B∧∀x∈A∀y∈BC∈U∧D∈V∧W∈SXOYT→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∈BC∈U∧D∈V∧W∈SXOYT→X∈A∧Y∈B∧S∈⦋X/x⦌⦋Y/y⦌C∧T∈⦋X/x⦌⦋Y/y⦌D
87 1 mpondm0 ⊢¬X∈A∧Y∈B→XOY=∅
88 87 oveqd ⊢¬X∈A∧Y∈B→SXOYT=S∅T
89 88 eleq2d ⊢¬X∈A∧Y∈B→W∈SXOYT↔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∈SXOYT→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∈BC∈U∧D∈V∧W∈SXOYT→X∈A∧Y∈B∧S∈⦋X/x⦌⦋Y/y⦌C∧T∈⦋X/x⦌⦋Y/y⦌D
96 86 95 pm2.61i ⊢∀x∈A∀y∈BC∈U∧D∈V∧W∈SXOYT→X∈A∧Y∈B∧S∈⦋X/x⦌⦋Y/y⦌C∧T∈⦋X/x⦌⦋Y/y⦌D
97 96 ex ⊢∀x∈A∀y∈BC∈U∧D∈V→W∈SXOYT→X∈A∧Y∈B∧S∈⦋X/x⦌⦋Y/y⦌C∧T∈⦋X/x⦌⦋Y/y⦌D