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