This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bropfvvvv

Description: If a binary relation holds for the result of an operation which is a function value, the involved classes are sets. (Contributed by AV, 31-Dec-2020) (Revised by AV, 16-Jan-2021)

Ref Expression
Hypotheses bropfvvvv.o ⊢ 𝑂 = ( 𝑎 ∈ 𝑈 ↦ ( 𝑏 ∈ 𝑉 , 𝑐 ∈ 𝑊 ↦ { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜑 } ) )
bropfvvvv.oo ⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) → ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) = { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜃 } )
bropfvvvv.s ⊢ ( 𝑎 = 𝐴 → 𝑉 = 𝑆 )
bropfvvvv.t ⊢ ( 𝑎 = 𝐴 → 𝑊 = 𝑇 )
bropfvvvv.p ⊢ ( 𝑎 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
Assertion bropfvvvv ( ( 𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌 ) → ( 𝐷 ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) 𝐸 → ( 𝐴 ∈ 𝑈 ∧ ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) )

Proof

Step Hyp Ref Expression
1 bropfvvvv.o ⊢ 𝑂 = ( 𝑎 ∈ 𝑈 ↦ ( 𝑏 ∈ 𝑉 , 𝑐 ∈ 𝑊 ↦ { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜑 } ) )
2 bropfvvvv.oo ⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) → ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) = { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜃 } )
3 bropfvvvv.s ⊢ ( 𝑎 = 𝐴 → 𝑉 = 𝑆 )
4 bropfvvvv.t ⊢ ( 𝑎 = 𝐴 → 𝑊 = 𝑇 )
5 bropfvvvv.p ⊢ ( 𝑎 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
6 brovpreldm ⊢ ( 𝐷 ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) 𝐸 → ⟨ 𝐵 , 𝐶 ⟩ ∈ dom ( 𝑂 ‘ 𝐴 ) )
7 5 opabbidv ⊢ ( 𝑎 = 𝐴 → { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜑 } = { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜓 } )
8 3 4 7 mpoeq123dv ⊢ ( 𝑎 = 𝐴 → ( 𝑏 ∈ 𝑉 , 𝑐 ∈ 𝑊 ↦ { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜑 } ) = ( 𝑏 ∈ 𝑆 , 𝑐 ∈ 𝑇 ↦ { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜓 } ) )
9 8 1 fvmptg ⊢ ( ( 𝐴 ∈ 𝑈 ∧ ( 𝑏 ∈ 𝑆 , 𝑐 ∈ 𝑇 ↦ { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜓 } ) ∈ V ) → ( 𝑂 ‘ 𝐴 ) = ( 𝑏 ∈ 𝑆 , 𝑐 ∈ 𝑇 ↦ { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜓 } ) )
10 9 dmeqd ⊢ ( ( 𝐴 ∈ 𝑈 ∧ ( 𝑏 ∈ 𝑆 , 𝑐 ∈ 𝑇 ↦ { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜓 } ) ∈ V ) → dom ( 𝑂 ‘ 𝐴 ) = dom ( 𝑏 ∈ 𝑆 , 𝑐 ∈ 𝑇 ↦ { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜓 } ) )
11 10 eleq2d ⊢ ( ( 𝐴 ∈ 𝑈 ∧ ( 𝑏 ∈ 𝑆 , 𝑐 ∈ 𝑇 ↦ { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜓 } ) ∈ V ) → ( ⟨ 𝐵 , 𝐶 ⟩ ∈ dom ( 𝑂 ‘ 𝐴 ) ↔ ⟨ 𝐵 , 𝐶 ⟩ ∈ dom ( 𝑏 ∈ 𝑆 , 𝑐 ∈ 𝑇 ↦ { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜓 } ) ) )
12 dmoprabss ⊢ dom { ⟨ ⟨ 𝑏 , 𝑐 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑇 ) ∧ 𝑧 = { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜓 } ) } ⊆ ( 𝑆 × 𝑇 )
13 12 sseli ⊢ ( ⟨ 𝐵 , 𝐶 ⟩ ∈ dom { ⟨ ⟨ 𝑏 , 𝑐 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑇 ) ∧ 𝑧 = { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜓 } ) } → ⟨ 𝐵 , 𝐶 ⟩ ∈ ( 𝑆 × 𝑇 ) )
14 1 2 bropfvvvvlem ⊢ ( ( ⟨ 𝐵 , 𝐶 ⟩ ∈ ( 𝑆 × 𝑇 ) ∧ 𝐷 ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) 𝐸 ) → ( 𝐴 ∈ 𝑈 ∧ ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) )
15 14 ex ⊢ ( ⟨ 𝐵 , 𝐶 ⟩ ∈ ( 𝑆 × 𝑇 ) → ( 𝐷 ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) 𝐸 → ( 𝐴 ∈ 𝑈 ∧ ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) )
16 13 15 syl ⊢ ( ⟨ 𝐵 , 𝐶 ⟩ ∈ dom { ⟨ ⟨ 𝑏 , 𝑐 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑇 ) ∧ 𝑧 = { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜓 } ) } → ( 𝐷 ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) 𝐸 → ( 𝐴 ∈ 𝑈 ∧ ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) )
17 df-mpo ⊢ ( 𝑏 ∈ 𝑆 , 𝑐 ∈ 𝑇 ↦ { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜓 } ) = { ⟨ ⟨ 𝑏 , 𝑐 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑇 ) ∧ 𝑧 = { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜓 } ) }
18 17 dmeqi ⊢ dom ( 𝑏 ∈ 𝑆 , 𝑐 ∈ 𝑇 ↦ { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜓 } ) = dom { ⟨ ⟨ 𝑏 , 𝑐 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑇 ) ∧ 𝑧 = { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜓 } ) }
19 16 18 eleq2s ⊢ ( ⟨ 𝐵 , 𝐶 ⟩ ∈ dom ( 𝑏 ∈ 𝑆 , 𝑐 ∈ 𝑇 ↦ { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜓 } ) → ( 𝐷 ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) 𝐸 → ( 𝐴 ∈ 𝑈 ∧ ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) )
20 11 19 biimtrdi ⊢ ( ( 𝐴 ∈ 𝑈 ∧ ( 𝑏 ∈ 𝑆 , 𝑐 ∈ 𝑇 ↦ { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜓 } ) ∈ V ) → ( ⟨ 𝐵 , 𝐶 ⟩ ∈ dom ( 𝑂 ‘ 𝐴 ) → ( 𝐷 ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) 𝐸 → ( 𝐴 ∈ 𝑈 ∧ ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) ) )
21 20 com23 ⊢ ( ( 𝐴 ∈ 𝑈 ∧ ( 𝑏 ∈ 𝑆 , 𝑐 ∈ 𝑇 ↦ { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜓 } ) ∈ V ) → ( 𝐷 ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) 𝐸 → ( ⟨ 𝐵 , 𝐶 ⟩ ∈ dom ( 𝑂 ‘ 𝐴 ) → ( 𝐴 ∈ 𝑈 ∧ ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) ) )
22 21 a1d ⊢ ( ( 𝐴 ∈ 𝑈 ∧ ( 𝑏 ∈ 𝑆 , 𝑐 ∈ 𝑇 ↦ { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜓 } ) ∈ V ) → ( ( 𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌 ) → ( 𝐷 ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) 𝐸 → ( ⟨ 𝐵 , 𝐶 ⟩ ∈ dom ( 𝑂 ‘ 𝐴 ) → ( 𝐴 ∈ 𝑈 ∧ ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) ) ) )
23 ianor ⊢ ( ¬ ( 𝐴 ∈ 𝑈 ∧ ( 𝑏 ∈ 𝑆 , 𝑐 ∈ 𝑇 ↦ { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜓 } ) ∈ V ) ↔ ( ¬ 𝐴 ∈ 𝑈 ∨ ¬ ( 𝑏 ∈ 𝑆 , 𝑐 ∈ 𝑇 ↦ { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜓 } ) ∈ V ) )
24 1 fvmptndm ⊢ ( ¬ 𝐴 ∈ 𝑈 → ( 𝑂 ‘ 𝐴 ) = ∅ )
25 24 dmeqd ⊢ ( ¬ 𝐴 ∈ 𝑈 → dom ( 𝑂 ‘ 𝐴 ) = dom ∅ )
26 25 eleq2d ⊢ ( ¬ 𝐴 ∈ 𝑈 → ( ⟨ 𝐵 , 𝐶 ⟩ ∈ dom ( 𝑂 ‘ 𝐴 ) ↔ ⟨ 𝐵 , 𝐶 ⟩ ∈ dom ∅ ) )
27 dm0 ⊢ dom ∅ = ∅
28 27 eleq2i ⊢ ( ⟨ 𝐵 , 𝐶 ⟩ ∈ dom ∅ ↔ ⟨ 𝐵 , 𝐶 ⟩ ∈ ∅ )
29 26 28 bitrdi ⊢ ( ¬ 𝐴 ∈ 𝑈 → ( ⟨ 𝐵 , 𝐶 ⟩ ∈ dom ( 𝑂 ‘ 𝐴 ) ↔ ⟨ 𝐵 , 𝐶 ⟩ ∈ ∅ ) )
30 noel ⊢ ¬ ⟨ 𝐵 , 𝐶 ⟩ ∈ ∅
31 30 pm2.21i ⊢ ( ⟨ 𝐵 , 𝐶 ⟩ ∈ ∅ → ( 𝐷 ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) 𝐸 → ( 𝐴 ∈ 𝑈 ∧ ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) )
32 29 31 biimtrdi ⊢ ( ¬ 𝐴 ∈ 𝑈 → ( ⟨ 𝐵 , 𝐶 ⟩ ∈ dom ( 𝑂 ‘ 𝐴 ) → ( 𝐷 ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) 𝐸 → ( 𝐴 ∈ 𝑈 ∧ ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) ) )
33 32 a1d ⊢ ( ¬ 𝐴 ∈ 𝑈 → ( ( 𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌 ) → ( ⟨ 𝐵 , 𝐶 ⟩ ∈ dom ( 𝑂 ‘ 𝐴 ) → ( 𝐷 ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) 𝐸 → ( 𝐴 ∈ 𝑈 ∧ ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) ) ) )
34 notnotb ⊢ ( 𝐴 ∈ 𝑈 ↔ ¬ ¬ 𝐴 ∈ 𝑈 )
35 elex ⊢ ( 𝑆 ∈ 𝑋 → 𝑆 ∈ V )
36 elex ⊢ ( 𝑇 ∈ 𝑌 → 𝑇 ∈ V )
37 35 36 anim12i ⊢ ( ( 𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌 ) → ( 𝑆 ∈ V ∧ 𝑇 ∈ V ) )
38 37 adantl ⊢ ( ( 𝐴 ∈ 𝑈 ∧ ( 𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌 ) ) → ( 𝑆 ∈ V ∧ 𝑇 ∈ V ) )
39 mpoexga ⊢ ( ( 𝑆 ∈ V ∧ 𝑇 ∈ V ) → ( 𝑏 ∈ 𝑆 , 𝑐 ∈ 𝑇 ↦ { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜓 } ) ∈ V )
40 38 39 syl ⊢ ( ( 𝐴 ∈ 𝑈 ∧ ( 𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌 ) ) → ( 𝑏 ∈ 𝑆 , 𝑐 ∈ 𝑇 ↦ { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜓 } ) ∈ V )
41 40 pm2.24d ⊢ ( ( 𝐴 ∈ 𝑈 ∧ ( 𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌 ) ) → ( ¬ ( 𝑏 ∈ 𝑆 , 𝑐 ∈ 𝑇 ↦ { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜓 } ) ∈ V → ( ⟨ 𝐵 , 𝐶 ⟩ ∈ dom ( 𝑂 ‘ 𝐴 ) → ( 𝐷 ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) 𝐸 → ( 𝐴 ∈ 𝑈 ∧ ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) ) ) )
42 41 ex ⊢ ( 𝐴 ∈ 𝑈 → ( ( 𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌 ) → ( ¬ ( 𝑏 ∈ 𝑆 , 𝑐 ∈ 𝑇 ↦ { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜓 } ) ∈ V → ( ⟨ 𝐵 , 𝐶 ⟩ ∈ dom ( 𝑂 ‘ 𝐴 ) → ( 𝐷 ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) 𝐸 → ( 𝐴 ∈ 𝑈 ∧ ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) ) ) ) )
43 42 com23 ⊢ ( 𝐴 ∈ 𝑈 → ( ¬ ( 𝑏 ∈ 𝑆 , 𝑐 ∈ 𝑇 ↦ { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜓 } ) ∈ V → ( ( 𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌 ) → ( ⟨ 𝐵 , 𝐶 ⟩ ∈ dom ( 𝑂 ‘ 𝐴 ) → ( 𝐷 ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) 𝐸 → ( 𝐴 ∈ 𝑈 ∧ ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) ) ) ) )
44 34 43 sylbir ⊢ ( ¬ ¬ 𝐴 ∈ 𝑈 → ( ¬ ( 𝑏 ∈ 𝑆 , 𝑐 ∈ 𝑇 ↦ { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜓 } ) ∈ V → ( ( 𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌 ) → ( ⟨ 𝐵 , 𝐶 ⟩ ∈ dom ( 𝑂 ‘ 𝐴 ) → ( 𝐷 ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) 𝐸 → ( 𝐴 ∈ 𝑈 ∧ ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) ) ) ) )
45 44 imp ⊢ ( ( ¬ ¬ 𝐴 ∈ 𝑈 ∧ ¬ ( 𝑏 ∈ 𝑆 , 𝑐 ∈ 𝑇 ↦ { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜓 } ) ∈ V ) → ( ( 𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌 ) → ( ⟨ 𝐵 , 𝐶 ⟩ ∈ dom ( 𝑂 ‘ 𝐴 ) → ( 𝐷 ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) 𝐸 → ( 𝐴 ∈ 𝑈 ∧ ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) ) ) )
46 33 45 jaoi3 ⊢ ( ( ¬ 𝐴 ∈ 𝑈 ∨ ¬ ( 𝑏 ∈ 𝑆 , 𝑐 ∈ 𝑇 ↦ { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜓 } ) ∈ V ) → ( ( 𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌 ) → ( ⟨ 𝐵 , 𝐶 ⟩ ∈ dom ( 𝑂 ‘ 𝐴 ) → ( 𝐷 ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) 𝐸 → ( 𝐴 ∈ 𝑈 ∧ ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) ) ) )
47 23 46 sylbi ⊢ ( ¬ ( 𝐴 ∈ 𝑈 ∧ ( 𝑏 ∈ 𝑆 , 𝑐 ∈ 𝑇 ↦ { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜓 } ) ∈ V ) → ( ( 𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌 ) → ( ⟨ 𝐵 , 𝐶 ⟩ ∈ dom ( 𝑂 ‘ 𝐴 ) → ( 𝐷 ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) 𝐸 → ( 𝐴 ∈ 𝑈 ∧ ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) ) ) )
48 47 com34 ⊢ ( ¬ ( 𝐴 ∈ 𝑈 ∧ ( 𝑏 ∈ 𝑆 , 𝑐 ∈ 𝑇 ↦ { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜓 } ) ∈ V ) → ( ( 𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌 ) → ( 𝐷 ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) 𝐸 → ( ⟨ 𝐵 , 𝐶 ⟩ ∈ dom ( 𝑂 ‘ 𝐴 ) → ( 𝐴 ∈ 𝑈 ∧ ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) ) ) )
49 22 48 pm2.61i ⊢ ( ( 𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌 ) → ( 𝐷 ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) 𝐸 → ( ⟨ 𝐵 , 𝐶 ⟩ ∈ dom ( 𝑂 ‘ 𝐴 ) → ( 𝐴 ∈ 𝑈 ∧ ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) ) )
50 6 49 mpdi ⊢ ( ( 𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌 ) → ( 𝐷 ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) 𝐸 → ( 𝐴 ∈ 𝑈 ∧ ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) )