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	syl6bi	⊢ ( ( 𝐴 ∈ 𝑈 ∧ ( 𝑏 ∈ 𝑆 , 𝑐 ∈ 𝑇 ↦ { ⟨ 𝑑 , 𝑒 ⟩ ∣ 𝜓 } ) ∈ 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	syl6bi	⊢ ( ¬ 𝐴 ∈ 𝑈 → ( ⟨ 𝐵 , 𝐶 ⟩ ∈ 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 ) ) ) )

Metamath Proof Explorer

Theorem bropfvvvv

Proof