Metamath Proof Explorer

Theorem satffunlem2

Description: Lemma 2 for satffun : induction step. (Contributed by AV, 28-Oct-2023)

Ref Expression
Assertion satffunlem2 
|- ( ( N e. _om /\ ( M e. V /\ E e. W ) ) -> ( Fun ( ( M Sat E ) ` suc N ) -> Fun ( ( M Sat E ) ` suc suc N ) ) )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( ( N e. _om /\ ( M e. V /\ E e. W ) ) /\ Fun ( ( M Sat E ) ` suc N ) ) -> Fun ( ( M Sat E ) ` suc N ) )
2 simpr 
 |-  ( ( N e. _om /\ ( M e. V /\ E e. W ) ) -> ( M e. V /\ E e. W ) )
3 peano2 
 |-  ( N e. _om -> suc N e. _om )
4 3 ancri 
 |-  ( N e. _om -> ( suc N e. _om /\ N e. _om ) )
5 4 adantr 
 |-  ( ( N e. _om /\ ( M e. V /\ E e. W ) ) -> ( suc N e. _om /\ N e. _om ) )
6 sssucid 
 |-  N C_ suc N
7 6 a1i 
 |-  ( ( N e. _om /\ ( M e. V /\ E e. W ) ) -> N C_ suc N )
8 eqid 
 |-  ( M Sat E ) = ( M Sat E )
9 8 satfsschain 
 |-  ( ( ( M e. V /\ E e. W ) /\ ( suc N e. _om /\ N e. _om ) ) -> ( N C_ suc N -> ( ( M Sat E ) ` N ) C_ ( ( M Sat E ) ` suc N ) ) )
10 9 imp 
 |-  ( ( ( ( M e. V /\ E e. W ) /\ ( suc N e. _om /\ N e. _om ) ) /\ N C_ suc N ) -> ( ( M Sat E ) ` N ) C_ ( ( M Sat E ) ` suc N ) )
11 2 5 7 10 syl21anc 
 |-  ( ( N e. _om /\ ( M e. V /\ E e. W ) ) -> ( ( M Sat E ) ` N ) C_ ( ( M Sat E ) ` suc N ) )
12 eqid 
 |-  ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) )
