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 ⊢ 𝐸 = ( 𝑀 Sat∈ ( 𝐴 ∈𝑔 𝐵 ) )
ex-sategoelel.s ⊢ 𝑆 = ( 𝑥 ∈ ω ↦ if ( 𝑥 = 𝐴 , 𝑍 , if ( 𝑥 = 𝐵 , 𝒫 𝑍 , ∅ ) ) )
Assertion ex-sategoelel ( ( ( 𝑀 ∈ WUni ∧ 𝑍 ∈ 𝑀 ) ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐴 ≠ 𝐵 ) ) → 𝑆 ∈ 𝐸 )

Proof

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