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 SatE ( A e.g B ) )
	ex-sategoelel.s	|- S = ( x e. _om |-> if ( x = A , Z , if ( x = B , ~P Z , (/) ) ) )
Assertion	ex-sategoel	|- ( ( ( M e. WUni /\ Z e. M ) /\ ( A e. _om /\ B e. _om /\ A =/= B ) ) -> ( S ` A ) e. ( S ` B ) )

Proof

Step	Hyp	Ref	Expression
1		sategoelfvb.s	|- E = ( M SatE ( A e.g B ) )
2		ex-sategoelel.s	|- S = ( x e. _om |-> if ( x = A , Z , if ( x = B , ~P Z , (/) ) ) )
3		simpll	|- ( ( ( M e. WUni /\ Z e. M ) /\ ( A e. _om /\ B e. _om /\ A =/= B ) ) -> M e. WUni )
4		3simpa	|- ( ( A e. _om /\ B e. _om /\ A =/= B ) -> ( A e. _om /\ B e. _om ) )
5	4	adantl	|- ( ( ( M e. WUni /\ Z e. M ) /\ ( A e. _om /\ B e. _om /\ A =/= B ) ) -> ( A e. _om /\ B e. _om ) )
6	1 2	ex-sategoelel	|- ( ( ( M e. WUni /\ Z e. M ) /\ ( A e. _om /\ B e. _om /\ A =/= B ) ) -> S e. E )
7	1	sategoelfv	|- ( ( M e. WUni /\ ( A e. _om /\ B e. _om ) /\ S e. E ) -> ( S ` A ) e. ( S ` B ) )
8	3 5 6 7	syl3anc	|- ( ( ( M e. WUni /\ Z e. M ) /\ ( A e. _om /\ B e. _om /\ A =/= B ) ) -> ( S ` A ) e. ( S ` B ) )