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

Metamath Proof Explorer

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 ( 𝑋 𝑂 𝑌 ) = 𝐾 )