Theorem prv

Description: The "proves" relation on a set. A wff encoded as U is true in a model M iff for every valuation s e. ( M ^m _om ) , the interpretation of the wff using the membership relation on M is true. (Contributed by AV, 5-Nov-2023)

	Ref	Expression
Assertion	prv	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝑈 ∈ 𝑊 ) → ( 𝑀 ⊧ 𝑈 ↔ ( 𝑀 Sat∈ 𝑈 ) = ( 𝑀 ↑m ω ) ) )

Proof

Step	Hyp	Ref	Expression
1		oveq12	⊢ ( ( 𝑚 = 𝑀 ∧ 𝑢 = 𝑈 ) → ( 𝑚 Sat∈ 𝑢 ) = ( 𝑀 Sat∈ 𝑈 ) )
2		simpl	⊢ ( ( 𝑚 = 𝑀 ∧ 𝑢 = 𝑈 ) → 𝑚 = 𝑀 )
3	2	oveq1d	⊢ ( ( 𝑚 = 𝑀 ∧ 𝑢 = 𝑈 ) → ( 𝑚 ↑m ω ) = ( 𝑀 ↑m ω ) )
4	1 3	eqeq12d	⊢ ( ( 𝑚 = 𝑀 ∧ 𝑢 = 𝑈 ) → ( ( 𝑚 Sat∈ 𝑢 ) = ( 𝑚 ↑m ω ) ↔ ( 𝑀 Sat∈ 𝑈 ) = ( 𝑀 ↑m ω ) ) )
5		df-prv	⊢ ⊧ = { ⟨ 𝑚 , 𝑢 ⟩ ∣ ( 𝑚 Sat∈ 𝑢 ) = ( 𝑚 ↑m ω ) }
6	4 5	brabga	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝑈 ∈ 𝑊 ) → ( 𝑀 ⊧ 𝑈 ↔ ( 𝑀 Sat∈ 𝑈 ) = ( 𝑀 ↑m ω ) ) )