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	$⊢ E = M {Sat}_{\in} (A \in_{𝑔} B)$
	Assertion	sategoelfv	$⊢ (M \in V \land (A \in ω \land B \in ω) \land S \in E) \to S (A) \in S (B)$

Proof

Step	Hyp	Ref	Expression
1		sategoelfvb.s	$⊢ E = M {Sat}_{\in} (A \in_{𝑔} B)$
2	1	sategoelfvb	$⊢ (M \in V \land (A \in ω \land B \in ω)) \to (S \in E \leftrightarrow (S \in (M^{ω}) \land S (A) \in S (B)))$
3		simpr	$⊢ (S \in (M^{ω}) \land S (A) \in S (B)) \to S (A) \in S (B)$
4	2 3	biimtrdi	$⊢ (M \in V \land (A \in ω \land B \in ω)) \to (S \in E \to S (A) \in S (B))$
5	4	3impia	$⊢ (M \in V \land (A \in ω \land B \in ω) \land S \in E) \to S (A) \in S (B)$