Metamath Proof Explorer

Theorem satfsschain

Description: The binary relation of a satisfaction predicate as function over wff codes is an increasing chain (with respect to inclusion). (Contributed by AV, 15-Oct-2023)

Ref Expression
Hypothesis satfsschain.s 
|- S = ( M Sat E )
Assertion satfsschain 
|- ( ( ( M e. V /\ E e. W ) /\ ( A e. _om /\ B e. _om ) ) -> ( B C_ A -> ( S ` B ) C_ ( S ` A ) ) )

Proof

Step Hyp Ref Expression
1 satfsschain.s 
 |-  S = ( M Sat E )
2 fveq2 
 |-  ( b = B -> ( S ` b ) = ( S ` B ) )
3 2 sseq2d 
 |-  ( b = B -> ( ( S ` B ) C_ ( S ` b ) <-> ( S ` B ) C_ ( S ` B ) ) )
4 3 imbi2d 
 |-  ( b = B -> ( ( ( M e. V /\ E e. W ) -> ( S ` B ) C_ ( S ` b ) ) <-> ( ( M e. V /\ E e. W ) -> ( S ` B ) C_ ( S ` B ) ) ) )
5 fveq2 
 |-  ( b = a -> ( S ` b ) = ( S ` a ) )
6 5 sseq2d 
 |-  ( b = a -> ( ( S ` B ) C_ ( S ` b ) <-> ( S ` B ) C_ ( S ` a ) ) )
7 6 imbi2d 
 |-  ( b = a -> ( ( ( M e. V /\ E e. W ) -> ( S ` B ) C_ ( S ` b ) ) <-> ( ( M e. V /\ E e. W ) -> ( S ` B ) C_ ( S ` a ) ) ) )
8 fveq2 
 |-  ( b = suc a -> ( S ` b ) = ( S ` suc a ) )
9 8 sseq2d 
 |-  ( b = suc a -> ( ( S ` B ) C_ ( S ` b ) <-> ( S ` B ) C_ ( S ` suc a ) ) )
10 9 imbi2d 
 |-  ( b = suc a -> ( ( ( M e. V /\ E e. W ) -> ( S ` B ) C_ ( S ` b ) ) <-> ( ( M e. V /\ E e. W ) -> ( S ` B ) C_ ( S ` suc a ) ) ) )
11 fveq2 
 |-  ( b = A -> ( S ` b ) = ( S ` A ) )
12 11 sseq2d 
 |-  ( b = A -> ( ( S ` B ) C_ ( S ` b ) <-> ( S ` B ) C_ ( S ` A ) ) )
13 12 imbi2d 
 |-  ( b = A -> ( ( ( M e. V /\ E e. W ) -> ( S ` B ) C_ ( S ` b ) ) <-> ( ( M e. V /\ E e. W ) -> ( S ` B ) C_ ( S ` A ) ) ) )
14 ssidd 
 |-  ( ( M e. V /\ E e. W ) -> ( S ` B ) C_ ( S ` B ) )
15 14 a1i 
 |-  ( B e. _om -> ( ( M e. V /\ E e. W ) -> ( S ` B ) C_ ( S ` B ) ) )
16 pm2.27 
 |-  ( ( M e. V /\ E e. W ) -> ( ( ( M e. V /\ E e. W ) -> ( S ` B ) C_ ( S ` a ) ) -> ( S ` B ) C_ ( S ` a ) ) )
17 16 adantl 
 |-  ( ( ( ( a e. _om /\ B e. _om ) /\ B C_ a ) /\ ( M e. V /\ E e. W ) ) -> ( ( ( M e. V /\ E e. W ) -> ( S ` B ) C_ ( S ` a ) ) -> ( S ` B ) C_ ( S ` a ) ) )
18 simpr 
 |-  ( ( ( ( ( a e. _om /\ B e. _om ) /\ B C_ a ) /\ ( M e. V /\ E e. W ) ) /\ ( S ` B ) C_ ( S ` a ) ) -> ( S ` B ) C_ ( S ` a ) )
