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 e. A , y e. B |-> ( s e. C , t e. D |-> E ) )
Assertion el2mpocsbcl 
|- ( A. x e. A A. y e. B ( C e. U /\ D e. V ) -> ( W e. ( S ( X O Y ) T ) -> ( ( X e. A /\ Y e. B ) /\ ( S e. [_ X / x ]_ [_ Y / y ]_ C /\ T e. [_ X / x ]_ [_ Y / y ]_ D ) ) ) )

Proof

Step Hyp Ref Expression
1 el2mpocsbcl.o 
 |-  O = ( x e. A , y e. B |-> ( s e. C , t e. D |-> E ) )
2 simpl 
 |-  ( ( ( X e. A /\ Y e. B ) /\ ( A. x e. A A. y e. B ( C e. U /\ D e. V ) /\ W e. ( S ( X O Y ) T ) ) ) -> ( X e. A /\ Y e. B ) )
3 nfcv 
 |-  F/_ a ( s e. C , t e. D |-> E )
4 nfcv 
 |-  F/_ b ( s e. C , t e. D |-> E )
5 nfcsb1v 
 |-  F/_ x [_ a / x ]_ [_ b / y ]_ C
6 nfcsb1v 
 |-  F/_ x [_ a / x ]_ [_ b / y ]_ D
7 nfcsb1v 
 |-  F/_ x [_ a / x ]_ [_ b / y ]_ E
8 5 6 7 nfmpo 
 |-  F/_ x ( s e. [_ a / x ]_ [_ b / y ]_ C , t e. [_ a / x ]_ [_ b / y ]_ D |-> [_ a / x ]_ [_ b / y ]_ E )
9 nfcv 
 |-  F/_ y a
10 nfcsb1v 
 |-  F/_ y [_ b / y ]_ C
11 9 10 nfcsbw 
 |-  F/_ y [_ a / x ]_ [_ b / y ]_ C
12 nfcsb1v 
 |-  F/_ y [_ b / y ]_ D
13 9 12 nfcsbw 
 |-  F/_ y [_ a / x ]_ [_ b / y ]_ D
14 nfcsb1v 
 |-  F/_ y [_ b / y ]_ E
15 9 14 nfcsbw 
 |-  F/_ y [_ a / x ]_ [_ b / y ]_ E
16 11 13 15 nfmpo 
 |-  F/_ y ( s e. [_ a / x ]_ [_ b / y ]_ C , t e. [_ 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 e. C , t e. D |-> E ) = ( s e. [_ a / x ]_ [_ b / y ]_ C , t e. [_ a / x ]_ [_ b / y ]_ D |-> [_ a / x ]_ [_ b / y ]_ E ) )
30 3 4 8 16 29 cbvmpo 
 |-  ( x e. A , y e. B |-> ( s e. C , t e. D |-> E ) ) = ( a e. A , b e. B |-> ( s e. [_ a / x ]_ [_ b / y ]_ C , t e. [_ a / x ]_ [_ b / y ]_ D |-> [_ a / x ]_ [_ b / y ]_ E ) )
31 1 30 eqtri 
 |-  O = ( a e. A , b e. B |-> ( s e. [_ a / x ]_ [_ b / y ]_ C , t e. [_ a / x ]_ [_ b / y ]_ D |-> [_ a / x ]_ [_ b / y ]_ E ) )
