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 e. V /\ U e. ( Fmla ` _om ) /\ S e. ( M SatE U ) ) -> S : _om --> M )

Proof

Step Hyp Ref Expression
1 satefv 
 |-  ( ( M e. V /\ U e. ( Fmla ` _om ) ) -> ( M SatE U ) = ( ( ( M Sat ( _E i^i ( M X. M ) ) ) ` _om ) ` U ) )
2 1 eleq2d 
 |-  ( ( M e. V /\ U e. ( Fmla ` _om ) ) -> ( S e. ( M SatE U ) <-> S e. ( ( ( M Sat ( _E i^i ( M X. M ) ) ) ` _om ) ` U ) ) )
3 simpl 
 |-  ( ( M e. V /\ U e. ( Fmla ` _om ) ) -> M e. V )
4 incom 
 |-  ( _E i^i ( M X. M ) ) = ( ( M X. M ) i^i _E )
5 sqxpexg 
 |-  ( M e. V -> ( M X. M ) e. _V )
6 5 adantr 
 |-  ( ( M e. V /\ U e. ( Fmla ` _om ) ) -> ( M X. M ) e. _V )
7 inex1g 
 |-  ( ( M X. M ) e. _V -> ( ( M X. M ) i^i _E ) e. _V )
8 6 7 syl 
 |-  ( ( M e. V /\ U e. ( Fmla ` _om ) ) -> ( ( M X. M ) i^i _E ) e. _V )
9 4 8 eqeltrid 
 |-  ( ( M e. V /\ U e. ( Fmla ` _om ) ) -> ( _E i^i ( M X. M ) ) e. _V )
10 3 9 jca 
 |-  ( ( M e. V /\ U e. ( Fmla ` _om ) ) -> ( M e. V /\ ( _E i^i ( M X. M ) ) e. _V ) )
11 10 adantr 
 |-  ( ( ( M e. V /\ U e. ( Fmla ` _om ) ) /\ S e. ( ( ( M Sat ( _E i^i ( M X. M ) ) ) ` _om ) ` U ) ) -> ( M e. V /\ ( _E i^i ( M X. M ) ) e. _V ) )
12 simpr 
 |-  ( ( M e. V /\ U e. ( Fmla ` _om ) ) -> U e. ( Fmla ` _om ) )
13 12 adantr 
 |-  ( ( ( M e. V /\ U e. ( Fmla ` _om ) ) /\ S e. ( ( ( M Sat ( _E i^i ( M X. M ) ) ) ` _om ) ` U ) ) -> U e. ( Fmla ` _om ) )
14 simpr 
 |-  ( ( ( M e. V /\ U e. ( Fmla ` _om ) ) /\ S e. ( ( ( M Sat ( _E i^i ( M X. M ) ) ) ` _om ) ` U ) ) -> S e. ( ( ( M Sat ( _E i^i ( M X. M ) ) ) ` _om ) ` U ) )
15 11 13 14 3jca 
 |-  ( ( ( M e. V /\ U e. ( Fmla ` _om ) ) /\ S e. ( ( ( M Sat ( _E i^i ( M X. M ) ) ) ` _om ) ` U ) ) -> ( ( M e. V /\ ( _E i^i ( M X. M ) ) e. _V ) /\ U e. ( Fmla ` _om ) /\ S e. ( ( ( M Sat ( _E i^i ( M X. M ) ) ) ` _om ) ` U ) ) )
16 15 ex 
 |-  ( ( M e. V /\ U e. ( Fmla ` _om ) ) -> ( S e. ( ( ( M Sat ( _E i^i ( M X. M ) ) ) ` _om ) ` U ) -> ( ( M e. V /\ ( _E i^i ( M X. M ) ) e. _V ) /\ U e. ( Fmla ` _om ) /\ S e. ( ( ( M Sat ( _E i^i ( M X. M ) ) ) ` _om ) ` U ) ) ) )
17 2 16 sylbid 
 |-  ( ( M e. V /\ U e. ( Fmla ` _om ) ) -> ( S e. ( M SatE U ) -> ( ( M e. V /\ ( _E i^i ( M X. M ) ) e. _V ) /\ U e. ( Fmla ` _om ) /\ S e. ( ( ( M Sat ( _E i^i ( M X. M ) ) ) ` _om ) ` U ) ) ) )
18 17 3impia 
 |-  ( ( M e. V /\ U e. ( Fmla ` _om ) /\ S e. ( M SatE U ) ) -> ( ( M e. V /\ ( _E i^i ( M X. M ) ) e. _V ) /\ U e. ( Fmla ` _om ) /\ S e. ( ( ( M Sat ( _E i^i ( M X. M ) ) ) ` _om ) ` U ) ) )
19 satfvel 
 |-  ( ( ( M e. V /\ ( _E i^i ( M X. M ) ) e. _V ) /\ U e. ( Fmla ` _om ) /\ S e. ( ( ( M Sat ( _E i^i ( M X. M ) ) ) ` _om ) ` U ) ) -> S : _om --> M )
20 18 19 syl 
 |-  ( ( M e. V /\ U e. ( Fmla ` _om ) /\ S e. ( M SatE U ) ) -> S : _om --> M )