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 ⊢ 𝑂 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ ( 𝑠 ∈ 𝐶 , 𝑡 ∈ 𝐷 ↦ 𝐸 ) )
el2mpocl.e ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( 𝐶 = 𝐹 ∧ 𝐷 = 𝐺 ) )
Assertion el2mpocl ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝐶 ∈ 𝑈 ∧ 𝐷 ∈ 𝑉 ) → ( 𝑊 ∈ ( 𝑆 ( 𝑋 𝑂 𝑌 ) 𝑇 ) → ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑆 ∈ 𝐹 ∧ 𝑇 ∈ 𝐺 ) ) ) )

Proof

Step Hyp Ref Expression
1 el2mpocl.o ⊢ 𝑂 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ ( 𝑠 ∈ 𝐶 , 𝑡 ∈ 𝐷 ↦ 𝐸 ) )
2 el2mpocl.e ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( 𝐶 = 𝐹 ∧ 𝐷 = 𝐺 ) )
3 1 el2mpocsbcl ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝐶 ∈ 𝑈 ∧ 𝐷 ∈ 𝑉 ) → ( 𝑊 ∈ ( 𝑆 ( 𝑋 𝑂 𝑌 ) 𝑇 ) → ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑆 ∈ ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐶 ∧ 𝑇 ∈ ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐷 ) ) ) )
4 simpl ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ∈ 𝐴 )
5 simplr ⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑥 = 𝑋 ) → 𝑌 ∈ 𝐵 )
6 2 simpld ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → 𝐶 = 𝐹 )
7 6 adantll ⊢ ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) → 𝐶 = 𝐹 )
8 5 7 csbied ⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑥 = 𝑋 ) → ⦋ 𝑌 / 𝑦 ⦌ 𝐶 = 𝐹 )
9 4 8 csbied ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐶 = 𝐹 )
10 9 eleq2d ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑆 ∈ ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐶 ↔ 𝑆 ∈ 𝐹 ) )
11 2 simprd ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → 𝐷 = 𝐺 )
12 11 adantll ⊢ ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) → 𝐷 = 𝐺 )
13 5 12 csbied ⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑥 = 𝑋 ) → ⦋ 𝑌 / 𝑦 ⦌ 𝐷 = 𝐺 )
14 4 13 csbied ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐷 = 𝐺 )
15 14 eleq2d ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑇 ∈ ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐷 ↔ 𝑇 ∈ 𝐺 ) )
16 10 15 anbi12d ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑆 ∈ ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐶 ∧ 𝑇 ∈ ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐷 ) ↔ ( 𝑆 ∈ 𝐹 ∧ 𝑇 ∈ 𝐺 ) ) )
17 16 biimpd ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑆 ∈ ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐶 ∧ 𝑇 ∈ ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐷 ) → ( 𝑆 ∈ 𝐹 ∧ 𝑇 ∈ 𝐺 ) ) )
18 17 imdistani ⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑆 ∈ ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐶 ∧ 𝑇 ∈ ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐷 ) ) → ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑆 ∈ 𝐹 ∧ 𝑇 ∈ 𝐺 ) ) )
19 3 18 syl6 ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝐶 ∈ 𝑈 ∧ 𝐷 ∈ 𝑉 ) → ( 𝑊 ∈ ( 𝑆 ( 𝑋 𝑂 𝑌 ) 𝑇 ) → ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑆 ∈ 𝐹 ∧ 𝑇 ∈ 𝐺 ) ) ) )