Metamath Proof Explorer

Theorem el2mpocl

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. Using implicit substitution. (Contributed by AV, 21-May-2021)

Ref Expression
Hypotheses el2mpocl.o 
|- O = ( x e. A , y e. B |-> ( s e. C , t e. D |-> E ) )
el2mpocl.e 
|- ( ( x = X /\ y = Y ) -> ( C = F /\ D = G ) )
Assertion el2mpocl 
|- ( 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. F /\ T e. G ) ) ) )

Proof

Step Hyp Ref Expression
1 el2mpocl.o 
 |-  O = ( x e. A , y e. B |-> ( s e. C , t e. D |-> E ) )
2 el2mpocl.e 
 |-  ( ( x = X /\ y = Y ) -> ( C = F /\ D = G ) )
3 1 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 ) ) ) )
4 simpl 
 |-  ( ( X e. A /\ Y e. B ) -> X e. A )
5 simplr 
 |-  ( ( ( X e. A /\ Y e. B ) /\ x = X ) -> Y e. B )
6 2 simpld 
 |-  ( ( x = X /\ y = Y ) -> C = F )
7 6 adantll 
 |-  ( ( ( ( X e. A /\ Y e. B ) /\ x = X ) /\ y = Y ) -> C = F )
8 5 7 csbied 
 |-  ( ( ( X e. A /\ Y e. B ) /\ x = X ) -> [_ Y / y ]_ C = F )
9 4 8 csbied 
 |-  ( ( X e. A /\ Y e. B ) -> [_ X / x ]_ [_ Y / y ]_ C = F )
10 9 eleq2d 
 |-  ( ( X e. A /\ Y e. B ) -> ( S e. [_ X / x ]_ [_ Y / y ]_ C <-> S e. F ) )
11 2 simprd 
 |-  ( ( x = X /\ y = Y ) -> D = G )
12 11 adantll 
 |-  ( ( ( ( X e. A /\ Y e. B ) /\ x = X ) /\ y = Y ) -> D = G )
13 5 12 csbied 
 |-  ( ( ( X e. A /\ Y e. B ) /\ x = X ) -> [_ Y / y ]_ D = G )
14 4 13 csbied 
 |-  ( ( X e. A /\ Y e. B ) -> [_ X / x ]_ [_ Y / y ]_ D = G )
15 14 eleq2d 
 |-  ( ( X e. A /\ Y e. B ) -> ( T e. [_ X / x ]_ [_ Y / y ]_ D <-> T e. G ) )
16 10 15 anbi12d 
 |-  ( ( X e. A /\ Y e. B ) -> ( ( S e. [_ X / x ]_ [_ Y / y ]_ C /\ T e. [_ X / x ]_ [_ Y / y ]_ D ) <-> ( S e. F /\ T e. G ) ) )
17 16 biimpd 
 |-  ( ( X e. A /\ Y e. B ) -> ( ( S e. [_ X / x ]_ [_ Y / y ]_ C /\ T e. [_ X / x ]_ [_ Y / y ]_ D ) -> ( S e. F /\ T e. G ) ) )
18 17 imdistani 
 |-  ( ( ( X e. A /\ Y e. B ) /\ ( S e. [_ X / x ]_ [_ Y / y ]_ C /\ T e. [_ X / x ]_ [_ Y / y ]_ D ) ) -> ( ( X e. A /\ Y e. B ) /\ ( S e. F /\ T e. G ) ) )
19 3 18 syl6 
 |-  ( 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. F /\ T e. G ) ) ) )