Metamath Proof Explorer

Theorem ex-sategoelel

Description: 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-sategoelel 
|- ( ( ( M e. WUni /\ Z e. M ) /\ ( A e. _om /\ B e. _om /\ A =/= B ) ) -> S e. E )

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 simpr 
 |-  ( ( M e. WUni /\ Z e. M ) -> Z e. M )
4 simpl 
 |-  ( ( M e. WUni /\ Z e. M ) -> M e. WUni )
5 4 3 wunpw 
 |-  ( ( M e. WUni /\ Z e. M ) -> ~P Z e. M )
6 4 wun0 
 |-  ( ( M e. WUni /\ Z e. M ) -> (/) e. M )
7 5 6 ifcld 
 |-  ( ( M e. WUni /\ Z e. M ) -> if ( x = B , ~P Z , (/) ) e. M )
8 3 7 ifcld 
 |-  ( ( M e. WUni /\ Z e. M ) -> if ( x = A , Z , if ( x = B , ~P Z , (/) ) ) e. M )
9 8 adantr 
 |-  ( ( ( M e. WUni /\ Z e. M ) /\ ( A e. _om /\ B e. _om /\ A =/= B ) ) -> if ( x = A , Z , if ( x = B , ~P Z , (/) ) ) e. M )
10 9 adantr 
 |-  ( ( ( ( M e. WUni /\ Z e. M ) /\ ( A e. _om /\ B e. _om /\ A =/= B ) ) /\ x e. _om ) -> if ( x = A , Z , if ( x = B , ~P Z , (/) ) ) e. M )
11 10 2 fmptd 
 |-  ( ( ( M e. WUni /\ Z e. M ) /\ ( A e. _om /\ B e. _om /\ A =/= B ) ) -> S : _om --> M )
12 4 adantr 
 |-  ( ( ( M e. WUni /\ Z e. M ) /\ ( A e. _om /\ B e. _om /\ A =/= B ) ) -> M e. WUni )
13 omex 
 |-  _om e. _V
14 13 a1i 
 |-  ( ( ( M e. WUni /\ Z e. M ) /\ ( A e. _om /\ B e. _om /\ A =/= B ) ) -> _om e. _V )
15 12 14 elmapd 
 |-  ( ( ( M e. WUni /\ Z e. M ) /\ ( A e. _om /\ B e. _om /\ A =/= B ) ) -> ( S e. ( M ^m _om ) <-> S : _om --> M ) )
16 11 15 mpbird 
 |-  ( ( ( M e. WUni /\ Z e. M ) /\ ( A e. _om /\ B e. _om /\ A =/= B ) ) -> S e. ( M ^m _om ) )
17 pwidg 
 |-  ( Z e. M -> Z e. ~P Z )
18 17 adantl 
 |-  ( ( M e. WUni /\ Z e. M ) -> Z e. ~P Z )
19 18 adantr 
 |-  ( ( ( M e. WUni /\ Z e. M ) /\ ( A e. _om /\ B e. _om /\ A =/= B ) ) -> Z e. ~P Z )
20 2 a1i 
 |-  ( ( ( M e. WUni /\ Z e. M ) /\ ( A e. _om /\ B e. _om /\ A =/= B ) ) -> S = ( x e. _om |-> if ( x = A , Z , if ( x = B , ~P Z , (/) ) ) ) )
21 iftrue 
 |-  ( x = A -> if ( x = A , Z , if ( x = B , ~P Z , (/) ) ) = Z )
22 21 adantl 
 |-  ( ( ( ( M e. WUni /\ Z e. M ) /\ ( A e. _om /\ B e. _om /\ A =/= B ) ) /\ x = A ) -> if ( x = A , Z , if ( x = B , ~P Z , (/) ) ) = Z )
23 simpr1 
 |-  ( ( ( M e. WUni /\ Z e. M ) /\ ( A e. _om /\ B e. _om /\ A =/= B ) ) -> A e. _om )
24 3 adantr 
 |-  ( ( ( M e. WUni /\ Z e. M ) /\ ( A e. _om /\ B e. _om /\ A =/= B ) ) -> Z e. M )
