Metamath Proof Explorer


Theorem satef

Description: The simplified satisfaction predicate as function over wff codes over an empty model. (Contributed by AV, 30-Oct-2023)

Ref Expression
Assertion satef M V U Fmla ω S M Sat U S : ω M

Proof

Step Hyp Ref Expression
1 satefv M V U Fmla ω M Sat U = M Sat E M × M ω U
2 1 eleq2d M V U Fmla ω S M Sat U S M Sat E M × M ω U
3 simpl M V U Fmla ω M V
4 incom E M × M = M × M E
5 sqxpexg M V M × M V
6 5 adantr M V U Fmla ω M × M V
7 inex1g M × M V M × M E V
8 6 7 syl M V U Fmla ω M × M E V
9 4 8 eqeltrid M V U Fmla ω E M × M V
10 3 9 jca M V U Fmla ω M V E M × M V
11 10 adantr M V U Fmla ω S M Sat E M × M ω U M V E M × M V
12 simpr M V U Fmla ω U Fmla ω
13 12 adantr M V U Fmla ω S M Sat E M × M ω U U Fmla ω
14 simpr M V U Fmla ω S M Sat E M × M ω U S M Sat E M × M ω U
15 11 13 14 3jca M V U Fmla ω S M Sat E M × M ω U M V E M × M V U Fmla ω S M Sat E M × M ω U
16 15 ex M V U Fmla ω S M Sat E M × M ω U M V E M × M V U Fmla ω S M Sat E M × M ω U
17 2 16 sylbid M V U Fmla ω S M Sat U M V E M × M V U Fmla ω S M Sat E M × M ω U
18 17 3impia M V U Fmla ω S M Sat U M V E M × M V U Fmla ω S M Sat E M × M ω U
19 satfvel M V E M × M V U Fmla ω S M Sat E M × M ω U S : ω M
20 18 19 syl M V U Fmla ω S M Sat U S : ω M