Metamath Proof Explorer

Theorem satfbrsuc

Description: The binary relation of a satisfaction predicate as function over wff codes at a successor. (Contributed by AV, 13-Oct-2023)

Ref Expression
Hypotheses satfbrsuc.s 
|- S = ( M Sat E )
satfbrsuc.p 
|- P = ( S ` N )
Assertion satfbrsuc 
|- ( ( ( M e. V /\ E e. W ) /\ N e. _om /\ ( A e. X /\ B e. Y ) ) -> ( A ( S ` suc N ) B <-> ( A P B \/ E. u e. P ( E. v e. P ( A = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ B = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( A = A.g i ( 1st ` u ) /\ B = { f e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) ) ) )

Proof

Step Hyp Ref Expression
1 satfbrsuc.s 
 |-  S = ( M Sat E )
2 satfbrsuc.p 
 |-  P = ( S ` N )
3 1 satfvsuc 
 |-  ( ( M e. V /\ E e. W /\ N e. _om ) -> ( S ` suc N ) = ( ( S ` N ) u. { <. x , y >. | E. u e. ( S ` N ) ( E. v e. ( S ` 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. z e. M ( { <. i , z >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) )
4 3 3expa 
 |-  ( ( ( M e. V /\ E e. W ) /\ N e. _om ) -> ( S ` suc N ) = ( ( S ` N ) u. { <. x , y >. | E. u e. ( S ` N ) ( E. v e. ( S ` 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. z e. M ( { <. i , z >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) )
5 4 3adant3 
 |-  ( ( ( M e. V /\ E e. W ) /\ N e. _om /\ ( A e. X /\ B e. Y ) ) -> ( S ` suc N ) = ( ( S ` N ) u. { <. x , y >. | E. u e. ( S ` N ) ( E. v e. ( S ` 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. z e. M ( { <. i , z >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) )
6 5 breqd 
 |-  ( ( ( M e. V /\ E e. W ) /\ N e. _om /\ ( A e. X /\ B e. Y ) ) -> ( A ( S ` suc N ) B <-> A ( ( S ` N ) u. { <. x , y >. | E. u e. ( S ` N ) ( E. v e. ( S ` 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. z e. M ( { <. i , z >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) B ) )
7 brun 
 |-  ( A ( ( S ` N ) u. { <. x , y >. | E. u e. ( S ` N ) ( E. v e. ( S ` 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. z e. M ( { <. i , z >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) B <-> ( A ( S ` N ) B \/ A { <. x , y >. | E. u e. ( S ` N ) ( E. v e. ( S ` 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. z e. M ( { <. i , z >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } B ) )
8 2 eqcomi 
 |-  ( S ` N ) = P
9 8 breqi 
 |-  ( A ( S ` N ) B <-> A P B )
10 9 a1i 
 |-  ( ( A e. X /\ B e. Y ) -> ( A ( S ` N ) B <-> A P B ) )
11 eqeq1 
 |-  ( x = A -> ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) <-> A = ( ( 1st ` u ) |g ( 1st ` v ) ) ) )
12 eqeq1 
 |-  ( y = B -> ( y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) <-> B = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) )
13 11 12 bi2anan9 
 |-  ( ( x = A /\ y = B ) -> ( ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) <-> ( A = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ B = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) ) )
14 13 rexbidv 
 |-  ( ( x = A /\ y = B ) -> ( E. v e. P ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) <-> E. v e. P ( A = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ B = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) ) )
15 eqeq1 
 |-  ( x = A -> ( x = A.g i ( 1st ` u ) <-> A = A.g i ( 1st ` u ) ) )
16 eqeq1 
 |-  ( y = B -> ( y = { f e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } <-> B = { f e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) )
17 15 16 bi2anan9 
 |-  ( ( x = A /\ y = B ) -> ( ( x = A.g i ( 1st ` u ) /\ y = { f e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) <-> ( A = A.g i ( 1st ` u ) /\ B = { f e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) )
18 17 rexbidv 
 |-  ( ( x = A /\ y = B ) -> ( E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { f e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) <-> E. i e. _om ( A = A.g i ( 1st ` u ) /\ B = { f e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) )
19 14 18 orbi12d 
 |-  ( ( x = A /\ y = B ) -> ( ( E. v e. P ( 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. z e. M ( { <. i , z >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) <-> ( E. v e. P ( A = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ B = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( A = A.g i ( 1st ` u ) /\ B = { f e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) ) )
20 19 rexbidv 
 |-  ( ( x = A /\ y = B ) -> ( E. u e. P ( E. v e. P ( 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. z e. M ( { <. i , z >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) <-> E. u e. P ( E. v e. P ( A = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ B = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( A = A.g i ( 1st ` u ) /\ B = { f e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) ) )
21 8 rexeqi 
 |-  ( E. v e. ( S ` N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) <-> E. v e. P ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) )
22 21 orbi1i 
 |-  ( ( E. v e. ( S ` 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. z e. M ( { <. i , z >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) <-> ( E. v e. P ( 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. z e. M ( { <. i , z >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) )
23 8 22 rexeqbii 
 |-  ( E. u e. ( S ` N ) ( E. v e. ( S ` 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. z e. M ( { <. i , z >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) <-> E. u e. P ( E. v e. P ( 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. z e. M ( { <. i , z >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) )
24 23 opabbii 
 |-  { <. x , y >. | E. u e. ( S ` N ) ( E. v e. ( S ` 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. z e. M ( { <. i , z >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } = { <. x , y >. | E. u e. P ( E. v e. P ( 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. z e. M ( { <. i , z >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) }
25 20 24 brabga 
 |-  ( ( A e. X /\ B e. Y ) -> ( A { <. x , y >. | E. u e. ( S ` N ) ( E. v e. ( S ` 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. z e. M ( { <. i , z >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } B <-> E. u e. P ( E. v e. P ( A = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ B = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( A = A.g i ( 1st ` u ) /\ B = { f e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) ) )
26 10 25 orbi12d 
 |-  ( ( A e. X /\ B e. Y ) -> ( ( A ( S ` N ) B \/ A { <. x , y >. | E. u e. ( S ` N ) ( E. v e. ( S ` 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. z e. M ( { <. i , z >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } B ) <-> ( A P B \/ E. u e. P ( E. v e. P ( A = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ B = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( A = A.g i ( 1st ` u ) /\ B = { f e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) ) ) )
27 7 26 syl5bb 
 |-  ( ( A e. X /\ B e. Y ) -> ( A ( ( S ` N ) u. { <. x , y >. | E. u e. ( S ` N ) ( E. v e. ( S ` 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. z e. M ( { <. i , z >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) B <-> ( A P B \/ E. u e. P ( E. v e. P ( A = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ B = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( A = A.g i ( 1st ` u ) /\ B = { f e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) ) ) )
28 27 3ad2ant3 
 |-  ( ( ( M e. V /\ E e. W ) /\ N e. _om /\ ( A e. X /\ B e. Y ) ) -> ( A ( ( S ` N ) u. { <. x , y >. | E. u e. ( S ` N ) ( E. v e. ( S ` 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. z e. M ( { <. i , z >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) B <-> ( A P B \/ E. u e. P ( E. v e. P ( A = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ B = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( A = A.g i ( 1st ` u ) /\ B = { f e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) ) ) )
29 6 28 bitrd 
 |-  ( ( ( M e. V /\ E e. W ) /\ N e. _om /\ ( A e. X /\ B e. Y ) ) -> ( A ( S ` suc N ) B <-> ( A P B \/ E. u e. P ( E. v e. P ( A = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ B = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( A = A.g i ( 1st ` u ) /\ B = { f e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) ) ) )