Metamath Proof Explorer


Theorem sategoelfv

Description: Condition of a valuation S of a simplified satisfaction predicate for a Godel-set of membership: The sets in model M corresponding to the variables A and B under the assignment of S are in a membership relation in M . (Contributed by AV, 5-Nov-2023)

Ref Expression
Hypothesis sategoelfvb.s 𝐸 = ( 𝑀 Sat ( 𝐴𝑔 𝐵 ) )
Assertion sategoelfv ( ( 𝑀𝑉 ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝑆𝐸 ) → ( 𝑆𝐴 ) ∈ ( 𝑆𝐵 ) )

Proof

Step Hyp Ref Expression
1 sategoelfvb.s 𝐸 = ( 𝑀 Sat ( 𝐴𝑔 𝐵 ) )
2 1 sategoelfvb ( ( 𝑀𝑉 ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( 𝑆𝐸 ↔ ( 𝑆 ∈ ( 𝑀m ω ) ∧ ( 𝑆𝐴 ) ∈ ( 𝑆𝐵 ) ) ) )
3 simpr ( ( 𝑆 ∈ ( 𝑀m ω ) ∧ ( 𝑆𝐴 ) ∈ ( 𝑆𝐵 ) ) → ( 𝑆𝐴 ) ∈ ( 𝑆𝐵 ) )
4 2 3 syl6bi ( ( 𝑀𝑉 ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( 𝑆𝐸 → ( 𝑆𝐴 ) ∈ ( 𝑆𝐵 ) ) )
5 4 3impia ( ( 𝑀𝑉 ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝑆𝐸 ) → ( 𝑆𝐴 ) ∈ ( 𝑆𝐵 ) )