Metamath Proof Explorer

Theorem satfun

Description: The satisfaction predicate as function over wff codes in the model M and the binary relation E on M . (Contributed by AV, 29-Oct-2023)

Ref Expression
Assertion satfun 
|- ( ( M e. V /\ E e. W ) -> ( ( M Sat E ) ` _om ) : ( Fmla ` _om ) --> ~P ( M ^m _om ) )

Proof

Step Hyp Ref Expression
1 satff 
 |-  ( ( M e. V /\ E e. W /\ x e. _om ) -> ( ( M Sat E ) ` x ) : ( Fmla ` x ) --> ~P ( M ^m _om ) )
2 1 3expa 
 |-  ( ( ( M e. V /\ E e. W ) /\ x e. _om ) -> ( ( M Sat E ) ` x ) : ( Fmla ` x ) --> ~P ( M ^m _om ) )
3 entric 
 |-  ( ( x e. _om /\ y e. _om ) -> ( x ~< y \/ x ~~ y \/ y ~< x ) )
4 3 adantl 
 |-  ( ( ( M e. V /\ E e. W ) /\ ( x e. _om /\ y e. _om ) ) -> ( x ~< y \/ x ~~ y \/ y ~< x ) )
5 nnsdomo 
 |-  ( ( x e. _om /\ y e. _om ) -> ( x ~< y <-> x C. y ) )
6 5 adantl 
 |-  ( ( ( M e. V /\ E e. W ) /\ ( x e. _om /\ y e. _om ) ) -> ( x ~< y <-> x C. y ) )
7 pm3.22 
 |-  ( ( x e. _om /\ y e. _om ) -> ( y e. _om /\ x e. _om ) )
8 7 anim2i 
 |-  ( ( ( M e. V /\ E e. W ) /\ ( x e. _om /\ y e. _om ) ) -> ( ( M e. V /\ E e. W ) /\ ( y e. _om /\ x e. _om ) ) )
9 pssss 
 |-  ( x C. y -> x C_ y )
10 eqid 
 |-  ( M Sat E ) = ( M Sat E )
11 10 satfsschain 
 |-  ( ( ( M e. V /\ E e. W ) /\ ( y e. _om /\ x e. _om ) ) -> ( x C_ y -> ( ( M Sat E ) ` x ) C_ ( ( M Sat E ) ` y ) ) )
12 11 imp 
 |-  ( ( ( ( M e. V /\ E e. W ) /\ ( y e. _om /\ x e. _om ) ) /\ x C_ y ) -> ( ( M Sat E ) ` x ) C_ ( ( M Sat E ) ` y ) )
13 8 9 12 syl2an 
 |-  ( ( ( ( M e. V /\ E e. W ) /\ ( x e. _om /\ y e. _om ) ) /\ x C. y ) -> ( ( M Sat E ) ` x ) C_ ( ( M Sat E ) ` y ) )
14 13 orcd 
 |-  ( ( ( ( M e. V /\ E e. W ) /\ ( x e. _om /\ y e. _om ) ) /\ x C. y ) -> ( ( ( M Sat E ) ` x ) C_ ( ( M Sat E ) ` y ) \/ ( ( M Sat E ) ` y ) C_ ( ( M Sat E ) ` x ) ) )
15 14 ex 
 |-  ( ( ( M e. V /\ E e. W ) /\ ( x e. _om /\ y e. _om ) ) -> ( x C. y -> ( ( ( M Sat E ) ` x ) C_ ( ( M Sat E ) ` y ) \/ ( ( M Sat E ) ` y ) C_ ( ( M Sat E ) ` x ) ) ) )
16 6 15 sylbid 
 |-  ( ( ( M e. V /\ E e. W ) /\ ( x e. _om /\ y e. _om ) ) -> ( x ~< y -> ( ( ( M Sat E ) ` x ) C_ ( ( M Sat E ) ` y ) \/ ( ( M Sat E ) ` y ) C_ ( ( M Sat E ) ` x ) ) ) )
