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

Metamath Proof Explorer

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 ∅ ) ‘ ω ) ‘ 𝑈 ) )