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 ∈ ω ⟼ if x = 2 𝑜 Z suc ⁡ Z
Assertion ex-sategoelelomsuc ⊢ Z ∈ ω → S ∈ ω Sat ∈ 2 𝑜 ∈ 𝑔 1 𝑜

Proof

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