Theorem ovmpt3rabdm

Description: If the value of a function which is the result of an operation defined by the maps-to notation is not empty, the operands and the argument of the function must be sets. (Contributed by AV, 16-May-2019)

	Ref	Expression
Hypotheses	ovmpt3rab1.o	⊢ 𝑂 = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑧 ∈ 𝑀 ↦ { 𝑎 ∈ 𝑁 ∣ 𝜑 } ) )
	ovmpt3rab1.m	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → 𝑀 = 𝐾 )
	ovmpt3rab1.n	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → 𝑁 = 𝐿 )
Assertion	ovmpt3rabdm	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐾 ∈ 𝑈 ) ∧ 𝐿 ∈ 𝑇 ) → dom ( 𝑋 𝑂 𝑌 ) = 𝐾 )

Proof

Step	Hyp	Ref	Expression
1		ovmpt3rab1.o	⊢ 𝑂 = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑧 ∈ 𝑀 ↦ { 𝑎 ∈ 𝑁 ∣ 𝜑 } ) )
2		ovmpt3rab1.m	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → 𝑀 = 𝐾 )
3		ovmpt3rab1.n	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → 𝑁 = 𝐿 )
4		sbceq1a	⊢ ( 𝑦 = 𝑌 → ( 𝜑 ↔ [ 𝑌 / 𝑦 ] 𝜑 ) )
5		sbceq1a	⊢ ( 𝑥 = 𝑋 → ( [ 𝑌 / 𝑦 ] 𝜑 ↔ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 ) )
6	4 5	sylan9bbr	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( 𝜑 ↔ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 ) )
7		nfsbc1v	⊢ Ⅎ 𝑥 [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑
8		nfcv	⊢ Ⅎ 𝑦 𝑋
9		nfsbc1v	⊢ Ⅎ 𝑦 [ 𝑌 / 𝑦 ] 𝜑
10	8 9	nfsbcw	⊢ Ⅎ 𝑦 [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑
11	1 2 3 6 7 10	ovmpt3rab1	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐾 ∈ 𝑈 ) → ( 𝑋 𝑂 𝑌 ) = ( 𝑧 ∈ 𝐾 ↦ { 𝑎 ∈ 𝐿 ∣ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 } ) )
12	11	adantr	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐾 ∈ 𝑈 ) ∧ 𝐿 ∈ 𝑇 ) → ( 𝑋 𝑂 𝑌 ) = ( 𝑧 ∈ 𝐾 ↦ { 𝑎 ∈ 𝐿 ∣ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 } ) )
13	12	dmeqd	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐾 ∈ 𝑈 ) ∧ 𝐿 ∈ 𝑇 ) → dom ( 𝑋 𝑂 𝑌 ) = dom ( 𝑧 ∈ 𝐾 ↦ { 𝑎 ∈ 𝐿 ∣ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 } ) )
14		rabexg	⊢ ( 𝐿 ∈ 𝑇 → { 𝑎 ∈ 𝐿 ∣ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 } ∈ V )
15	14	adantl	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐾 ∈ 𝑈 ) ∧ 𝐿 ∈ 𝑇 ) → { 𝑎 ∈ 𝐿 ∣ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 } ∈ V )
16	15	ralrimivw	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐾 ∈ 𝑈 ) ∧ 𝐿 ∈ 𝑇 ) → ∀ 𝑧 ∈ 𝐾 { 𝑎 ∈ 𝐿 ∣ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 } ∈ V )
17		dmmptg	⊢ ( ∀ 𝑧 ∈ 𝐾 { 𝑎 ∈ 𝐿 ∣ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 } ∈ V → dom ( 𝑧 ∈ 𝐾 ↦ { 𝑎 ∈ 𝐿 ∣ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 } ) = 𝐾 )
18	16 17	syl	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐾 ∈ 𝑈 ) ∧ 𝐿 ∈ 𝑇 ) → dom ( 𝑧 ∈ 𝐾 ↦ { 𝑎 ∈ 𝐿 ∣ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 } ) = 𝐾 )
19	13 18	eqtrd	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐾 ∈ 𝑈 ) ∧ 𝐿 ∈ 𝑇 ) → dom ( 𝑋 𝑂 𝑌 ) = 𝐾 )