13 eqid 
 |-  { f e. ( M ^m _om ) | A. j e. M ( { <. i , j >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } = { f e. ( M ^m _om ) | A. j e. M ( { <. i , j >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) }
14 8 12 13 satffunlem2lem1 
 |-  ( ( Fun ( ( M Sat E ) ` suc N ) /\ ( ( M Sat E ) ` N ) C_ ( ( M Sat E ) ` suc N ) ) -> Fun { <. x , y >. | ( E. u e. ( ( ( M Sat E ) ` suc N ) \ ( ( M Sat E ) ` N ) ) ( E. v e. ( ( M Sat E ) ` suc N ) ( 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 = { f e. ( M ^m _om ) | A. j e. M ( { <. i , j >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) \/ E. u e. ( ( M Sat E ) ` N ) E. v e. ( ( ( M Sat E ) ` suc N ) \ ( ( M Sat E ) ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) ) } )
15 14 expcom 
 |-  ( ( ( M Sat E ) ` N ) C_ ( ( M Sat E ) ` suc N ) -> ( Fun ( ( M Sat E ) ` suc N ) -> Fun { <. x , y >. | ( E. u e. ( ( ( M Sat E ) ` suc N ) \ ( ( M Sat E ) ` N ) ) ( E. v e. ( ( M Sat E ) ` suc N ) ( 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 = { f e. ( M ^m _om ) | A. j e. M ( { <. i , j >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) \/ E. u e. ( ( M Sat E ) ` N ) E. v e. ( ( ( M Sat E ) ` suc N ) \ ( ( M Sat E ) ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) ) } ) )
16 11 15 syl 
 |-  ( ( N e. _om /\ ( M e. V /\ E e. W ) ) -> ( Fun ( ( M Sat E ) ` suc N ) -> Fun { <. x , y >. | ( E. u e. ( ( ( M Sat E ) ` suc N ) \ ( ( M Sat E ) ` N ) ) ( E. v e. ( ( M Sat E ) ` suc N ) ( 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 = { f e. ( M ^m _om ) | A. j e. M ( { <. i , j >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) \/ E. u e. ( ( M Sat E ) ` N ) E. v e. ( ( ( M Sat E ) ` suc N ) \ ( ( M Sat E ) ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) ) } ) )
17 16 imp 
 |-  ( ( ( N e. _om /\ ( M e. V /\ E e. W ) ) /\ Fun ( ( M Sat E ) ` suc N ) ) -> Fun { <. x , y >. | ( E. u e. ( ( ( M Sat E ) ` suc N ) \ ( ( M Sat E ) ` N ) ) ( E. v e. ( ( M Sat E ) ` suc N ) ( 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 = { f e. ( M ^m _om ) | A. j e. M ( { <. i , j >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) \/ E. u e. ( ( M Sat E ) ` N ) E. v e. ( ( ( M Sat E ) ` suc N ) \ ( ( M Sat E ) ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) ) } )
18 8 12 13 satffunlem2lem2 
 |-  ( ( ( N e. _om /\ ( M e. V /\ E e. W ) ) /\ Fun ( ( M Sat E ) ` suc N ) ) -> ( dom ( ( M Sat E ) ` suc N ) i^i dom { <. x , y >. | ( E. u e. ( ( ( M Sat E ) ` suc N ) \ ( ( M Sat E ) ` N ) ) ( E. v e. ( ( M Sat E ) ` suc N ) ( 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 = { f e. ( M ^m _om ) | A. j e. M ( { <. i , j >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) \/ E. u e. ( ( M Sat E ) ` N ) E. v e. ( ( ( M Sat E ) ` suc N ) \ ( ( M Sat E ) ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) ) } ) = (/) )
19 funun 
 |-  ( ( ( Fun ( ( M Sat E ) ` suc N ) /\ Fun { <. x , y >. | ( E. u e. ( ( ( M Sat E ) ` suc N ) \ ( ( M Sat E ) ` N ) ) ( E. v e. ( ( M Sat E ) ` suc N ) ( 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 = { f e. ( M ^m _om ) | A. j e. M ( { <. i , j >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) \/ E. u e. ( ( M Sat E ) ` N ) E. v e. ( ( ( M Sat E ) ` suc N ) \ ( ( M Sat E ) ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) ) } ) /\ ( dom ( ( M Sat E ) ` suc N ) i^i dom { <. x , y >. | ( E. u e. ( ( ( M Sat E ) ` suc N ) \ ( ( M Sat E ) ` N ) ) ( E. v e. ( ( M Sat E ) ` suc N ) ( 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 = { f e. ( M ^m _om ) | A. j e. M ( { <. i , j >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) \/ E. u e. ( ( M Sat E ) ` N ) E. v e. ( ( ( M Sat E ) ` suc N ) \ ( ( M Sat E ) ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) ) } ) = (/) ) -> Fun ( ( ( M Sat E ) ` suc N ) u. { <. x , y >. | ( E. u e. ( ( ( M Sat E ) ` suc N ) \ ( ( M Sat E ) ` N ) ) ( E. v e. ( ( M Sat E ) ` suc N ) ( 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 = { f e. ( M ^m _om ) | A. j e. M ( { <. i , j >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) \/ E. u e. ( ( M Sat E ) ` N ) E. v e. ( ( ( M Sat E ) ` suc N ) \ ( ( M Sat E ) ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) ) } ) )
20 1 17 18 19 syl21anc 
 |-  ( ( ( N e. _om /\ ( M e. V /\ E e. W ) ) /\ Fun ( ( M Sat E ) ` suc N ) ) -> Fun ( ( ( M Sat E ) ` suc N ) u. { <. x , y >. | ( E. u e. ( ( ( M Sat E ) ` suc N ) \ ( ( M Sat E ) ` N ) ) ( E. v e. ( ( M Sat E ) ` suc N ) ( 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 = { f e. ( M ^m _om ) | A. j e. M ( { <. i , j >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) \/ E. u e. ( ( M Sat E ) ` N ) E. v e. ( ( ( M Sat E ) ` suc N ) \ ( ( M Sat E ) ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) ) } ) )
21 simpl 
 |-  ( ( M e. V /\ E e. W ) -> M e. V )
22 simpr 
 |-  ( ( M e. V /\ E e. W ) -> E e. W )
23 simpl 
 |-  ( ( N e. _om /\ ( M e. V /\ E e. W ) ) -> N e. _om )
24 8 12 13 satfvsucsuc 
 |-  ( ( M e. V /\ E e. W /\ N e. _om ) -> ( ( M Sat E ) ` suc suc N ) = ( ( ( M Sat E ) ` suc N ) u. { <. x , y >. | ( E. u e. ( ( ( M Sat E ) ` suc N ) \ ( ( M Sat E ) ` N ) ) ( E. v e. ( ( M Sat E ) ` suc N ) ( 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 = { f e. ( M ^m _om ) | A. j e. M ( { <. i , j >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) \/ E. u e. ( ( M Sat E ) ` N ) E. v e. ( ( ( M Sat E ) ` suc N ) \ ( ( M Sat E ) ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) ) } ) )
25 21 22 23 24 syl2an23an 
 |-  ( ( N e. _om /\ ( M e. V /\ E e. W ) ) -> ( ( M Sat E ) ` suc suc N ) = ( ( ( M Sat E ) ` suc N ) u. { <. x , y >. | ( E. u e. ( ( ( M Sat E ) ` suc N ) \ ( ( M Sat E ) ` N ) ) ( E. v e. ( ( M Sat E ) ` suc N ) ( 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 = { f e. ( M ^m _om ) | A. j e. M ( { <. i , j >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) \/ E. u e. ( ( M Sat E ) ` N ) E. v e. ( ( ( M Sat E ) ` suc N ) \ ( ( M Sat E ) ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) ) } ) )
26 25 funeqd 
 |-  ( ( N e. _om /\ ( M e. V /\ E e. W ) ) -> ( Fun ( ( M Sat E ) ` suc suc N ) <-> Fun ( ( ( M Sat E ) ` suc N ) u. { <. x , y >. | ( E. u e. ( ( ( M Sat E ) ` suc N ) \ ( ( M Sat E ) ` N ) ) ( E. v e. ( ( M Sat E ) ` suc N ) ( 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 = { f e. ( M ^m _om ) | A. j e. M ( { <. i , j >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) \/ E. u e. ( ( M Sat E ) ` N ) E. v e. ( ( ( M Sat E ) ` suc N ) \ ( ( M Sat E ) ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) ) } ) ) )
27 26 adantr 
 |-  ( ( ( N e. _om /\ ( M e. V /\ E e. W ) ) /\ Fun ( ( M Sat E ) ` suc N ) ) -> ( Fun ( ( M Sat E ) ` suc suc N ) <-> Fun ( ( ( M Sat E ) ` suc N ) u. { <. x , y >. | ( E. u e. ( ( ( M Sat E ) ` suc N ) \ ( ( M Sat E ) ` N ) ) ( E. v e. ( ( M Sat E ) ` suc N ) ( 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 = { f e. ( M ^m _om ) | A. j e. M ( { <. i , j >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) \/ E. u e. ( ( M Sat E ) ` N ) E. v e. ( ( ( M Sat E ) ` suc N ) \ ( ( M Sat E ) ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) ) } ) ) )
28 20 27 mpbird 
 |-  ( ( ( N e. _om /\ ( M e. V /\ E e. W ) ) /\ Fun ( ( M Sat E ) ` suc N ) ) -> Fun ( ( M Sat E ) ` suc suc N ) )
29 28 ex 
 |-  ( ( N e. _om /\ ( M e. V /\ E e. W ) ) -> ( Fun ( ( M Sat E ) ` suc N ) -> Fun ( ( M Sat E ) ` suc suc N ) ) )