Metamath Proof Explorer

Theorem sate0fv0

Description: A simplified satisfaction predicate as function over wff codes over an empty model is an empty set. (Contributed by AV, 31-Oct-2023)

Ref Expression
Assertion sate0fv0 
|- ( U e. ( Fmla ` _om ) -> ( S e. ( (/) SatE U ) -> S = (/) ) )

Proof

Step Hyp Ref Expression
1 0ex 
 |-  (/) e. _V
2 satef 
 |-  ( ( (/) e. _V /\ U e. ( Fmla ` _om ) /\ S e. ( (/) SatE U ) ) -> S : _om --> (/) )
3 1 2 mp3an1 
 |-  ( ( U e. ( Fmla ` _om ) /\ S e. ( (/) SatE U ) ) -> S : _om --> (/) )
4 3 ex 
 |-  ( U e. ( Fmla ` _om ) -> ( S e. ( (/) SatE U ) -> S : _om --> (/) ) )
5 f00 
 |-  ( S : _om --> (/) <-> ( S = (/) /\ _om = (/) ) )
6 5 simplbi 
 |-  ( S : _om --> (/) -> S = (/) )
7 4 6 syl6 
 |-  ( U e. ( Fmla ` _om ) -> ( S e. ( (/) SatE U ) -> S = (/) ) )