Metamath Proof Explorer

Theorem satefv

Description: The simplified satisfaction predicate as function over wff codes in the model M at the code U . (Contributed by AV, 30-Oct-2023)

Ref Expression
Assertion satefv ⊢ M ∈ V ∧ U ∈ W → M Sat ∈ U = M Sat E ∩ M × M ⁡ ω ⁡ U

Proof

Step Hyp Ref Expression
1 df-sate ⊢ Sat ∈ = m ∈ V , u ∈ V ⟼ m Sat E ∩ m × m ⁡ ω ⁡ u
2 1 a1i ⊢ M ∈ V ∧ U ∈ W → Sat ∈ = m ∈ V , u ∈ V ⟼ m Sat E ∩ m × m ⁡ ω ⁡ u
3 id ⊢ m = M → m = M
4 3 sqxpeqd ⊢ m = M → m × m = M × M
5 4 ineq2d ⊢ m = M → E ∩ m × m = E ∩ M × M
6 3 5 oveq12d ⊢ m = M → m Sat E ∩ m × m = M Sat E ∩ M × M
7 6 fveq1d ⊢ m = M → m Sat E ∩ m × m ⁡ ω = M Sat E ∩ M × M ⁡ ω
8 7 adantr ⊢ m = M ∧ u = U → m Sat E ∩ m × m ⁡ ω = M Sat E ∩ M × M ⁡ ω
9 simpr ⊢ m = M ∧ u = U → u = U
10 8 9 fveq12d ⊢ m = M ∧ u = U → m Sat E ∩ m × m ⁡ ω ⁡ u = M Sat E ∩ M × M ⁡ ω ⁡ U
11 10 adantl ⊢ M ∈ V ∧ U ∈ W ∧ m = M ∧ u = U → m Sat E ∩ m × m ⁡ ω ⁡ u = M Sat E ∩ M × M ⁡ ω ⁡ U
12 elex ⊢ M ∈ V → M ∈ V
13 12 adantr ⊢ M ∈ V ∧ U ∈ W → M ∈ V
14 elex ⊢ U ∈ W → U ∈ V
15 14 adantl ⊢ M ∈ V ∧ U ∈ W → U ∈ V
16 fvexd ⊢ M ∈ V ∧ U ∈ W → M Sat E ∩ M × M ⁡ ω ⁡ U ∈ V
17 2 11 13 15 16 ovmpod ⊢ M ∈ V ∧ U ∈ W → M Sat ∈ U = M Sat E ∩ M × M ⁡ ω ⁡ U