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

Metamath Proof Explorer

Theorem ex-sategoelel12

Description: Example of a valuation of a simplified satisfaction predicate over a proper pair (of ordinal numbers) as model for a Godel-set of membership using the properties of a successor: ( S2o ) = 1o e. 2o = ( 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-sategoelel12.s 
|- S = ( x e. _om |-> if ( x = 2o , 1o , 2o ) )
Assertion ex-sategoelel12 
|- S e. ( { 1o , 2o } SatE ( 2o e.g 1o ) )

Proof

Step Hyp Ref Expression
1 ex-sategoelel12.s 
 |-  S = ( x e. _om |-> if ( x = 2o , 1o , 2o ) )
2 1oex 
 |-  1o e. _V
3 2 prid1 
 |-  1o e. { 1o , 2o }
4 2oex 
 |-  2o e. _V
5 4 prid2 
 |-  2o e. { 1o , 2o }
6 3 5 ifcli 
 |-  if ( x = 2o , 1o , 2o ) e. { 1o , 2o }
7 6 a1i 
 |-  ( x e. _om -> if ( x = 2o , 1o , 2o ) e. { 1o , 2o } )
8 1 7 fmpti 
 |-  S : _om --> { 1o , 2o }
9 prex 
 |-  { 1o , 2o } e. _V
10 omex 
 |-  _om e. _V
11 9 10 elmap 
 |-  ( S e. ( { 1o , 2o } ^m _om ) <-> S : _om --> { 1o , 2o } )
12 8 11 mpbir 
 |-  S e. ( { 1o , 2o } ^m _om )
13 2 sucid 
 |-  1o e. suc 1o
14 df-2o 
 |-  2o = suc 1o
15 13 14 eleqtrri 
 |-  1o e. 2o
16 2onn 
 |-  2o e. _om
17 1onn 
 |-  1o e. _om
18 iftrue 
 |-  ( x = 2o -> if ( x = 2o , 1o , 2o ) = 1o )
19 18 1 fvmptg 
 |-  ( ( 2o e. _om /\ 1o e. _om ) -> ( S ` 2o ) = 1o )
20 16 17 19 mp2an 
 |-  ( S ` 2o ) = 1o
21 1one2o 
 |-  1o =/= 2o
22 21 neii 
 |-  -. 1o = 2o
23 eqeq1 
 |-  ( x = 1o -> ( x = 2o <-> 1o = 2o ) )
24 22 23 mtbiri 
 |-  ( x = 1o -> -. x = 2o )
25 24 iffalsed 
 |-  ( x = 1o -> if ( x = 2o , 1o , 2o ) = 2o )
26 25 1 fvmptg 
 |-  ( ( 1o e. _om /\ 2o e. _om ) -> ( S ` 1o ) = 2o )
27 17 16 26 mp2an 
 |-  ( S ` 1o ) = 2o
28 15 20 27 3eltr4i 
 |-  ( S ` 2o ) e. ( S ` 1o )
29 12 28 pm3.2i 
 |-  ( S e. ( { 1o , 2o } ^m _om ) /\ ( S ` 2o ) e. ( S ` 1o ) )
30 16 17 pm3.2i 
 |-  ( 2o e. _om /\ 1o e. _om )
31 eqid 
 |-  ( { 1o , 2o } SatE ( 2o e.g 1o ) ) = ( { 1o , 2o } SatE ( 2o e.g 1o ) )
32 31 sategoelfvb 
 |-  ( ( { 1o , 2o } e. _V /\ ( 2o e. _om /\ 1o e. _om ) ) -> ( S e. ( { 1o , 2o } SatE ( 2o e.g 1o ) ) <-> ( S e. ( { 1o , 2o } ^m _om ) /\ ( S ` 2o ) e. ( S ` 1o ) ) ) )
33 9 30 32 mp2an 
 |-  ( S e. ( { 1o , 2o } SatE ( 2o e.g 1o ) ) <-> ( S e. ( { 1o , 2o } ^m _om ) /\ ( S ` 2o ) e. ( S ` 1o ) ) )
34 29 33 mpbir 
 |-  S e. ( { 1o , 2o } SatE ( 2o e.g 1o ) )