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 syl6bi
 |-  ( ( ( 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 ) )