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 ⊢ 𝑆 = ( 𝑥 ∈ ω ↦ if ( 𝑥 = 2o , 𝑍 , suc 𝑍 ) )
Assertion ex-sategoelelomsuc ( 𝑍 ∈ ω → 𝑆 ∈ ( ω Sat∈ ( 2o ∈𝑔 1o ) ) )

Proof

Step Hyp Ref Expression
1 ex-sategoelelomsuc.s ⊢ 𝑆 = ( 𝑥 ∈ ω ↦ if ( 𝑥 = 2o , 𝑍 , suc 𝑍 ) )
2 id ⊢ ( 𝑍 ∈ ω → 𝑍 ∈ ω )
3 peano2 ⊢ ( 𝑍 ∈ ω → suc 𝑍 ∈ ω )
4 2 3 ifcld ⊢ ( 𝑍 ∈ ω → if ( 𝑥 = 2o , 𝑍 , suc 𝑍 ) ∈ ω )
5 4 adantr ⊢ ( ( 𝑍 ∈ ω ∧ 𝑥 ∈ ω ) → if ( 𝑥 = 2o , 𝑍 , suc 𝑍 ) ∈ ω )
6 5 1 fmptd ⊢ ( 𝑍 ∈ ω → 𝑆 : ω ⟶ ω )
7 omex ⊢ ω ∈ V
8 7 a1i ⊢ ( 𝑍 ∈ ω → ω ∈ V )
9 8 8 elmapd ⊢ ( 𝑍 ∈ ω → ( 𝑆 ∈ ( ω ↑m ω ) ↔ 𝑆 : ω ⟶ ω ) )
10 6 9 mpbird ⊢ ( 𝑍 ∈ ω → 𝑆 ∈ ( ω ↑m ω ) )
11 sucidg ⊢ ( 𝑍 ∈ ω → 𝑍 ∈ suc 𝑍 )
12 1 a1i ⊢ ( 𝑍 ∈ ω → 𝑆 = ( 𝑥 ∈ ω ↦ if ( 𝑥 = 2o , 𝑍 , suc 𝑍 ) ) )
13 iftrue ⊢ ( 𝑥 = 2o → if ( 𝑥 = 2o , 𝑍 , suc 𝑍 ) = 𝑍 )
14 13 adantl ⊢ ( ( 𝑍 ∈ ω ∧ 𝑥 = 2o ) → if ( 𝑥 = 2o , 𝑍 , suc 𝑍 ) = 𝑍 )
15 2onn ⊢ 2o ∈ ω
16 15 a1i ⊢ ( 𝑍 ∈ ω → 2o ∈ ω )
17 12 14 16 2 fvmptd ⊢ ( 𝑍 ∈ ω → ( 𝑆 ‘ 2o ) = 𝑍 )
18 1one2o ⊢ 1o ≠ 2o
19 18 neii ⊢ ¬ 1o = 2o
20 eqeq1 ⊢ ( 𝑥 = 1o → ( 𝑥 = 2o ↔ 1o = 2o ) )
21 19 20 mtbiri ⊢ ( 𝑥 = 1o → ¬ 𝑥 = 2o )
22 21 iffalsed ⊢ ( 𝑥 = 1o → if ( 𝑥 = 2o , 𝑍 , suc 𝑍 ) = suc 𝑍 )
23 22 adantl ⊢ ( ( 𝑍 ∈ ω ∧ 𝑥 = 1o ) → if ( 𝑥 = 2o , 𝑍 , suc 𝑍 ) = suc 𝑍 )
24 1onn ⊢ 1o ∈ ω
25 24 a1i ⊢ ( 𝑍 ∈ ω → 1o ∈ ω )
26 12 23 25 3 fvmptd ⊢ ( 𝑍 ∈ ω → ( 𝑆 ‘ 1o ) = suc 𝑍 )
27 11 17 26 3eltr4d ⊢ ( 𝑍 ∈ ω → ( 𝑆 ‘ 2o ) ∈ ( 𝑆 ‘ 1o ) )
28 15 24 pm3.2i ⊢ ( 2o ∈ ω ∧ 1o ∈ ω )
29 7 28 pm3.2i ⊢ ( ω ∈ V ∧ ( 2o ∈ ω ∧ 1o ∈ ω ) )
30 eqid ⊢ ( ω Sat∈ ( 2o ∈𝑔 1o ) ) = ( ω Sat∈ ( 2o ∈𝑔 1o ) )
31 30 sategoelfvb ⊢ ( ( ω ∈ V ∧ ( 2o ∈ ω ∧ 1o ∈ ω ) ) → ( 𝑆 ∈ ( ω Sat∈ ( 2o ∈𝑔 1o ) ) ↔ ( 𝑆 ∈ ( ω ↑m ω ) ∧ ( 𝑆 ‘ 2o ) ∈ ( 𝑆 ‘ 1o ) ) ) )
32 29 31 mp1i ⊢ ( 𝑍 ∈ ω → ( 𝑆 ∈ ( ω Sat∈ ( 2o ∈𝑔 1o ) ) ↔ ( 𝑆 ∈ ( ω ↑m ω ) ∧ ( 𝑆 ‘ 2o ) ∈ ( 𝑆 ‘ 1o ) ) ) )
33 10 27 32 mpbir2and ⊢ ( 𝑍 ∈ ω → 𝑆 ∈ ( ω Sat∈ ( 2o ∈𝑔 1o ) ) )