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

Metamath Proof Explorer

Theorem sprmpod

Description: The extension of a binary relation which is the value of an operation given in maps-to notation. (Contributed by Alexander van der Vekens, 30-Oct-2017) (Revised by AV, 20-Jun-2019)

Ref Expression
Hypotheses sprmpod.1 ⊢ 𝑀 = ( 𝑣 ∈ V , 𝑒 ∈ V ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ( 𝑣 𝑅 𝑒 ) 𝑦 ∧ 𝜒 ) } )
sprmpod.2 ⊢ ( ( 𝜑 ∧ 𝑣 = 𝑉 ∧ 𝑒 = 𝐸 ) → ( 𝜒 ↔ 𝜓 ) )
sprmpod.3 ⊢ ( 𝜑 → ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) )
sprmpod.4 ⊢ ( 𝜑 → ∀ 𝑥 ∀ 𝑦 ( 𝑥 ( 𝑉 𝑅 𝐸 ) 𝑦 → 𝜃 ) )
sprmpod.5 ⊢ ( 𝜑 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜃 } ∈ V )
Assertion sprmpod ( 𝜑 → ( 𝑉 𝑀 𝐸 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ( 𝑉 𝑅 𝐸 ) 𝑦 ∧ 𝜓 ) } )

Proof

Step Hyp Ref Expression
1 sprmpod.1 ⊢ 𝑀 = ( 𝑣 ∈ V , 𝑒 ∈ V ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ( 𝑣 𝑅 𝑒 ) 𝑦 ∧ 𝜒 ) } )
2 sprmpod.2 ⊢ ( ( 𝜑 ∧ 𝑣 = 𝑉 ∧ 𝑒 = 𝐸 ) → ( 𝜒 ↔ 𝜓 ) )
3 sprmpod.3 ⊢ ( 𝜑 → ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) )
4 sprmpod.4 ⊢ ( 𝜑 → ∀ 𝑥 ∀ 𝑦 ( 𝑥 ( 𝑉 𝑅 𝐸 ) 𝑦 → 𝜃 ) )
5 sprmpod.5 ⊢ ( 𝜑 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜃 } ∈ V )
6 1 a1i ⊢ ( 𝜑 → 𝑀 = ( 𝑣 ∈ V , 𝑒 ∈ V ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ( 𝑣 𝑅 𝑒 ) 𝑦 ∧ 𝜒 ) } ) )
7 oveq12 ⊢ ( ( 𝑣 = 𝑉 ∧ 𝑒 = 𝐸 ) → ( 𝑣 𝑅 𝑒 ) = ( 𝑉 𝑅 𝐸 ) )
8 7 breqd ⊢ ( ( 𝑣 = 𝑉 ∧ 𝑒 = 𝐸 ) → ( 𝑥 ( 𝑣 𝑅 𝑒 ) 𝑦 ↔ 𝑥 ( 𝑉 𝑅 𝐸 ) 𝑦 ) )
9 8 adantl ⊢ ( ( 𝜑 ∧ ( 𝑣 = 𝑉 ∧ 𝑒 = 𝐸 ) ) → ( 𝑥 ( 𝑣 𝑅 𝑒 ) 𝑦 ↔ 𝑥 ( 𝑉 𝑅 𝐸 ) 𝑦 ) )
10 2 3expb ⊢ ( ( 𝜑 ∧ ( 𝑣 = 𝑉 ∧ 𝑒 = 𝐸 ) ) → ( 𝜒 ↔ 𝜓 ) )
11 9 10 anbi12d ⊢ ( ( 𝜑 ∧ ( 𝑣 = 𝑉 ∧ 𝑒 = 𝐸 ) ) → ( ( 𝑥 ( 𝑣 𝑅 𝑒 ) 𝑦 ∧ 𝜒 ) ↔ ( 𝑥 ( 𝑉 𝑅 𝐸 ) 𝑦 ∧ 𝜓 ) ) )
12 11 opabbidv ⊢ ( ( 𝜑 ∧ ( 𝑣 = 𝑉 ∧ 𝑒 = 𝐸 ) ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ( 𝑣 𝑅 𝑒 ) 𝑦 ∧ 𝜒 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ( 𝑉 𝑅 𝐸 ) 𝑦 ∧ 𝜓 ) } )
13 3 simpld ⊢ ( 𝜑 → 𝑉 ∈ V )
14 3 simprd ⊢ ( 𝜑 → 𝐸 ∈ V )
15 opabbrex ⊢ ( ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 ( 𝑉 𝑅 𝐸 ) 𝑦 → 𝜃 ) ∧ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜃 } ∈ V ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ( 𝑉 𝑅 𝐸 ) 𝑦 ∧ 𝜓 ) } ∈ V )
16 4 5 15 syl2anc ⊢ ( 𝜑 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ( 𝑉 𝑅 𝐸 ) 𝑦 ∧ 𝜓 ) } ∈ V )
17 6 12 13 14 16 ovmpod ⊢ ( 𝜑 → ( 𝑉 𝑀 𝐸 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ( 𝑉 𝑅 𝐸 ) 𝑦 ∧ 𝜓 ) } )