This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 e. V -> ( (/) SatE U ) = ( ( ( (/) Sat (/) ) ` _om ) ` U ) )

Proof

Step Hyp Ref Expression
1 0ex 
 |-  (/) e. _V
2 satefv 
 |-  ( ( (/) e. _V /\ U e. V ) -> ( (/) SatE U ) = ( ( ( (/) Sat ( _E i^i ( (/) X. (/) ) ) ) ` _om ) ` U ) )
3 1 2 mpan 
 |-  ( U e. V -> ( (/) SatE U ) = ( ( ( (/) Sat ( _E i^i ( (/) X. (/) ) ) ) ` _om ) ` U ) )
4 xp0 
 |-  ( (/) X. (/) ) = (/)
5 4 ineq2i 
 |-  ( _E i^i ( (/) X. (/) ) ) = ( _E i^i (/) )
6 in0 
 |-  ( _E i^i (/) ) = (/)
7 5 6 eqtri 
 |-  ( _E i^i ( (/) X. (/) ) ) = (/)
8 7 oveq2i 
 |-  ( (/) Sat ( _E i^i ( (/) X. (/) ) ) ) = ( (/) Sat (/) )
9 8 fveq1i 
 |-  ( ( (/) Sat ( _E i^i ( (/) X. (/) ) ) ) ` _om ) = ( ( (/) Sat (/) ) ` _om )
10 9 fveq1i 
 |-  ( ( ( (/) Sat ( _E i^i ( (/) X. (/) ) ) ) ` _om ) ` U ) = ( ( ( (/) Sat (/) ) ` _om ) ` U )
11 3 10 eqtrdi 
 |-  ( U e. V -> ( (/) SatE U ) = ( ( ( (/) Sat (/) ) ` _om ) ` U ) )