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 ⊢ 𝑆 = ( 𝑥 ∈ ω ↦ if ( 𝑥 = 2o , 1o , 2o ) )
Assertion ex-sategoelel12 𝑆 ∈ ( { 1o , 2o } Sat∈ ( 2o ∈𝑔 1o ) )

Proof

Step Hyp Ref Expression
1 ex-sategoelel12.s ⊢ 𝑆 = ( 𝑥 ∈ ω ↦ if ( 𝑥 = 2o , 1o , 2o ) )
2 1oex ⊢ 1o ∈ V
3 2 prid1 ⊢ 1o ∈ { 1o , 2o }
4 2oex ⊢ 2o ∈ V
5 4 prid2 ⊢ 2o ∈ { 1o , 2o }
6 3 5 ifcli ⊢ if ( 𝑥 = 2o , 1o , 2o ) ∈ { 1o , 2o }
7 6 a1i ⊢ ( 𝑥 ∈ ω → if ( 𝑥 = 2o , 1o , 2o ) ∈ { 1o , 2o } )
8 1 7 fmpti ⊢ 𝑆 : ω ⟶ { 1o , 2o }
9 prex ⊢ { 1o , 2o } ∈ V
10 omex ⊢ ω ∈ V
11 9 10 elmap ⊢ ( 𝑆 ∈ ( { 1o , 2o } ↑m ω ) ↔ 𝑆 : ω ⟶ { 1o , 2o } )
12 8 11 mpbir ⊢ 𝑆 ∈ ( { 1o , 2o } ↑m ω )
13 2 sucid ⊢ 1o ∈ suc 1o
14 df-2o ⊢ 2o = suc 1o
15 13 14 eleqtrri ⊢ 1o ∈ 2o
16 2onn ⊢ 2o ∈ ω
17 1onn ⊢ 1o ∈ ω
18 iftrue ⊢ ( 𝑥 = 2o → if ( 𝑥 = 2o , 1o , 2o ) = 1o )
19 18 1 fvmptg ⊢ ( ( 2o ∈ ω ∧ 1o ∈ ω ) → ( 𝑆 ‘ 2o ) = 1o )
20 16 17 19 mp2an ⊢ ( 𝑆 ‘ 2o ) = 1o
21 1one2o ⊢ 1o ≠ 2o
22 21 neii ⊢ ¬ 1o = 2o
23 eqeq1 ⊢ ( 𝑥 = 1o → ( 𝑥 = 2o ↔ 1o = 2o ) )
24 22 23 mtbiri ⊢ ( 𝑥 = 1o → ¬ 𝑥 = 2o )
25 24 iffalsed ⊢ ( 𝑥 = 1o → if ( 𝑥 = 2o , 1o , 2o ) = 2o )
26 25 1 fvmptg ⊢ ( ( 1o ∈ ω ∧ 2o ∈ ω ) → ( 𝑆 ‘ 1o ) = 2o )
27 17 16 26 mp2an ⊢ ( 𝑆 ‘ 1o ) = 2o
28 15 20 27 3eltr4i ⊢ ( 𝑆 ‘ 2o ) ∈ ( 𝑆 ‘ 1o )
29 12 28 pm3.2i ⊢ ( 𝑆 ∈ ( { 1o , 2o } ↑m ω ) ∧ ( 𝑆 ‘ 2o ) ∈ ( 𝑆 ‘ 1o ) )
30 16 17 pm3.2i ⊢ ( 2o ∈ ω ∧ 1o ∈ ω )
31 eqid ⊢ ( { 1o , 2o } Sat∈ ( 2o ∈𝑔 1o ) ) = ( { 1o , 2o } Sat∈ ( 2o ∈𝑔 1o ) )
32 31 sategoelfvb ⊢ ( ( { 1o , 2o } ∈ V ∧ ( 2o ∈ ω ∧ 1o ∈ ω ) ) → ( 𝑆 ∈ ( { 1o , 2o } Sat∈ ( 2o ∈𝑔 1o ) ) ↔ ( 𝑆 ∈ ( { 1o , 2o } ↑m ω ) ∧ ( 𝑆 ‘ 2o ) ∈ ( 𝑆 ‘ 1o ) ) ) )
33 9 30 32 mp2an ⊢ ( 𝑆 ∈ ( { 1o , 2o } Sat∈ ( 2o ∈𝑔 1o ) ) ↔ ( 𝑆 ∈ ( { 1o , 2o } ↑m ω ) ∧ ( 𝑆 ‘ 2o ) ∈ ( 𝑆 ‘ 1o ) ) )
34 29 33 mpbir ⊢ 𝑆 ∈ ( { 1o , 2o } Sat∈ ( 2o ∈𝑔 1o ) )