Metamath Proof Explorer

Theorem ex-sategoel

Description: Instance of sategoelfv for the example of a valuation of a simplified satisfaction predicate for a Godel-set of membership. (Contributed by AV, 5-Nov-2023)

		Ref	Expression
	Hypotheses	sategoelfvb.s	$⊢ E = M {Sat}_{\in} (A \in_{𝑔} B)$
		ex-sategoelel.s	$⊢ S = (x \in ω ⟼ if (x = A, Z, if (x = B, 𝒫 Z, \emptyset)))$
	Assertion	ex-sategoel	$⊢ ((M \in WUni \land Z \in M) \land (A \in ω \land B \in ω \land A \neq B)) \to S (A) \in S (B)$

Proof

Step	Hyp	Ref	Expression
1		sategoelfvb.s	$⊢ E = M {Sat}_{\in} (A \in_{𝑔} B)$
2		ex-sategoelel.s	$⊢ S = (x \in ω ⟼ if (x = A, Z, if (x = B, 𝒫 Z, \emptyset)))$
3		simpll	$⊢ ((M \in WUni \land Z \in M) \land (A \in ω \land B \in ω \land A \neq B)) \to M \in WUni$
4		3simpa	$⊢ (A \in ω \land B \in ω \land A \neq B) \to (A \in ω \land B \in ω)$
5	4	adantl	$⊢ ((M \in WUni \land Z \in M) \land (A \in ω \land B \in ω \land A \neq B)) \to (A \in ω \land B \in ω)$
6	1 2	ex-sategoelel	$⊢ ((M \in WUni \land Z \in M) \land (A \in ω \land B \in ω \land A \neq B)) \to S \in E$
7	1	sategoelfv	$⊢ (M \in WUni \land (A \in ω \land B \in ω) \land S \in E) \to S (A) \in S (B)$
8	3 5 6 7	syl3anc	$⊢ ((M \in WUni \land Z \in M) \land (A \in ω \land B \in ω \land A \neq B)) \to S (A) \in S (B)$