This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 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 ) )