19 ssun1 
 |-  ( S ` a ) C_ ( ( S ` a ) u. { <. x , y >. | E. u e. ( S ` a ) ( E. v e. ( S ` a ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { z e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( z |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } )
20 simpl 
 |-  ( ( M e. V /\ E e. W ) -> M e. V )
21 simpr 
 |-  ( ( M e. V /\ E e. W ) -> E e. W )
22 simplll 
 |-  ( ( ( ( a e. _om /\ B e. _om ) /\ B C_ a ) /\ ( M e. V /\ E e. W ) ) -> a e. _om )
23 1 satfvsuc 
 |-  ( ( M e. V /\ E e. W /\ a e. _om ) -> ( S ` suc a ) = ( ( S ` a ) u. { <. x , y >. | E. u e. ( S ` a ) ( E. v e. ( S ` a ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { z e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( z |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) )
24 20 21 22 23 syl2an23an 
 |-  ( ( ( ( a e. _om /\ B e. _om ) /\ B C_ a ) /\ ( M e. V /\ E e. W ) ) -> ( S ` suc a ) = ( ( S ` a ) u. { <. x , y >. | E. u e. ( S ` a ) ( E. v e. ( S ` a ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { z e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( z |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) )
25 19 24 sseqtrrid 
 |-  ( ( ( ( a e. _om /\ B e. _om ) /\ B C_ a ) /\ ( M e. V /\ E e. W ) ) -> ( S ` a ) C_ ( S ` suc a ) )
26 25 adantr 
 |-  ( ( ( ( ( a e. _om /\ B e. _om ) /\ B C_ a ) /\ ( M e. V /\ E e. W ) ) /\ ( S ` B ) C_ ( S ` a ) ) -> ( S ` a ) C_ ( S ` suc a ) )
27 18 26 sstrd 
 |-  ( ( ( ( ( a e. _om /\ B e. _om ) /\ B C_ a ) /\ ( M e. V /\ E e. W ) ) /\ ( S ` B ) C_ ( S ` a ) ) -> ( S ` B ) C_ ( S ` suc a ) )
28 27 ex 
 |-  ( ( ( ( a e. _om /\ B e. _om ) /\ B C_ a ) /\ ( M e. V /\ E e. W ) ) -> ( ( S ` B ) C_ ( S ` a ) -> ( S ` B ) C_ ( S ` suc a ) ) )
29 17 28 syld 
 |-  ( ( ( ( a e. _om /\ B e. _om ) /\ B C_ a ) /\ ( M e. V /\ E e. W ) ) -> ( ( ( M e. V /\ E e. W ) -> ( S ` B ) C_ ( S ` a ) ) -> ( S ` B ) C_ ( S ` suc a ) ) )
30 29 ex 
 |-  ( ( ( a e. _om /\ B e. _om ) /\ B C_ a ) -> ( ( M e. V /\ E e. W ) -> ( ( ( M e. V /\ E e. W ) -> ( S ` B ) C_ ( S ` a ) ) -> ( S ` B ) C_ ( S ` suc a ) ) ) )
31 30 com23 
 |-  ( ( ( a e. _om /\ B e. _om ) /\ B C_ a ) -> ( ( ( M e. V /\ E e. W ) -> ( S ` B ) C_ ( S ` a ) ) -> ( ( M e. V /\ E e. W ) -> ( S ` B ) C_ ( S ` suc a ) ) ) )
32 4 7 10 13 15 31 findsg 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ B C_ A ) -> ( ( M e. V /\ E e. W ) -> ( S ` B ) C_ ( S ` A ) ) )
33 32 ex 
 |-  ( ( A e. _om /\ B e. _om ) -> ( B C_ A -> ( ( M e. V /\ E e. W ) -> ( S ` B ) C_ ( S ` A ) ) ) )
34 33 com23 
 |-  ( ( A e. _om /\ B e. _om ) -> ( ( M e. V /\ E e. W ) -> ( B C_ A -> ( S ` B ) C_ ( S ` A ) ) ) )
35 34 impcom 
 |-  ( ( ( M e. V /\ E e. W ) /\ ( A e. _om /\ B e. _om ) ) -> ( B C_ A -> ( S ` B ) C_ ( S ` A ) ) )