Metamath Proof Explorer

Theorem ex-sategoelelomsuc

Description: Example of a valuation of a simplified satisfaction predicate over the ordinal numbers as model for a Godel-set of membership using the properties of a successor: ( S2o ) = Z e. suc Z = ( S2o ) . Remark: the indices 1o and 2o are intentionally reversed to distinguish them from elements of the model: ( 2o e.g 1o ) should not be confused with 2o e. 1o , which is false. (Contributed by AV, 19-Nov-2023)

Ref Expression
Hypothesis ex-sategoelelomsuc.s 
|- S = ( x e. _om |-> if ( x = 2o , Z , suc Z ) )
Assertion ex-sategoelelomsuc 
|- ( Z e. _om -> S e. ( _om SatE ( 2o e.g 1o ) ) )

Proof

Step Hyp Ref Expression
1 ex-sategoelelomsuc.s 
 |-  S = ( x e. _om |-> if ( x = 2o , Z , suc Z ) )
2 id 
 |-  ( Z e. _om -> Z e. _om )
3 peano2 
 |-  ( Z e. _om -> suc Z e. _om )
4 2 3 ifcld 
 |-  ( Z e. _om -> if ( x = 2o , Z , suc Z ) e. _om )
5 4 adantr 
 |-  ( ( Z e. _om /\ x e. _om ) -> if ( x = 2o , Z , suc Z ) e. _om )
6 5 1 fmptd 
 |-  ( Z e. _om -> S : _om --> _om )
7 omex 
 |-  _om e. _V
8 7 a1i 
 |-  ( Z e. _om -> _om e. _V )
9 8 8 elmapd 
 |-  ( Z e. _om -> ( S e. ( _om ^m _om ) <-> S : _om --> _om ) )
10 6 9 mpbird 
 |-  ( Z e. _om -> S e. ( _om ^m _om ) )
11 sucidg 
 |-  ( Z e. _om -> Z e. suc Z )
12 1 a1i 
 |-  ( Z e. _om -> S = ( x e. _om |-> if ( x = 2o , Z , suc Z ) ) )
13 iftrue 
 |-  ( x = 2o -> if ( x = 2o , Z , suc Z ) = Z )
14 13 adantl 
 |-  ( ( Z e. _om /\ x = 2o ) -> if ( x = 2o , Z , suc Z ) = Z )
15 2onn 
 |-  2o e. _om
16 15 a1i 
 |-  ( Z e. _om -> 2o e. _om )
17 12 14 16 2 fvmptd 
 |-  ( Z e. _om -> ( S ` 2o ) = Z )
18 1one2o 
 |-  1o =/= 2o
19 18 neii 
 |-  -. 1o = 2o
20 eqeq1 
 |-  ( x = 1o -> ( x = 2o <-> 1o = 2o ) )
21 19 20 mtbiri 
 |-  ( x = 1o -> -. x = 2o )
22 21 iffalsed 
 |-  ( x = 1o -> if ( x = 2o , Z , suc Z ) = suc Z )
23 22 adantl 
 |-  ( ( Z e. _om /\ x = 1o ) -> if ( x = 2o , Z , suc Z ) = suc Z )
24 1onn 
 |-  1o e. _om
25 24 a1i 
 |-  ( Z e. _om -> 1o e. _om )
26 12 23 25 3 fvmptd 
 |-  ( Z e. _om -> ( S ` 1o ) = suc Z )
27 11 17 26 3eltr4d 
 |-  ( Z e. _om -> ( S ` 2o ) e. ( S ` 1o ) )
28 15 24 pm3.2i 
 |-  ( 2o e. _om /\ 1o e. _om )
29 7 28 pm3.2i 
 |-  ( _om e. _V /\ ( 2o e. _om /\ 1o e. _om ) )
30 eqid 
 |-  ( _om SatE ( 2o e.g 1o ) ) = ( _om SatE ( 2o e.g 1o ) )
31 30 sategoelfvb 
 |-  ( ( _om e. _V /\ ( 2o e. _om /\ 1o e. _om ) ) -> ( S e. ( _om SatE ( 2o e.g 1o ) ) <-> ( S e. ( _om ^m _om ) /\ ( S ` 2o ) e. ( S ` 1o ) ) ) )
32 29 31 mp1i 
 |-  ( Z e. _om -> ( S e. ( _om SatE ( 2o e.g 1o ) ) <-> ( S e. ( _om ^m _om ) /\ ( S ` 2o ) e. ( S ` 1o ) ) ) )
33 10 27 32 mpbir2and 
 |-  ( Z e. _om -> S e. ( _om SatE ( 2o e.g 1o ) ) )