Theorem sate0

Description: The simplified satisfaction predicate for any wff code over an empty model. (Contributed by AV, 6-Oct-2023) (Revised by AV, 5-Nov-2023)

	Ref	Expression
Assertion	sate0	⊢ ( 𝑈 ∈ 𝑉 → ( ∅ Sat∈ 𝑈 ) = ( ( ( ∅ Sat ∅ ) ‘ ω ) ‘ 𝑈 ) )

Proof

Step	Hyp	Ref	Expression
1		0ex	⊢ ∅ ∈ V
2		satefv	⊢ ( ( ∅ ∈ V ∧ 𝑈 ∈ 𝑉 ) → ( ∅ Sat∈ 𝑈 ) = ( ( ( ∅ Sat ( E ∩ ( ∅ × ∅ ) ) ) ‘ ω ) ‘ 𝑈 ) )
3	1 2	mpan	⊢ ( 𝑈 ∈ 𝑉 → ( ∅ Sat∈ 𝑈 ) = ( ( ( ∅ Sat ( E ∩ ( ∅ × ∅ ) ) ) ‘ ω ) ‘ 𝑈 ) )
4		xp0	⊢ ( ∅ × ∅ ) = ∅
5	4	ineq2i	⊢ ( E ∩ ( ∅ × ∅ ) ) = ( E ∩ ∅ )
6		in0	⊢ ( E ∩ ∅ ) = ∅
7	5 6	eqtri	⊢ ( E ∩ ( ∅ × ∅ ) ) = ∅
8	7	oveq2i	⊢ ( ∅ Sat ( E ∩ ( ∅ × ∅ ) ) ) = ( ∅ Sat ∅ )
9	8	fveq1i	⊢ ( ( ∅ Sat ( E ∩ ( ∅ × ∅ ) ) ) ‘ ω ) = ( ( ∅ Sat ∅ ) ‘ ω )
10	9	fveq1i	⊢ ( ( ( ∅ Sat ( E ∩ ( ∅ × ∅ ) ) ) ‘ ω ) ‘ 𝑈 ) = ( ( ( ∅ Sat ∅ ) ‘ ω ) ‘ 𝑈 )
11	3 10	eqtrdi	⊢ ( 𝑈 ∈ 𝑉 → ( ∅ Sat∈ 𝑈 ) = ( ( ( ∅ Sat ∅ ) ‘ ω ) ‘ 𝑈 ) )