Metamath Proof Explorer

Theorem satffunlem1

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

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

Proof

Step Hyp Ref Expression
1 satfv0fun 
 |-  ( ( M e. V /\ E e. W ) -> Fun ( ( M Sat E ) ` (/) ) )
2 satffunlem1lem1 
 |-  ( Fun ( ( M Sat E ) ` (/) ) -> Fun { <. x , y >. | E. u e. ( ( M Sat E ) ` (/) ) ( E. v e. ( ( M Sat E ) ` (/) ) ( 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 ) } ) ) } )
3 1 2 syl 
 |-  ( ( M e. V /\ E e. W ) -> Fun { <. x , y >. | E. u e. ( ( M Sat E ) ` (/) ) ( E. v e. ( ( M Sat E ) ` (/) ) ( 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 ) } ) ) } )
4 satffunlem1lem2 
 |-  ( ( M e. V /\ E e. W ) -> ( dom ( ( M Sat E ) ` (/) ) i^i dom { <. x , y >. | E. u e. ( ( M Sat E ) ` (/) ) ( E. v e. ( ( M Sat E ) ` (/) ) ( 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 ) } ) ) } ) = (/) )
5 funun 
 |-  ( ( ( Fun ( ( M Sat E ) ` (/) ) /\ Fun { <. x , y >. | E. u e. ( ( M Sat E ) ` (/) ) ( E. v e. ( ( M Sat E ) ` (/) ) ( 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 ) } ) ) } ) /\ ( dom ( ( M Sat E ) ` (/) ) i^i dom { <. x , y >. | E. u e. ( ( M Sat E ) ` (/) ) ( E. v e. ( ( M Sat E ) ` (/) ) ( 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 ) } ) ) } ) = (/) ) -> Fun ( ( ( M Sat E ) ` (/) ) u. { <. x , y >. | E. u e. ( ( M Sat E ) ` (/) ) ( E. v e. ( ( M Sat E ) ` (/) ) ( 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 ) } ) ) } ) )
6 1 3 4 5 syl21anc 
 |-  ( ( M e. V /\ E e. W ) -> Fun ( ( ( M Sat E ) ` (/) ) u. { <. x , y >. | E. u e. ( ( M Sat E ) ` (/) ) ( E. v e. ( ( M Sat E ) ` (/) ) ( 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 ) } ) ) } ) )
7 peano1 
 |-  (/) e. _om
8 eqid 
 |-  ( M Sat E ) = ( M Sat E )
9 8 satfvsuc 
 |-  ( ( M e. V /\ E e. W /\ (/) e. _om ) -> ( ( M Sat E ) ` suc (/) ) = ( ( ( M Sat E ) ` (/) ) u. { <. x , y >. | E. u e. ( ( M Sat E ) ` (/) ) ( E. v e. ( ( M Sat E ) ` (/) ) ( 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 ) } ) ) } ) )
10 7 9 mp3an3 
 |-  ( ( M e. V /\ E e. W ) -> ( ( M Sat E ) ` suc (/) ) = ( ( ( M Sat E ) ` (/) ) u. { <. x , y >. | E. u e. ( ( M Sat E ) ` (/) ) ( E. v e. ( ( M Sat E ) ` (/) ) ( 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 ) } ) ) } ) )
11 10 funeqd 
 |-  ( ( M e. V /\ E e. W ) -> ( Fun ( ( M Sat E ) ` suc (/) ) <-> Fun ( ( ( M Sat E ) ` (/) ) u. { <. x , y >. | E. u e. ( ( M Sat E ) ` (/) ) ( E. v e. ( ( M Sat E ) ` (/) ) ( 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 ) } ) ) } ) ) )
12 6 11 mpbird 
 |-  ( ( M e. V /\ E e. W ) -> Fun ( ( M Sat E ) ` suc (/) ) )