This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ex-sategoel

Description: Instance of sategoelfv for the 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-sategoel ( ( ( 𝑀 ∈ WUni ∧ 𝑍 ∈ 𝑀 ) ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐴 ≠ 𝐵 ) ) → ( 𝑆 ‘ 𝐴 ) ∈ ( 𝑆 ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 sategoelfvb.s ⊢ 𝐸 = ( 𝑀 Sat∈ ( 𝐴 ∈𝑔 𝐵 ) )
2 ex-sategoelel.s ⊢ 𝑆 = ( 𝑥 ∈ ω ↦ if ( 𝑥 = 𝐴 , 𝑍 , if ( 𝑥 = 𝐵 , 𝒫 𝑍 , ∅ ) ) )
3 simpll ⊢ ( ( ( 𝑀 ∈ WUni ∧ 𝑍 ∈ 𝑀 ) ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐴 ≠ 𝐵 ) ) → 𝑀 ∈ WUni )
4 3simpa ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐴 ≠ 𝐵 ) → ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) )
5 4 adantl ⊢ ( ( ( 𝑀 ∈ WUni ∧ 𝑍 ∈ 𝑀 ) ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐴 ≠ 𝐵 ) ) → ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) )
6 1 2 ex-sategoelel ⊢ ( ( ( 𝑀 ∈ WUni ∧ 𝑍 ∈ 𝑀 ) ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐴 ≠ 𝐵 ) ) → 𝑆 ∈ 𝐸 )
7 1 sategoelfv ⊢ ( ( 𝑀 ∈ WUni ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝑆 ∈ 𝐸 ) → ( 𝑆 ‘ 𝐴 ) ∈ ( 𝑆 ‘ 𝐵 ) )
8 3 5 6 7 syl3anc ⊢ ( ( ( 𝑀 ∈ WUni ∧ 𝑍 ∈ 𝑀 ) ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐴 ≠ 𝐵 ) ) → ( 𝑆 ‘ 𝐴 ) ∈ ( 𝑆 ‘ 𝐵 ) )