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

Proof

Step Hyp Ref Expression
1 el2mpocsbcl.o ⊢ 𝑂 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ ( 𝑠 ∈ 𝐶 , 𝑡 ∈ 𝐷 ↦ 𝐸 ) )
2 simpl ⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝐶 ∈ 𝑈 ∧ 𝐷 ∈ 𝑉 ) ∧ 𝑊 ∈ ( 𝑆 ( 𝑋 𝑂 𝑌 ) 𝑇 ) ) ) → ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) )
3 nfcv ⊢ Ⅎ 𝑎 ( 𝑠 ∈ 𝐶 , 𝑡 ∈ 𝐷 ↦ 𝐸 )
4 nfcv ⊢ Ⅎ 𝑏 ( 𝑠 ∈ 𝐶 , 𝑡 ∈ 𝐷 ↦ 𝐸 )
5 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑎 / 𝑥 ⦌ ⦋ 𝑏 / 𝑦 ⦌ 𝐶
6 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑎 / 𝑥 ⦌ ⦋ 𝑏 / 𝑦 ⦌ 𝐷
7 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑎 / 𝑥 ⦌ ⦋ 𝑏 / 𝑦 ⦌ 𝐸
8 5 6 7 nfmpo ⊢ Ⅎ 𝑥 ( 𝑠 ∈ ⦋ 𝑎 / 𝑥 ⦌ ⦋ 𝑏 / 𝑦 ⦌ 𝐶 , 𝑡 ∈ ⦋ 𝑎 / 𝑥 ⦌ ⦋ 𝑏 / 𝑦 ⦌ 𝐷 ↦ ⦋ 𝑎 / 𝑥 ⦌ ⦋ 𝑏 / 𝑦 ⦌ 𝐸 )
9 nfcv ⊢ Ⅎ 𝑦 𝑎
10 nfcsb1v ⊢ Ⅎ 𝑦 ⦋ 𝑏 / 𝑦 ⦌ 𝐶
11 9 10 nfcsbw ⊢ Ⅎ 𝑦 ⦋ 𝑎 / 𝑥 ⦌ ⦋ 𝑏 / 𝑦 ⦌ 𝐶
12 nfcsb1v ⊢ Ⅎ 𝑦 ⦋ 𝑏 / 𝑦 ⦌ 𝐷
13 9 12 nfcsbw ⊢ Ⅎ 𝑦 ⦋ 𝑎 / 𝑥 ⦌ ⦋ 𝑏 / 𝑦 ⦌ 𝐷
14 nfcsb1v ⊢ Ⅎ 𝑦 ⦋ 𝑏 / 𝑦 ⦌ 𝐸
15 9 14 nfcsbw ⊢ Ⅎ 𝑦 ⦋ 𝑎 / 𝑥 ⦌ ⦋ 𝑏 / 𝑦 ⦌ 𝐸
16 11 13 15 nfmpo ⊢ Ⅎ 𝑦 ( 𝑠 ∈ ⦋ 𝑎 / 𝑥 ⦌ ⦋ 𝑏 / 𝑦 ⦌ 𝐶 , 𝑡 ∈ ⦋ 𝑎 / 𝑥 ⦌ ⦋ 𝑏 / 𝑦 ⦌ 𝐷 ↦ ⦋ 𝑎 / 𝑥 ⦌ ⦋ 𝑏 / 𝑦 ⦌ 𝐸 )
17 csbeq1a ⊢ ( 𝑥 = 𝑎 → 𝐶 = ⦋ 𝑎 / 𝑥 ⦌ 𝐶 )
18 csbeq1a ⊢ ( 𝑦 = 𝑏 → 𝐶 = ⦋ 𝑏 / 𝑦 ⦌ 𝐶 )
19 18 csbeq2dv ⊢ ( 𝑦 = 𝑏 → ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝑎 / 𝑥 ⦌ ⦋ 𝑏 / 𝑦 ⦌ 𝐶 )
20 17 19 sylan9eq ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → 𝐶 = ⦋ 𝑎 / 𝑥 ⦌ ⦋ 𝑏 / 𝑦 ⦌ 𝐶 )
21 csbeq1a ⊢ ( 𝑥 = 𝑎 → 𝐷 = ⦋ 𝑎 / 𝑥 ⦌ 𝐷 )
22 csbeq1a ⊢ ( 𝑦 = 𝑏 → 𝐷 = ⦋ 𝑏 / 𝑦 ⦌ 𝐷 )
23 22 csbeq2dv ⊢ ( 𝑦 = 𝑏 → ⦋ 𝑎 / 𝑥 ⦌ 𝐷 = ⦋ 𝑎 / 𝑥 ⦌ ⦋ 𝑏 / 𝑦 ⦌ 𝐷 )
24 21 23 sylan9eq ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → 𝐷 = ⦋ 𝑎 / 𝑥 ⦌ ⦋ 𝑏 / 𝑦 ⦌ 𝐷 )
25 csbeq1a ⊢ ( 𝑥 = 𝑎 → 𝐸 = ⦋ 𝑎 / 𝑥 ⦌ 𝐸 )
26 csbeq1a ⊢ ( 𝑦 = 𝑏 → 𝐸 = ⦋ 𝑏 / 𝑦 ⦌ 𝐸 )
27 26 csbeq2dv ⊢ ( 𝑦 = 𝑏 → ⦋ 𝑎 / 𝑥 ⦌ 𝐸 = ⦋ 𝑎 / 𝑥 ⦌ ⦋ 𝑏 / 𝑦 ⦌ 𝐸 )
28 25 27 sylan9eq ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → 𝐸 = ⦋ 𝑎 / 𝑥 ⦌ ⦋ 𝑏 / 𝑦 ⦌ 𝐸 )
29 20 24 28 mpoeq123dv ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → ( 𝑠 ∈ 𝐶 , 𝑡 ∈ 𝐷 ↦ 𝐸 ) = ( 𝑠 ∈ ⦋ 𝑎 / 𝑥 ⦌ ⦋ 𝑏 / 𝑦 ⦌ 𝐶 , 𝑡 ∈ ⦋ 𝑎 / 𝑥 ⦌ ⦋ 𝑏 / 𝑦 ⦌ 𝐷 ↦ ⦋ 𝑎 / 𝑥 ⦌ ⦋ 𝑏 / 𝑦 ⦌ 𝐸 ) )
30 3 4 8 16 29 cbvmpo ⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ ( 𝑠 ∈ 𝐶 , 𝑡 ∈ 𝐷 ↦ 𝐸 ) ) = ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐵 ↦ ( 𝑠 ∈ ⦋ 𝑎 / 𝑥 ⦌ ⦋ 𝑏 / 𝑦 ⦌ 𝐶 , 𝑡 ∈ ⦋ 𝑎 / 𝑥 ⦌ ⦋ 𝑏 / 𝑦 ⦌ 𝐷 ↦ ⦋ 𝑎 / 𝑥 ⦌ ⦋ 𝑏 / 𝑦 ⦌ 𝐸 ) )
31 1 30 eqtri ⊢ 𝑂 = ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐵 ↦ ( 𝑠 ∈ ⦋ 𝑎 / 𝑥 ⦌ ⦋ 𝑏 / 𝑦 ⦌ 𝐶 , 𝑡 ∈ ⦋ 𝑎 / 𝑥 ⦌ ⦋ 𝑏 / 𝑦 ⦌ 𝐷 ↦ ⦋ 𝑎 / 𝑥 ⦌ ⦋ 𝑏 / 𝑦 ⦌ 𝐸 ) )
32 31 a1i ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝐶 ∈ 𝑈 ∧ 𝐷 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑂 = ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐵 ↦ ( 𝑠 ∈ ⦋ 𝑎 / 𝑥 ⦌ ⦋ 𝑏 / 𝑦 ⦌ 𝐶 , 𝑡 ∈ ⦋ 𝑎 / 𝑥 ⦌ ⦋ 𝑏 / 𝑦 ⦌ 𝐷 ↦ ⦋ 𝑎 / 𝑥 ⦌ ⦋ 𝑏 / 𝑦 ⦌ 𝐸 ) ) )
33 csbeq1 ⊢ ( 𝑎 = 𝑋 → ⦋ 𝑎 / 𝑥 ⦌ ⦋ 𝑏 / 𝑦 ⦌ 𝐶 = ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑏 / 𝑦 ⦌ 𝐶 )
34 33 adantr ⊢ ( ( 𝑎 = 𝑋 ∧ 𝑏 = 𝑌 ) → ⦋ 𝑎 / 𝑥 ⦌ ⦋ 𝑏 / 𝑦 ⦌ 𝐶 = ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑏 / 𝑦 ⦌ 𝐶 )
35 csbeq1 ⊢ ( 𝑏 = 𝑌 → ⦋ 𝑏 / 𝑦 ⦌ 𝐶 = ⦋ 𝑌 / 𝑦 ⦌ 𝐶 )
36 35 adantl ⊢ ( ( 𝑎 = 𝑋 ∧ 𝑏 = 𝑌 ) → ⦋ 𝑏 / 𝑦 ⦌ 𝐶 = ⦋ 𝑌 / 𝑦 ⦌ 𝐶 )
37 36 csbeq2dv ⊢ ( ( 𝑎 = 𝑋 ∧ 𝑏 = 𝑌 ) → ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑏 / 𝑦 ⦌ 𝐶 = ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐶 )
38 34 37 eqtrd ⊢ ( ( 𝑎 = 𝑋 ∧ 𝑏 = 𝑌 ) → ⦋ 𝑎 / 𝑥 ⦌ ⦋ 𝑏 / 𝑦 ⦌ 𝐶 = ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐶 )
39 csbeq1 ⊢ ( 𝑎 = 𝑋 → ⦋ 𝑎 / 𝑥 ⦌ ⦋ 𝑏 / 𝑦 ⦌ 𝐷 = ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑏 / 𝑦 ⦌ 𝐷 )
40 39 adantr ⊢ ( ( 𝑎 = 𝑋 ∧ 𝑏 = 𝑌 ) → ⦋ 𝑎 / 𝑥 ⦌ ⦋ 𝑏 / 𝑦 ⦌ 𝐷 = ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑏 / 𝑦 ⦌ 𝐷 )
41 csbeq1 ⊢ ( 𝑏 = 𝑌 → ⦋ 𝑏 / 𝑦 ⦌ 𝐷 = ⦋ 𝑌 / 𝑦 ⦌ 𝐷 )
42 41 adantl ⊢ ( ( 𝑎 = 𝑋 ∧ 𝑏 = 𝑌 ) → ⦋ 𝑏 / 𝑦 ⦌ 𝐷 = ⦋ 𝑌 / 𝑦 ⦌ 𝐷 )
43 42 csbeq2dv ⊢ ( ( 𝑎 = 𝑋 ∧ 𝑏 = 𝑌 ) → ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑏 / 𝑦 ⦌ 𝐷 = ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐷 )
44 40 43 eqtrd ⊢ ( ( 𝑎 = 𝑋 ∧ 𝑏 = 𝑌 ) → ⦋ 𝑎 / 𝑥 ⦌ ⦋ 𝑏 / 𝑦 ⦌ 𝐷 = ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐷 )
45 csbeq1 ⊢ ( 𝑎 = 𝑋 → ⦋ 𝑎 / 𝑥 ⦌ ⦋ 𝑏 / 𝑦 ⦌ 𝐸 = ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑏 / 𝑦 ⦌ 𝐸 )
46 45 adantr ⊢ ( ( 𝑎 = 𝑋 ∧ 𝑏 = 𝑌 ) → ⦋ 𝑎 / 𝑥 ⦌ ⦋ 𝑏 / 𝑦 ⦌ 𝐸 = ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑏 / 𝑦 ⦌ 𝐸 )
47 csbeq1 ⊢ ( 𝑏 = 𝑌 → ⦋ 𝑏 / 𝑦 ⦌ 𝐸 = ⦋ 𝑌 / 𝑦 ⦌ 𝐸 )
48 47 adantl ⊢ ( ( 𝑎 = 𝑋 ∧ 𝑏 = 𝑌 ) → ⦋ 𝑏 / 𝑦 ⦌ 𝐸 = ⦋ 𝑌 / 𝑦 ⦌ 𝐸 )
49 48 csbeq2dv ⊢ ( ( 𝑎 = 𝑋 ∧ 𝑏 = 𝑌 ) → ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑏 / 𝑦 ⦌ 𝐸 = ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐸 )
50 46 49 eqtrd ⊢ ( ( 𝑎 = 𝑋 ∧ 𝑏 = 𝑌 ) → ⦋ 𝑎 / 𝑥 ⦌ ⦋ 𝑏 / 𝑦 ⦌ 𝐸 = ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐸 )
51 38 44 50 mpoeq123dv ⊢ ( ( 𝑎 = 𝑋 ∧ 𝑏 = 𝑌 ) → ( 𝑠 ∈ ⦋ 𝑎 / 𝑥 ⦌ ⦋ 𝑏 / 𝑦 ⦌ 𝐶 , 𝑡 ∈ ⦋ 𝑎 / 𝑥 ⦌ ⦋ 𝑏 / 𝑦 ⦌ 𝐷 ↦ ⦋ 𝑎 / 𝑥 ⦌ ⦋ 𝑏 / 𝑦 ⦌ 𝐸 ) = ( 𝑠 ∈ ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐶 , 𝑡 ∈ ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐷 ↦ ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐸 ) )
52 51 adantl ⊢ ( ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝐶 ∈ 𝑈 ∧ 𝐷 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ) ∧ ( 𝑎 = 𝑋 ∧ 𝑏 = 𝑌 ) ) → ( 𝑠 ∈ ⦋ 𝑎 / 𝑥 ⦌ ⦋ 𝑏 / 𝑦 ⦌ 𝐶 , 𝑡 ∈ ⦋ 𝑎 / 𝑥 ⦌ ⦋ 𝑏 / 𝑦 ⦌ 𝐷 ↦ ⦋ 𝑎 / 𝑥 ⦌ ⦋ 𝑏 / 𝑦 ⦌ 𝐸 ) = ( 𝑠 ∈ ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐶 , 𝑡 ∈ ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐷 ↦ ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐸 ) )
53 simpl ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ∈ 𝐴 )
54 53 adantl ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝐶 ∈ 𝑈 ∧ 𝐷 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑋 ∈ 𝐴 )
55 simpr ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → 𝑌 ∈ 𝐵 )
56 55 adantl ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝐶 ∈ 𝑈 ∧ 𝐷 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑌 ∈ 𝐵 )
57 simpl ⊢ ( ( 𝐶 ∈ 𝑈 ∧ 𝐷 ∈ 𝑉 ) → 𝐶 ∈ 𝑈 )
58 57 ralimi ⊢ ( ∀ 𝑦 ∈ 𝐵 ( 𝐶 ∈ 𝑈 ∧ 𝐷 ∈ 𝑉 ) → ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝑈 )
59 rspcsbela ⊢ ( ( 𝑌 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝑈 ) → ⦋ 𝑌 / 𝑦 ⦌ 𝐶 ∈ 𝑈 )
60 55 58 59 syl2an ⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐶 ∈ 𝑈 ∧ 𝐷 ∈ 𝑉 ) ) → ⦋ 𝑌 / 𝑦 ⦌ 𝐶 ∈ 𝑈 )
61 60 ex ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → ( ∀ 𝑦 ∈ 𝐵 ( 𝐶 ∈ 𝑈 ∧ 𝐷 ∈ 𝑉 ) → ⦋ 𝑌 / 𝑦 ⦌ 𝐶 ∈ 𝑈 ) )
62 61 ralimdv ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝐶 ∈ 𝑈 ∧ 𝐷 ∈ 𝑉 ) → ∀ 𝑥 ∈ 𝐴 ⦋ 𝑌 / 𝑦 ⦌ 𝐶 ∈ 𝑈 ) )
63 62 impcom ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝐶 ∈ 𝑈 ∧ 𝐷 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ) → ∀ 𝑥 ∈ 𝐴 ⦋ 𝑌 / 𝑦 ⦌ 𝐶 ∈ 𝑈 )
64 rspcsbela ⊢ ( ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ⦋ 𝑌 / 𝑦 ⦌ 𝐶 ∈ 𝑈 ) → ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐶 ∈ 𝑈 )
65 54 63 64 syl2anc ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝐶 ∈ 𝑈 ∧ 𝐷 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ) → ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐶 ∈ 𝑈 )
66 simpr ⊢ ( ( 𝐶 ∈ 𝑈 ∧ 𝐷 ∈ 𝑉 ) → 𝐷 ∈ 𝑉 )
67 66 ralimi ⊢ ( ∀ 𝑦 ∈ 𝐵 ( 𝐶 ∈ 𝑈 ∧ 𝐷 ∈ 𝑉 ) → ∀ 𝑦 ∈ 𝐵 𝐷 ∈ 𝑉 )
68 rspcsbela ⊢ ( ( 𝑌 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 𝐷 ∈ 𝑉 ) → ⦋ 𝑌 / 𝑦 ⦌ 𝐷 ∈ 𝑉 )
69 55 67 68 syl2an ⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐶 ∈ 𝑈 ∧ 𝐷 ∈ 𝑉 ) ) → ⦋ 𝑌 / 𝑦 ⦌ 𝐷 ∈ 𝑉 )
70 69 ex ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → ( ∀ 𝑦 ∈ 𝐵 ( 𝐶 ∈ 𝑈 ∧ 𝐷 ∈ 𝑉 ) → ⦋ 𝑌 / 𝑦 ⦌ 𝐷 ∈ 𝑉 ) )
71 70 ralimdv ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝐶 ∈ 𝑈 ∧ 𝐷 ∈ 𝑉 ) → ∀ 𝑥 ∈ 𝐴 ⦋ 𝑌 / 𝑦 ⦌ 𝐷 ∈ 𝑉 ) )
72 71 impcom ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝐶 ∈ 𝑈 ∧ 𝐷 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ) → ∀ 𝑥 ∈ 𝐴 ⦋ 𝑌 / 𝑦 ⦌ 𝐷 ∈ 𝑉 )
73 rspcsbela ⊢ ( ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ⦋ 𝑌 / 𝑦 ⦌ 𝐷 ∈ 𝑉 ) → ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐷 ∈ 𝑉 )
74 54 72 73 syl2anc ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝐶 ∈ 𝑈 ∧ 𝐷 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ) → ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐷 ∈ 𝑉 )
75 mpoexga ⊢ ( ( ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐶 ∈ 𝑈 ∧ ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐷 ∈ 𝑉 ) → ( 𝑠 ∈ ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐶 , 𝑡 ∈ ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐷 ↦ ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐸 ) ∈ V )
76 65 74 75 syl2anc ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝐶 ∈ 𝑈 ∧ 𝐷 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑠 ∈ ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐶 , 𝑡 ∈ ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐷 ↦ ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐸 ) ∈ V )
77 32 52 54 56 76 ovmpod ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝐶 ∈ 𝑈 ∧ 𝐷 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 𝑂 𝑌 ) = ( 𝑠 ∈ ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐶 , 𝑡 ∈ ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐷 ↦ ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐸 ) )
78 77 oveqd ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝐶 ∈ 𝑈 ∧ 𝐷 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑆 ( 𝑋 𝑂 𝑌 ) 𝑇 ) = ( 𝑆 ( 𝑠 ∈ ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐶 , 𝑡 ∈ ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐷 ↦ ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐸 ) 𝑇 ) )
79 78 eleq2d ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝐶 ∈ 𝑈 ∧ 𝐷 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑊 ∈ ( 𝑆 ( 𝑋 𝑂 𝑌 ) 𝑇 ) ↔ 𝑊 ∈ ( 𝑆 ( 𝑠 ∈ ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐶 , 𝑡 ∈ ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐷 ↦ ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐸 ) 𝑇 ) ) )
80 eqid ⊢ ( 𝑠 ∈ ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐶 , 𝑡 ∈ ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐷 ↦ ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐸 ) = ( 𝑠 ∈ ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐶 , 𝑡 ∈ ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐷 ↦ ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐸 )
81 80 elmpocl ⊢ ( 𝑊 ∈ ( 𝑆 ( 𝑠 ∈ ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐶 , 𝑡 ∈ ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐷 ↦ ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐸 ) 𝑇 ) → ( 𝑆 ∈ ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐶 ∧ 𝑇 ∈ ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐷 ) )
82 79 81 syl6bi ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝐶 ∈ 𝑈 ∧ 𝐷 ∈ 𝑉 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑊 ∈ ( 𝑆 ( 𝑋 𝑂 𝑌 ) 𝑇 ) → ( 𝑆 ∈ ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐶 ∧ 𝑇 ∈ ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐷 ) ) )
83 82 impancom ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝐶 ∈ 𝑈 ∧ 𝐷 ∈ 𝑉 ) ∧ 𝑊 ∈ ( 𝑆 ( 𝑋 𝑂 𝑌 ) 𝑇 ) ) → ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑆 ∈ ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐶 ∧ 𝑇 ∈ ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐷 ) ) )
84 83 impcom ⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝐶 ∈ 𝑈 ∧ 𝐷 ∈ 𝑉 ) ∧ 𝑊 ∈ ( 𝑆 ( 𝑋 𝑂 𝑌 ) 𝑇 ) ) ) → ( 𝑆 ∈ ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐶 ∧ 𝑇 ∈ ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐷 ) )
85 2 84 jca ⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝐶 ∈ 𝑈 ∧ 𝐷 ∈ 𝑉 ) ∧ 𝑊 ∈ ( 𝑆 ( 𝑋 𝑂 𝑌 ) 𝑇 ) ) ) → ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑆 ∈ ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐶 ∧ 𝑇 ∈ ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐷 ) ) )
86 85 ex ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝐶 ∈ 𝑈 ∧ 𝐷 ∈ 𝑉 ) ∧ 𝑊 ∈ ( 𝑆 ( 𝑋 𝑂 𝑌 ) 𝑇 ) ) → ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑆 ∈ ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐶 ∧ 𝑇 ∈ ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐷 ) ) ) )
87 1 mpondm0 ⊢ ( ¬ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 𝑂 𝑌 ) = ∅ )
88 87 oveqd ⊢ ( ¬ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑆 ( 𝑋 𝑂 𝑌 ) 𝑇 ) = ( 𝑆 ∅ 𝑇 ) )
89 88 eleq2d ⊢ ( ¬ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑊 ∈ ( 𝑆 ( 𝑋 𝑂 𝑌 ) 𝑇 ) ↔ 𝑊 ∈ ( 𝑆 ∅ 𝑇 ) ) )
90 noel ⊢ ¬ 𝑊 ∈ ∅
91 90 pm2.21i ⊢ ( 𝑊 ∈ ∅ → ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑆 ∈ ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐶 ∧ 𝑇 ∈ ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐷 ) ) )
92 0ov ⊢ ( 𝑆 ∅ 𝑇 ) = ∅
93 91 92 eleq2s ⊢ ( 𝑊 ∈ ( 𝑆 ∅ 𝑇 ) → ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑆 ∈ ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐶 ∧ 𝑇 ∈ ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐷 ) ) )
94 89 93 syl6bi ⊢ ( ¬ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑊 ∈ ( 𝑆 ( 𝑋 𝑂 𝑌 ) 𝑇 ) → ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑆 ∈ ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐶 ∧ 𝑇 ∈ ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐷 ) ) ) )
95 94 adantld ⊢ ( ¬ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝐶 ∈ 𝑈 ∧ 𝐷 ∈ 𝑉 ) ∧ 𝑊 ∈ ( 𝑆 ( 𝑋 𝑂 𝑌 ) 𝑇 ) ) → ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑆 ∈ ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐶 ∧ 𝑇 ∈ ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐷 ) ) ) )
96 86 95 pm2.61i ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝐶 ∈ 𝑈 ∧ 𝐷 ∈ 𝑉 ) ∧ 𝑊 ∈ ( 𝑆 ( 𝑋 𝑂 𝑌 ) 𝑇 ) ) → ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑆 ∈ ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐶 ∧ 𝑇 ∈ ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐷 ) ) )
97 96 ex ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝐶 ∈ 𝑈 ∧ 𝐷 ∈ 𝑉 ) → ( 𝑊 ∈ ( 𝑆 ( 𝑋 𝑂 𝑌 ) 𝑇 ) → ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑆 ∈ ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐶 ∧ 𝑇 ∈ ⦋ 𝑋 / 𝑥 ⦌ ⦋ 𝑌 / 𝑦 ⦌ 𝐷 ) ) ) )