Metamath Proof Explorer

Theorem satfrel

Description: The value of the satisfaction predicate as function over wff codes at a natural number is a relation. (Contributed by AV, 12-Oct-2023)

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

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( a = (/) -> ( ( M Sat E ) ` a ) = ( ( M Sat E ) ` (/) ) )
2 1 releqd 
 |-  ( a = (/) -> ( Rel ( ( M Sat E ) ` a ) <-> Rel ( ( M Sat E ) ` (/) ) ) )
3 2 imbi2d 
 |-  ( a = (/) -> ( ( ( M e. V /\ E e. W ) -> Rel ( ( M Sat E ) ` a ) ) <-> ( ( M e. V /\ E e. W ) -> Rel ( ( M Sat E ) ` (/) ) ) ) )
4 fveq2 
 |-  ( a = b -> ( ( M Sat E ) ` a ) = ( ( M Sat E ) ` b ) )
5 4 releqd 
 |-  ( a = b -> ( Rel ( ( M Sat E ) ` a ) <-> Rel ( ( M Sat E ) ` b ) ) )
6 5 imbi2d 
 |-  ( a = b -> ( ( ( M e. V /\ E e. W ) -> Rel ( ( M Sat E ) ` a ) ) <-> ( ( M e. V /\ E e. W ) -> Rel ( ( M Sat E ) ` b ) ) ) )
7 fveq2 
 |-  ( a = suc b -> ( ( M Sat E ) ` a ) = ( ( M Sat E ) ` suc b ) )
8 7 releqd 
 |-  ( a = suc b -> ( Rel ( ( M Sat E ) ` a ) <-> Rel ( ( M Sat E ) ` suc b ) ) )
9 8 imbi2d 
 |-  ( a = suc b -> ( ( ( M e. V /\ E e. W ) -> Rel ( ( M Sat E ) ` a ) ) <-> ( ( M e. V /\ E e. W ) -> Rel ( ( M Sat E ) ` suc b ) ) ) )
10 fveq2 
 |-  ( a = N -> ( ( M Sat E ) ` a ) = ( ( M Sat E ) ` N ) )
11 10 releqd 
 |-  ( a = N -> ( Rel ( ( M Sat E ) ` a ) <-> Rel ( ( M Sat E ) ` N ) ) )
12 11 imbi2d 
 |-  ( a = N -> ( ( ( M e. V /\ E e. W ) -> Rel ( ( M Sat E ) ` a ) ) <-> ( ( M e. V /\ E e. W ) -> Rel ( ( M Sat E ) ` N ) ) ) )
13 relopabv 
 |-  Rel { <. x , y >. | E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) }
14 eqid 
 |-  ( M Sat E ) = ( M Sat E )
15 14 satfv0 
 |-  ( ( M e. V /\ E e. W ) -> ( ( M Sat E ) ` (/) ) = { <. x , y >. | E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) } )
16 15 releqd 
 |-  ( ( M e. V /\ E e. W ) -> ( Rel ( ( M Sat E ) ` (/) ) <-> Rel { <. x , y >. | E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) } ) )
17 13 16 mpbiri 
 |-  ( ( M e. V /\ E e. W ) -> Rel ( ( M Sat E ) ` (/) ) )
18 pm2.27 
 |-  ( ( M e. V /\ E e. W ) -> ( ( ( M e. V /\ E e. W ) -> Rel ( ( M Sat E ) ` b ) ) -> Rel ( ( M Sat E ) ` b ) ) )
19 simpr 
 |-  ( ( ( ( M e. V /\ E e. W ) /\ b e. _om ) /\ Rel ( ( M Sat E ) ` b ) ) -> Rel ( ( M Sat E ) ` b ) )
20 relopabv 
 |-  Rel { <. x , y >. | E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( 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 = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) }
21 relun 
 |-  ( Rel ( ( ( M Sat E ) ` b ) u. { <. x , y >. | E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( 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 = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) <-> ( Rel ( ( M Sat E ) ` b ) /\ Rel { <. x , y >. | E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( 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 = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) )
22 19 20 21 sylanblrc 
 |-  ( ( ( ( M e. V /\ E e. W ) /\ b e. _om ) /\ Rel ( ( M Sat E ) ` b ) ) -> Rel ( ( ( M Sat E ) ` b ) u. { <. x , y >. | E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( 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 = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) )
23 14 satfvsuc 
 |-  ( ( M e. V /\ E e. W /\ b e. _om ) -> ( ( M Sat E ) ` suc b ) = ( ( ( M Sat E ) ` b ) u. { <. x , y >. | E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( 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 = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) )
24 23 ad4ant123 
 |-  ( ( ( ( M e. V /\ E e. W ) /\ b e. _om ) /\ Rel ( ( M Sat E ) ` b ) ) -> ( ( M Sat E ) ` suc b ) = ( ( ( M Sat E ) ` b ) u. { <. x , y >. | E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( 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 = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) )
25 24 releqd 
 |-  ( ( ( ( M e. V /\ E e. W ) /\ b e. _om ) /\ Rel ( ( M Sat E ) ` b ) ) -> ( Rel ( ( M Sat E ) ` suc b ) <-> Rel ( ( ( M Sat E ) ` b ) u. { <. x , y >. | E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( 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 = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) ) )
26 22 25 mpbird 
 |-  ( ( ( ( M e. V /\ E e. W ) /\ b e. _om ) /\ Rel ( ( M Sat E ) ` b ) ) -> Rel ( ( M Sat E ) ` suc b ) )
27 26 exp31 
 |-  ( ( M e. V /\ E e. W ) -> ( b e. _om -> ( Rel ( ( M Sat E ) ` b ) -> Rel ( ( M Sat E ) ` suc b ) ) ) )
28 27 com23 
 |-  ( ( M e. V /\ E e. W ) -> ( Rel ( ( M Sat E ) ` b ) -> ( b e. _om -> Rel ( ( M Sat E ) ` suc b ) ) ) )
29 18 28 syld 
 |-  ( ( M e. V /\ E e. W ) -> ( ( ( M e. V /\ E e. W ) -> Rel ( ( M Sat E ) ` b ) ) -> ( b e. _om -> Rel ( ( M Sat E ) ` suc b ) ) ) )
30 29 com13 
 |-  ( b e. _om -> ( ( ( M e. V /\ E e. W ) -> Rel ( ( M Sat E ) ` b ) ) -> ( ( M e. V /\ E e. W ) -> Rel ( ( M Sat E ) ` suc b ) ) ) )
31 3 6 9 12 17 30 finds 
 |-  ( N e. _om -> ( ( M e. V /\ E e. W ) -> Rel ( ( M Sat E ) ` N ) ) )
32 31 com12 
 |-  ( ( M e. V /\ E e. W ) -> ( N e. _om -> Rel ( ( M Sat E ) ` N ) ) )
33 32 3impia 
 |-  ( ( M e. V /\ E e. W /\ N e. _om ) -> Rel ( ( M Sat E ) ` N ) )