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 ⊢ U ∈ V → ∅ Sat ∈ U = ∅ Sat ∅ ⁡ ω ⁡ U

Proof

Step Hyp Ref Expression
1 0ex ⊢ ∅ ∈ V
2 satefv ⊢ ∅ ∈ V ∧ U ∈ V → ∅ Sat ∈ U = ∅ Sat E ∩ ∅ × ∅ ⁡ ω ⁡ U
3 1 2 mpan ⊢ U ∈ V → ∅ Sat ∈ U = ∅ Sat E ∩ ∅ × ∅ ⁡ ω ⁡ U
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 ∩ ∅ × ∅ ⁡ ω ⁡ U = ∅ Sat ∅ ⁡ ω ⁡ U
11 3 10 eqtrdi ⊢ U ∈ V → ∅ Sat ∈ U = ∅ Sat ∅ ⁡ ω ⁡ U