17 nneneq 
 |-  ( ( x e. _om /\ y e. _om ) -> ( x ~~ y <-> x = y ) )
18 17 adantl 
 |-  ( ( ( M e. V /\ E e. W ) /\ ( x e. _om /\ y e. _om ) ) -> ( x ~~ y <-> x = y ) )
19 ssid 
 |-  ( ( M Sat E ) ` y ) C_ ( ( M Sat E ) ` y )
20 fveq2 
 |-  ( x = y -> ( ( M Sat E ) ` x ) = ( ( M Sat E ) ` y ) )
21 19 20 sseqtrrid 
 |-  ( x = y -> ( ( M Sat E ) ` y ) C_ ( ( M Sat E ) ` x ) )
22 21 olcd 
 |-  ( x = y -> ( ( ( M Sat E ) ` x ) C_ ( ( M Sat E ) ` y ) \/ ( ( M Sat E ) ` y ) C_ ( ( M Sat E ) ` x ) ) )
23 18 22 biimtrdi 
 |-  ( ( ( M e. V /\ E e. W ) /\ ( x e. _om /\ y e. _om ) ) -> ( x ~~ y -> ( ( ( M Sat E ) ` x ) C_ ( ( M Sat E ) ` y ) \/ ( ( M Sat E ) ` y ) C_ ( ( M Sat E ) ` x ) ) ) )
24 nnsdomo 
 |-  ( ( y e. _om /\ x e. _om ) -> ( y ~< x <-> y C. x ) )
25 24 ancoms 
 |-  ( ( x e. _om /\ y e. _om ) -> ( y ~< x <-> y C. x ) )
26 25 adantl 
 |-  ( ( ( M e. V /\ E e. W ) /\ ( x e. _om /\ y e. _om ) ) -> ( y ~< x <-> y C. x ) )
27 10 satfsschain 
 |-  ( ( ( M e. V /\ E e. W ) /\ ( x e. _om /\ y e. _om ) ) -> ( y C_ x -> ( ( M Sat E ) ` y ) C_ ( ( M Sat E ) ` x ) ) )
28 pssss 
 |-  ( y C. x -> y C_ x )
29 27 28 impel 
 |-  ( ( ( ( M e. V /\ E e. W ) /\ ( x e. _om /\ y e. _om ) ) /\ y C. x ) -> ( ( M Sat E ) ` y ) C_ ( ( M Sat E ) ` x ) )
30 29 olcd 
 |-  ( ( ( ( M e. V /\ E e. W ) /\ ( x e. _om /\ y e. _om ) ) /\ y C. x ) -> ( ( ( M Sat E ) ` x ) C_ ( ( M Sat E ) ` y ) \/ ( ( M Sat E ) ` y ) C_ ( ( M Sat E ) ` x ) ) )
31 30 ex 
 |-  ( ( ( M e. V /\ E e. W ) /\ ( x e. _om /\ y e. _om ) ) -> ( y C. x -> ( ( ( M Sat E ) ` x ) C_ ( ( M Sat E ) ` y ) \/ ( ( M Sat E ) ` y ) C_ ( ( M Sat E ) ` x ) ) ) )
32 26 31 sylbid 
 |-  ( ( ( M e. V /\ E e. W ) /\ ( x e. _om /\ y e. _om ) ) -> ( y ~< x -> ( ( ( M Sat E ) ` x ) C_ ( ( M Sat E ) ` y ) \/ ( ( M Sat E ) ` y ) C_ ( ( M Sat E ) ` x ) ) ) )
33 16 23 32 3jaod 
 |-  ( ( ( M e. V /\ E e. W ) /\ ( x e. _om /\ y e. _om ) ) -> ( ( x ~< y \/ x ~~ y \/ y ~< x ) -> ( ( ( M Sat E ) ` x ) C_ ( ( M Sat E ) ` y ) \/ ( ( M Sat E ) ` y ) C_ ( ( M Sat E ) ` x ) ) ) )