25 20 22 23 24 fvmptd 
 |-  ( ( ( M e. WUni /\ Z e. M ) /\ ( A e. _om /\ B e. _om /\ A =/= B ) ) -> ( S ` A ) = Z )
26 eqeq1 
 |-  ( x = B -> ( x = A <-> B = A ) )
27 eqeq1 
 |-  ( x = B -> ( x = B <-> B = B ) )
28 27 ifbid 
 |-  ( x = B -> if ( x = B , ~P Z , (/) ) = if ( B = B , ~P Z , (/) ) )
29 26 28 ifbieq2d 
 |-  ( x = B -> if ( x = A , Z , if ( x = B , ~P Z , (/) ) ) = if ( B = A , Z , if ( B = B , ~P Z , (/) ) ) )
30 necom 
 |-  ( A =/= B <-> B =/= A )
31 ifnefalse 
 |-  ( B =/= A -> if ( B = A , Z , if ( B = B , ~P Z , (/) ) ) = if ( B = B , ~P Z , (/) ) )
32 30 31 sylbi 
 |-  ( A =/= B -> if ( B = A , Z , if ( B = B , ~P Z , (/) ) ) = if ( B = B , ~P Z , (/) ) )
33 32 3ad2ant3 
 |-  ( ( A e. _om /\ B e. _om /\ A =/= B ) -> if ( B = A , Z , if ( B = B , ~P Z , (/) ) ) = if ( B = B , ~P Z , (/) ) )
34 33 adantl 
 |-  ( ( ( M e. WUni /\ Z e. M ) /\ ( A e. _om /\ B e. _om /\ A =/= B ) ) -> if ( B = A , Z , if ( B = B , ~P Z , (/) ) ) = if ( B = B , ~P Z , (/) ) )
35 29 34 sylan9eqr 
 |-  ( ( ( ( M e. WUni /\ Z e. M ) /\ ( A e. _om /\ B e. _om /\ A =/= B ) ) /\ x = B ) -> if ( x = A , Z , if ( x = B , ~P Z , (/) ) ) = if ( B = B , ~P Z , (/) ) )
36 simpr2 
 |-  ( ( ( M e. WUni /\ Z e. M ) /\ ( A e. _om /\ B e. _om /\ A =/= B ) ) -> B e. _om )
37 pwexg 
 |-  ( Z e. M -> ~P Z e. _V )
38 37 adantl 
 |-  ( ( M e. WUni /\ Z e. M ) -> ~P Z e. _V )
39 0ex 
 |-  (/) e. _V
40 39 a1i 
 |-  ( ( M e. WUni /\ Z e. M ) -> (/) e. _V )
41 38 40 ifcld 
 |-  ( ( M e. WUni /\ Z e. M ) -> if ( B = B , ~P Z , (/) ) e. _V )
42 41 adantr 
 |-  ( ( ( M e. WUni /\ Z e. M ) /\ ( A e. _om /\ B e. _om /\ A =/= B ) ) -> if ( B = B , ~P Z , (/) ) e. _V )
43 20 35 36 42 fvmptd 
 |-  ( ( ( M e. WUni /\ Z e. M ) /\ ( A e. _om /\ B e. _om /\ A =/= B ) ) -> ( S ` B ) = if ( B = B , ~P Z , (/) ) )
44 eqid 
 |-  B = B
45 44 iftruei 
 |-  if ( B = B , ~P Z , (/) ) = ~P Z
46 43 45 eqtrdi 
 |-  ( ( ( M e. WUni /\ Z e. M ) /\ ( A e. _om /\ B e. _om /\ A =/= B ) ) -> ( S ` B ) = ~P Z )
47 19 25 46 3eltr4d 
 |-  ( ( ( M e. WUni /\ Z e. M ) /\ ( A e. _om /\ B e. _om /\ A =/= B ) ) -> ( S ` A ) e. ( S ` B ) )
48 3simpa 
 |-  ( ( A e. _om /\ B e. _om /\ A =/= B ) -> ( A e. _om /\ B e. _om ) )
49 1 sategoelfvb 
 |-  ( ( M e. WUni /\ ( A e. _om /\ B e. _om ) ) -> ( S e. E <-> ( S e. ( M ^m _om ) /\ ( S ` A ) e. ( S ` B ) ) ) )
50 4 48 49 syl2an 
 |-  ( ( ( M e. WUni /\ Z e. M ) /\ ( A e. _om /\ B e. _om /\ A =/= B ) ) -> ( S e. E <-> ( S e. ( M ^m _om ) /\ ( S ` A ) e. ( S ` B ) ) ) )
51 16 47 50 mpbir2and 
 |-  ( ( ( M e. WUni /\ Z e. M ) /\ ( A e. _om /\ B e. _om /\ A =/= B ) ) -> S e. E )