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	⊢ ( 𝜑 → ( 𝑉 𝑀 𝐸 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ( 𝑉 𝑅 𝐸 ) 𝑦 ∧ 𝜓 ) } )