32 31 a1i 
 |-  ( ( A. x e. A A. y e. B ( C e. U /\ D e. V ) /\ ( X e. A /\ Y e. B ) ) -> O = ( a e. A , b e. B |-> ( s e. [_ a / x ]_ [_ b / y ]_ C , t e. [_ 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 e. [_ a / x ]_ [_ b / y ]_ C , t e. [_ a / x ]_ [_ b / y ]_ D |-> [_ a / x ]_ [_ b / y ]_ E ) = ( s e. [_ X / x ]_ [_ Y / y ]_ C , t e. [_ X / x ]_ [_ Y / y ]_ D |-> [_ X / x ]_ [_ Y / y ]_ E ) )
52 51 adantl 
 |-  ( ( ( A. x e. A A. y e. B ( C e. U /\ D e. V ) /\ ( X e. A /\ Y e. B ) ) /\ ( a = X /\ b = Y ) ) -> ( s e. [_ a / x ]_ [_ b / y ]_ C , t e. [_ a / x ]_ [_ b / y ]_ D |-> [_ a / x ]_ [_ b / y ]_ E ) = ( s e. [_ X / x ]_ [_ Y / y ]_ C , t e. [_ X / x ]_ [_ Y / y ]_ D |-> [_ X / x ]_ [_ Y / y ]_ E ) )
53 simpl 
 |-  ( ( X e. A /\ Y e. B ) -> X e. A )
54 53 adantl 
 |-  ( ( A. x e. A A. y e. B ( C e. U /\ D e. V ) /\ ( X e. A /\ Y e. B ) ) -> X e. A )
55 simpr 
 |-  ( ( X e. A /\ Y e. B ) -> Y e. B )
56 55 adantl 
 |-  ( ( A. x e. A A. y e. B ( C e. U /\ D e. V ) /\ ( X e. A /\ Y e. B ) ) -> Y e. B )
57 simpl 
 |-  ( ( C e. U /\ D e. V ) -> C e. U )
58 57 ralimi 
 |-  ( A. y e. B ( C e. U /\ D e. V ) -> A. y e. B C e. U )
59 rspcsbela 
 |-  ( ( Y e. B /\ A. y e. B C e. U ) -> [_ Y / y ]_ C e. U )
60 55 58 59 syl2an 
 |-  ( ( ( X e. A /\ Y e. B ) /\ A. y e. B ( C e. U /\ D e. V ) ) -> [_ Y / y ]_ C e. U )
61 60 ex 
 |-  ( ( X e. A /\ Y e. B ) -> ( A. y e. B ( C e. U /\ D e. V ) -> [_ Y / y ]_ C e. U ) )
62 61 ralimdv 
 |-  ( ( X e. A /\ Y e. B ) -> ( A. x e. A A. y e. B ( C e. U /\ D e. V ) -> A. x e. A [_ Y / y ]_ C e. U ) )
63 62 impcom 
 |-  ( ( A. x e. A A. y e. B ( C e. U /\ D e. V ) /\ ( X e. A /\ Y e. B ) ) -> A. x e. A [_ Y / y ]_ C e. U )
64 rspcsbela 
 |-  ( ( X e. A /\ A. x e. A [_ Y / y ]_ C e. U ) -> [_ X / x ]_ [_ Y / y ]_ C e. U )
65 54 63 64 syl2anc 
 |-  ( ( A. x e. A A. y e. B ( C e. U /\ D e. V ) /\ ( X e. A /\ Y e. B ) ) -> [_ X / x ]_ [_ Y / y ]_ C e. U )
66 simpr 
 |-  ( ( C e. U /\ D e. V ) -> D e. V )
67 66 ralimi 
 |-  ( A. y e. B ( C e. U /\ D e. V ) -> A. y e. B D e. V )
68 rspcsbela 
 |-  ( ( Y e. B /\ A. y e. B D e. V ) -> [_ Y / y ]_ D e. V )
69 55 67 68 syl2an 
 |-  ( ( ( X e. A /\ Y e. B ) /\ A. y e. B ( C e. U /\ D e. V ) ) -> [_ Y / y ]_ D e. V )
70 69 ex 
 |-  ( ( X e. A /\ Y e. B ) -> ( A. y e. B ( C e. U /\ D e. V ) -> [_ Y / y ]_ D e. V ) )
71 70 ralimdv 
 |-  ( ( X e. A /\ Y e. B ) -> ( A. x e. A A. y e. B ( C e. U /\ D e. V ) -> A. x e. A [_ Y / y ]_ D e. V ) )
72 71 impcom 
 |-  ( ( A. x e. A A. y e. B ( C e. U /\ D e. V ) /\ ( X e. A /\ Y e. B ) ) -> A. x e. A [_ Y / y ]_ D e. V )
73 rspcsbela 
 |-  ( ( X e. A /\ A. x e. A [_ Y / y ]_ D e. V ) -> [_ X / x ]_ [_ Y / y ]_ D e. V )
74 54 72 73 syl2anc 
 |-  ( ( A. x e. A A. y e. B ( C e. U /\ D e. V ) /\ ( X e. A /\ Y e. B ) ) -> [_ X / x ]_ [_ Y / y ]_ D e. V )
75 mpoexga 
 |-  ( ( [_ X / x ]_ [_ Y / y ]_ C e. U /\ [_ X / x ]_ [_ Y / y ]_ D e. V ) -> ( s e. [_ X / x ]_ [_ Y / y ]_ C , t e. [_ X / x ]_ [_ Y / y ]_ D |-> [_ X / x ]_ [_ Y / y ]_ E ) e. _V )
76 65 74 75 syl2anc 
 |-  ( ( A. x e. A A. y e. B ( C e. U /\ D e. V ) /\ ( X e. A /\ Y e. B ) ) -> ( s e. [_ X / x ]_ [_ Y / y ]_ C , t e. [_ X / x ]_ [_ Y / y ]_ D |-> [_ X / x ]_ [_ Y / y ]_ E ) e. _V )
77 32 52 54 56 76 ovmpod 
 |-  ( ( A. x e. A A. y e. B ( C e. U /\ D e. V ) /\ ( X e. A /\ Y e. B ) ) -> ( X O Y ) = ( s e. [_ X / x ]_ [_ Y / y ]_ C , t e. [_ X / x ]_ [_ Y / y ]_ D |-> [_ X / x ]_ [_ Y / y ]_ E ) )
78 77 oveqd 
 |-  ( ( A. x e. A A. y e. B ( C e. U /\ D e. V ) /\ ( X e. A /\ Y e. B ) ) -> ( S ( X O Y ) T ) = ( S ( s e. [_ X / x ]_ [_ Y / y ]_ C , t e. [_ X / x ]_ [_ Y / y ]_ D |-> [_ X / x ]_ [_ Y / y ]_ E ) T ) )
79 78 eleq2d 
 |-  ( ( A. x e. A A. y e. B ( C e. U /\ D e. V ) /\ ( X e. A /\ Y e. B ) ) -> ( W e. ( S ( X O Y ) T ) <-> W e. ( S ( s e. [_ X / x ]_ [_ Y / y ]_ C , t e. [_ X / x ]_ [_ Y / y ]_ D |-> [_ X / x ]_ [_ Y / y ]_ E ) T ) ) )
80 eqid 
 |-  ( s e. [_ X / x ]_ [_ Y / y ]_ C , t e. [_ X / x ]_ [_ Y / y ]_ D |-> [_ X / x ]_ [_ Y / y ]_ E ) = ( s e. [_ X / x ]_ [_ Y / y ]_ C , t e. [_ X / x ]_ [_ Y / y ]_ D |-> [_ X / x ]_ [_ Y / y ]_ E )
81 80 elmpocl 
 |-  ( W e. ( S ( s e. [_ X / x ]_ [_ Y / y ]_ C , t e. [_ X / x ]_ [_ Y / y ]_ D |-> [_ X / x ]_ [_ Y / y ]_ E ) T ) -> ( S e. [_ X / x ]_ [_ Y / y ]_ C /\ T e. [_ X / x ]_ [_ Y / y ]_ D ) )
82 79 81 syl6bi 
 |-  ( ( A. x e. A A. y e. B ( C e. U /\ D e. V ) /\ ( X e. A /\ Y e. B ) ) -> ( W e. ( S ( X O Y ) T ) -> ( S e. [_ X / x ]_ [_ Y / y ]_ C /\ T e. [_ X / x ]_ [_ Y / y ]_ D ) ) )
83 82 impancom 
 |-  ( ( A. x e. A A. y e. B ( C e. U /\ D e. V ) /\ W e. ( S ( X O Y ) T ) ) -> ( ( X e. A /\ Y e. B ) -> ( S e. [_ X / x ]_ [_ Y / y ]_ C /\ T e. [_ X / x ]_ [_ Y / y ]_ D ) ) )
84 83 impcom 
 |-  ( ( ( X e. A /\ Y e. B ) /\ ( A. x e. A A. y e. B ( C e. U /\ D e. V ) /\ W e. ( S ( X O Y ) T ) ) ) -> ( S e. [_ X / x ]_ [_ Y / y ]_ C /\ T e. [_ X / x ]_ [_ Y / y ]_ D ) )
85 2 84 jca 
 |-  ( ( ( X e. A /\ Y e. B ) /\ ( A. x e. A A. y e. B ( C e. U /\ D e. V ) /\ W e. ( S ( X O Y ) T ) ) ) -> ( ( X e. A /\ Y e. B ) /\ ( S e. [_ X / x ]_ [_ Y / y ]_ C /\ T e. [_ X / x ]_ [_ Y / y ]_ D ) ) )
86 85 ex 
 |-  ( ( X e. A /\ Y e. B ) -> ( ( A. x e. A A. y e. B ( C e. U /\ D e. V ) /\ W e. ( S ( X O Y ) T ) ) -> ( ( X e. A /\ Y e. B ) /\ ( S e. [_ X / x ]_ [_ Y / y ]_ C /\ T e. [_ X / x ]_ [_ Y / y ]_ D ) ) ) )
87 1 mpondm0 
 |-  ( -. ( X e. A /\ Y e. B ) -> ( X O Y ) = (/) )
88 87 oveqd 
 |-  ( -. ( X e. A /\ Y e. B ) -> ( S ( X O Y ) T ) = ( S (/) T ) )
89 88 eleq2d 
 |-  ( -. ( X e. A /\ Y e. B ) -> ( W e. ( S ( X O Y ) T ) <-> W e. ( S (/) T ) ) )
90 noel 
 |-  -. W e. (/)
91 90 pm2.21i 
 |-  ( W e. (/) -> ( ( X e. A /\ Y e. B ) /\ ( S e. [_ X / x ]_ [_ Y / y ]_ C /\ T e. [_ X / x ]_ [_ Y / y ]_ D ) ) )
92 0ov 
 |-  ( S (/) T ) = (/)
93 91 92 eleq2s 
 |-  ( W e. ( S (/) T ) -> ( ( X e. A /\ Y e. B ) /\ ( S e. [_ X / x ]_ [_ Y / y ]_ C /\ T e. [_ X / x ]_ [_ Y / y ]_ D ) ) )
94 89 93 syl6bi 
 |-  ( -. ( X e. A /\ Y e. B ) -> ( W e. ( S ( X O Y ) T ) -> ( ( X e. A /\ Y e. B ) /\ ( S e. [_ X / x ]_ [_ Y / y ]_ C /\ T e. [_ X / x ]_ [_ Y / y ]_ D ) ) ) )
95 94 adantld 
 |-  ( -. ( X e. A /\ Y e. B ) -> ( ( A. x e. A A. y e. B ( C e. U /\ D e. V ) /\ W e. ( S ( X O Y ) T ) ) -> ( ( X e. A /\ Y e. B ) /\ ( S e. [_ X / x ]_ [_ Y / y ]_ C /\ T e. [_ X / x ]_ [_ Y / y ]_ D ) ) ) )
96 86 95 pm2.61i 
 |-  ( ( A. x e. A A. y e. B ( C e. U /\ D e. V ) /\ W e. ( S ( X O Y ) T ) ) -> ( ( X e. A /\ Y e. B ) /\ ( S e. [_ X / x ]_ [_ Y / y ]_ C /\ T e. [_ X / x ]_ [_ Y / y ]_ D ) ) )
97 96 ex 
 |-  ( A. x e. A A. y e. B ( C e. U /\ D e. V ) -> ( W e. ( S ( X O Y ) T ) -> ( ( X e. A /\ Y e. B ) /\ ( S e. [_ X / x ]_ [_ Y / y ]_ C /\ T e. [_ X / x ]_ [_ Y / y ]_ D ) ) ) )