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 ∧ 𝑍 ∈ 𝑀 ) ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐴 ≠ 𝐵 ) ) → ( 𝑆 ‘ 𝐴 ) ∈ ( 𝑆 ‘ 𝐵 ) )