Metamath Proof Explorer

Theorem ex-sategoelel

Description: Example of a valuation of a simplified satisfaction predicate for a Godel-set of membership. (Contributed by AV, 5-Nov-2023)

Ref Expression
Hypotheses sategoelfvb.s ⊢ E = M Sat ∈ A ∈ 𝑔 B
ex-sategoelel.s ⊢ S = x ∈ ω ⟼ if x = A Z if x = B 𝒫 Z ∅
Assertion ex-sategoelel ⊢ M ∈ WUni ∧ Z ∈ M ∧ A ∈ ω ∧ B ∈ ω ∧ A ≠ B → S ∈ E

Proof

Step Hyp Ref Expression
1 sategoelfvb.s ⊢ E = M Sat ∈ A ∈ 𝑔 B
2 ex-sategoelel.s ⊢ S = x ∈ ω ⟼ if x = A Z if x = B 𝒫 Z ∅
3 simpr ⊢ M ∈ WUni ∧ Z ∈ M → Z ∈ M
4 simpl ⊢ M ∈ WUni ∧ Z ∈ M → M ∈ WUni
5 4 3 wunpw ⊢ M ∈ WUni ∧ Z ∈ M → 𝒫 Z ∈ M
6 4 wun0 ⊢ M ∈ WUni ∧ Z ∈ M → ∅ ∈ M
7 5 6 ifcld ⊢ M ∈ WUni ∧ Z ∈ M → if x = B 𝒫 Z ∅ ∈ M
8 3 7 ifcld ⊢ M ∈ WUni ∧ Z ∈ M → if x = A Z if x = B 𝒫 Z ∅ ∈ M
9 8 adantr ⊢ M ∈ WUni ∧ Z ∈ M ∧ A ∈ ω ∧ B ∈ ω ∧ A ≠ B → if x = A Z if x = B 𝒫 Z ∅ ∈ M
10 9 adantr ⊢ M ∈ WUni ∧ Z ∈ M ∧ A ∈ ω ∧ B ∈ ω ∧ A ≠ B ∧ x ∈ ω → if x = A Z if x = B 𝒫 Z ∅ ∈ M
11 10 2 fmptd ⊢ M ∈ WUni ∧ Z ∈ M ∧ A ∈ ω ∧ B ∈ ω ∧ A ≠ B → S : ω ⟶ M
12 4 adantr ⊢ M ∈ WUni ∧ Z ∈ M ∧ A ∈ ω ∧ B ∈ ω ∧ A ≠ B → M ∈ WUni
13 omex ⊢ ω ∈ V
14 13 a1i ⊢ M ∈ WUni ∧ Z ∈ M ∧ A ∈ ω ∧ B ∈ ω ∧ A ≠ B → ω ∈ V
15 12 14 elmapd ⊢ M ∈ WUni ∧ Z ∈ M ∧ A ∈ ω ∧ B ∈ ω ∧ A ≠ B → S ∈ M ω ↔ S : ω ⟶ M
16 11 15 mpbird ⊢ M ∈ WUni ∧ Z ∈ M ∧ A ∈ ω ∧ B ∈ ω ∧ A ≠ B → S ∈ M ω
17 pwidg ⊢ Z ∈ M → Z ∈ 𝒫 Z
18 17 adantl ⊢ M ∈ WUni ∧ Z ∈ M → Z ∈ 𝒫 Z
19 18 adantr ⊢ M ∈ WUni ∧ Z ∈ M ∧ A ∈ ω ∧ B ∈ ω ∧ A ≠ B → Z ∈ 𝒫 Z
20 2 a1i ⊢ M ∈ WUni ∧ Z ∈ M ∧ A ∈ ω ∧ B ∈ ω ∧ A ≠ B → S = x ∈ ω ⟼ if x = A Z if x = B 𝒫 Z ∅
21 iftrue ⊢ x = A → if x = A Z if x = B 𝒫 Z ∅ = Z
22 21 adantl ⊢ M ∈ WUni ∧ Z ∈ M ∧ A ∈ ω ∧ B ∈ ω ∧ A ≠ B ∧ x = A → if x = A Z if x = B 𝒫 Z ∅ = Z
23 simpr1 ⊢ M ∈ WUni ∧ Z ∈ M ∧ A ∈ ω ∧ B ∈ ω ∧ A ≠ B → A ∈ ω
24 3 adantr ⊢ M ∈ WUni ∧ Z ∈ M ∧ A ∈ ω ∧ B ∈ ω ∧ A ≠ B → Z ∈ M
25 20 22 23 24 fvmptd ⊢ M ∈ WUni ∧ Z ∈ M ∧ A ∈ ω ∧ B ∈ ω ∧ A ≠ B → S ⁡ A = Z
26 eqeq1 ⊢ x = B → x = A ↔ B = A
27 eqeq1 ⊢ x = B → x = B ↔ B = B
28 27 ifbid ⊢ x = B → if x = B 𝒫 Z ∅ = if B = B 𝒫 Z ∅
29 26 28 ifbieq2d ⊢ x = B → if x = A Z if x = B 𝒫 Z ∅ = if B = A Z if B = B 𝒫 Z ∅
30 necom ⊢ A ≠ B ↔ B ≠ A
31 ifnefalse ⊢ B ≠ A → if B = A Z if B = B 𝒫 Z ∅ = if B = B 𝒫 Z ∅
32 30 31 sylbi ⊢ A ≠ B → if B = A Z if B = B 𝒫 Z ∅ = if B = B 𝒫 Z ∅
33 32 3ad2ant3 ⊢ A ∈ ω ∧ B ∈ ω ∧ A ≠ B → if B = A Z if B = B 𝒫 Z ∅ = if B = B 𝒫 Z ∅
34 33 adantl ⊢ M ∈ WUni ∧ Z ∈ M ∧ A ∈ ω ∧ B ∈ ω ∧ A ≠ B → if B = A Z if B = B 𝒫 Z ∅ = if B = B 𝒫 Z ∅
35 29 34 sylan9eqr ⊢ M ∈ WUni ∧ Z ∈ M ∧ A ∈ ω ∧ B ∈ ω ∧ A ≠ B ∧ x = B → if x = A Z if x = B 𝒫 Z ∅ = if B = B 𝒫 Z ∅
36 simpr2 ⊢ M ∈ WUni ∧ Z ∈ M ∧ A ∈ ω ∧ B ∈ ω ∧ A ≠ B → B ∈ ω
37 pwexg ⊢ Z ∈ M → 𝒫 Z ∈ V
38 37 adantl ⊢ M ∈ WUni ∧ Z ∈ M → 𝒫 Z ∈ V
39 0ex ⊢ ∅ ∈ V
40 39 a1i ⊢ M ∈ WUni ∧ Z ∈ M → ∅ ∈ V
41 38 40 ifcld ⊢ M ∈ WUni ∧ Z ∈ M → if B = B 𝒫 Z ∅ ∈ V
42 41 adantr ⊢ M ∈ WUni ∧ Z ∈ M ∧ A ∈ ω ∧ B ∈ ω ∧ A ≠ B → if B = B 𝒫 Z ∅ ∈ V
43 20 35 36 42 fvmptd ⊢ M ∈ WUni ∧ Z ∈ M ∧ A ∈ ω ∧ B ∈ ω ∧ A ≠ B → S ⁡ B = if B = B 𝒫 Z ∅
44 eqid ⊢ B = B
45 44 iftruei ⊢ if B = B 𝒫 Z ∅ = 𝒫 Z
46 43 45 eqtrdi ⊢ M ∈ WUni ∧ Z ∈ M ∧ A ∈ ω ∧ B ∈ ω ∧ A ≠ B → S ⁡ B = 𝒫 Z
47 19 25 46 3eltr4d ⊢ M ∈ WUni ∧ Z ∈ M ∧ A ∈ ω ∧ B ∈ ω ∧ A ≠ B → S ⁡ A ∈ S ⁡ B
48 3simpa ⊢ A ∈ ω ∧ B ∈ ω ∧ A ≠ B → A ∈ ω ∧ B ∈ ω
49 1 sategoelfvb ⊢ M ∈ WUni ∧ A ∈ ω ∧ B ∈ ω → S ∈ E ↔ S ∈ M ω ∧ S ⁡ A ∈ S ⁡ B
50 4 48 49 syl2an ⊢ M ∈ WUni ∧ Z ∈ M ∧ A ∈ ω ∧ B ∈ ω ∧ A ≠ B → S ∈ E ↔ S ∈ M ω ∧ S ⁡ A ∈ S ⁡ B
51 16 47 50 mpbir2and ⊢ M ∈ WUni ∧ Z ∈ M ∧ A ∈ ω ∧ B ∈ ω ∧ A ≠ B → S ∈ E