34 4 33 mpd 
 |-  ( ( ( M e. V /\ E e. W ) /\ ( x e. _om /\ y e. _om ) ) -> ( ( ( M Sat E ) ` x ) C_ ( ( M Sat E ) ` y ) \/ ( ( M Sat E ) ` y ) C_ ( ( M Sat E ) ` x ) ) )
35 34 expr 
 |-  ( ( ( M e. V /\ E e. W ) /\ x e. _om ) -> ( y e. _om -> ( ( ( M Sat E ) ` x ) C_ ( ( M Sat E ) ` y ) \/ ( ( M Sat E ) ` y ) C_ ( ( M Sat E ) ` x ) ) ) )
36 35 ralrimiv 
 |-  ( ( ( M e. V /\ E e. W ) /\ x e. _om ) -> A. y e. _om ( ( ( M Sat E ) ` x ) C_ ( ( M Sat E ) ` y ) \/ ( ( M Sat E ) ` y ) C_ ( ( M Sat E ) ` x ) ) )
37 2 36 jca 
 |-  ( ( ( M e. V /\ E e. W ) /\ x e. _om ) -> ( ( ( M Sat E ) ` x ) : ( Fmla ` x ) --> ~P ( M ^m _om ) /\ A. y e. _om ( ( ( M Sat E ) ` x ) C_ ( ( M Sat E ) ` y ) \/ ( ( M Sat E ) ` y ) C_ ( ( M Sat E ) ` x ) ) ) )
38 37 ralrimiva 
 |-  ( ( M e. V /\ E e. W ) -> A. x e. _om ( ( ( M Sat E ) ` x ) : ( Fmla ` x ) --> ~P ( M ^m _om ) /\ A. y e. _om ( ( ( M Sat E ) ` x ) C_ ( ( M Sat E ) ` y ) \/ ( ( M Sat E ) ` y ) C_ ( ( M Sat E ) ` x ) ) ) )
39 fvex 
 |-  ( ( M Sat E ) ` x ) e. _V
40 20 39 fiun 
 |-  ( A. x e. _om ( ( ( M Sat E ) ` x ) : ( Fmla ` x ) --> ~P ( M ^m _om ) /\ A. y e. _om ( ( ( M Sat E ) ` x ) C_ ( ( M Sat E ) ` y ) \/ ( ( M Sat E ) ` y ) C_ ( ( M Sat E ) ` x ) ) ) -> U_ x e. _om ( ( M Sat E ) ` x ) : U_ x e. _om ( Fmla ` x ) --> ~P ( M ^m _om ) )
41 38 40 syl 
 |-  ( ( M e. V /\ E e. W ) -> U_ x e. _om ( ( M Sat E ) ` x ) : U_ x e. _om ( Fmla ` x ) --> ~P ( M ^m _om ) )
42 satom 
 |-  ( ( M e. V /\ E e. W ) -> ( ( M Sat E ) ` _om ) = U_ x e. _om ( ( M Sat E ) ` x ) )
43 fmla 
 |-  ( Fmla ` _om ) = U_ x e. _om ( Fmla ` x )
44 43 a1i 
 |-  ( ( M e. V /\ E e. W ) -> ( Fmla ` _om ) = U_ x e. _om ( Fmla ` x ) )
45 42 44 feq12d 
 |-  ( ( M e. V /\ E e. W ) -> ( ( ( M Sat E ) ` _om ) : ( Fmla ` _om ) --> ~P ( M ^m _om ) <-> U_ x e. _om ( ( M Sat E ) ` x ) : U_ x e. _om ( Fmla ` x ) --> ~P ( M ^m _om ) ) )
46 41 45 mpbird 
 |-  ( ( M e. V /\ E e. W ) -> ( ( M Sat E ) ` _om ) : ( Fmla ` _om ) --> ~P ( M ^m _om ) )