Metamath Proof Explorer

Theorem satfv0

Description: The value of the satisfaction predicate as function over wff codes at (/) . (Contributed by AV, 8-Oct-2023)

Ref Expression
Hypothesis satfv0.s 
|- S = ( M Sat E )
Assertion satfv0 
|- ( ( M e. V /\ E e. W ) -> ( S ` (/) ) = { <. 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 ) } ) } )

Proof

Step Hyp Ref Expression
1 satfv0.s 
 |-  S = ( M Sat E )
2 peano1 
 |-  (/) e. _om
3 elelsuc 
 |-  ( (/) e. _om -> (/) e. suc _om )
4 2 3 mp1i 
 |-  ( ( M e. V /\ E e. W ) -> (/) e. suc _om )
5 1 satfvsucom 
 |-  ( ( M e. V /\ E e. W /\ (/) e. suc _om ) -> ( S ` (/) ) = ( rec ( ( f e. _V |-> ( f u. { <. x , y >. | E. u e. f ( E. v e. f ( 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 ) } ) ) } ) ) , { <. 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 ) } ) } ) ` (/) ) )
6 4 5 mpd3an3 
 |-  ( ( M e. V /\ E e. W ) -> ( S ` (/) ) = ( rec ( ( f e. _V |-> ( f u. { <. x , y >. | E. u e. f ( E. v e. f ( 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 ) } ) ) } ) ) , { <. 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 ) } ) } ) ` (/) ) )
7 goelel3xp 
 |-  ( ( i e. _om /\ j e. _om ) -> ( i e.g j ) e. ( _om X. ( _om X. _om ) ) )
8 eleq1 
 |-  ( x = ( i e.g j ) -> ( x e. ( _om X. ( _om X. _om ) ) <-> ( i e.g j ) e. ( _om X. ( _om X. _om ) ) ) )
9 7 8 syl5ibrcom 
 |-  ( ( i e. _om /\ j e. _om ) -> ( x = ( i e.g j ) -> x e. ( _om X. ( _om X. _om ) ) ) )
10 9 adantrd 
 |-  ( ( i e. _om /\ j e. _om ) -> ( ( x = ( i e.g j ) /\ y = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) -> x e. ( _om X. ( _om X. _om ) ) ) )
11 10 pm4.71d 
 |-  ( ( i e. _om /\ j e. _om ) -> ( ( x = ( i e.g j ) /\ y = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) <-> ( ( x = ( i e.g j ) /\ y = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) /\ x e. ( _om X. ( _om X. _om ) ) ) ) )
12 11 2rexbiia 
 |-  ( E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) <-> E. i e. _om E. j e. _om ( ( x = ( i e.g j ) /\ y = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) /\ x e. ( _om X. ( _om X. _om ) ) ) )
13 r19.41vv 
 |-  ( E. i e. _om E. j e. _om ( ( x = ( i e.g j ) /\ y = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) /\ x e. ( _om X. ( _om X. _om ) ) ) <-> ( E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) /\ x e. ( _om X. ( _om X. _om ) ) ) )
14 ancom 
 |-  ( ( E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) /\ x e. ( _om X. ( _om X. _om ) ) ) <-> ( x e. ( _om X. ( _om X. _om ) ) /\ E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) ) )
15 12 13 14 3bitri 
 |-  ( E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) <-> ( x e. ( _om X. ( _om X. _om ) ) /\ 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 opabbii 
 |-  { <. 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 ) } ) } = { <. x , y >. | ( x e. ( _om X. ( _om X. _om ) ) /\ 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 omex 
 |-  _om e. _V
18 17 17 xpex 
 |-  ( _om X. _om ) e. _V
19 xpexg 
 |-  ( ( _om e. _V /\ ( _om X. _om ) e. _V ) -> ( _om X. ( _om X. _om ) ) e. _V )
20 oveq1 
 |-  ( i = m -> ( i e.g j ) = ( m e.g j ) )
21 20 eqeq2d 
 |-  ( i = m -> ( x = ( i e.g j ) <-> x = ( m e.g j ) ) )
22 fveq2 
 |-  ( i = m -> ( a ` i ) = ( a ` m ) )
23 22 breq1d 
 |-  ( i = m -> ( ( a ` i ) E ( a ` j ) <-> ( a ` m ) E ( a ` j ) ) )
24 23 rabbidv 
 |-  ( i = m -> { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } = { a e. ( M ^m _om ) | ( a ` m ) E ( a ` j ) } )
25 24 eqeq2d 
 |-  ( i = m -> ( y = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } <-> y = { a e. ( M ^m _om ) | ( a ` m ) E ( a ` j ) } ) )
26 21 25 anbi12d 
 |-  ( i = m -> ( ( x = ( i e.g j ) /\ y = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) <-> ( x = ( m e.g j ) /\ y = { a e. ( M ^m _om ) | ( a ` m ) E ( a ` j ) } ) ) )
27 oveq2 
 |-  ( j = n -> ( m e.g j ) = ( m e.g n ) )
28 27 eqeq2d 
 |-  ( j = n -> ( x = ( m e.g j ) <-> x = ( m e.g n ) ) )
29 fveq2 
 |-  ( j = n -> ( a ` j ) = ( a ` n ) )
30 29 breq2d 
 |-  ( j = n -> ( ( a ` m ) E ( a ` j ) <-> ( a ` m ) E ( a ` n ) ) )
31 30 rabbidv 
 |-  ( j = n -> { a e. ( M ^m _om ) | ( a ` m ) E ( a ` j ) } = { a e. ( M ^m _om ) | ( a ` m ) E ( a ` n ) } )
32 31 eqeq2d 
 |-  ( j = n -> ( y = { a e. ( M ^m _om ) | ( a ` m ) E ( a ` j ) } <-> y = { a e. ( M ^m _om ) | ( a ` m ) E ( a ` n ) } ) )
33 28 32 anbi12d 
 |-  ( j = n -> ( ( x = ( m e.g j ) /\ y = { a e. ( M ^m _om ) | ( a ` m ) E ( a ` j ) } ) <-> ( x = ( m e.g n ) /\ y = { a e. ( M ^m _om ) | ( a ` m ) E ( a ` n ) } ) ) )
34 26 33 cbvrex2vw 
 |-  ( E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) <-> E. m e. _om E. n e. _om ( x = ( m e.g n ) /\ y = { a e. ( M ^m _om ) | ( a ` m ) E ( a ` n ) } ) )
35 eqeq1 
 |-  ( x = ( i e.g j ) -> ( x = ( m e.g n ) <-> ( i e.g j ) = ( m e.g n ) ) )
36 35 adantl 
 |-  ( ( ( ( m e. _om /\ n e. _om ) /\ ( i e. _om /\ j e. _om ) ) /\ x = ( i e.g j ) ) -> ( x = ( m e.g n ) <-> ( i e.g j ) = ( m e.g n ) ) )
37 goeleq12bg 
 |-  ( ( ( m e. _om /\ n e. _om ) /\ ( i e. _om /\ j e. _om ) ) -> ( ( i e.g j ) = ( m e.g n ) <-> ( i = m /\ j = n ) ) )
38 22 eqcomd 
 |-  ( i = m -> ( a ` m ) = ( a ` i ) )
39 29 eqcomd 
 |-  ( j = n -> ( a ` n ) = ( a ` j ) )
40 38 39 breqan12d 
 |-  ( ( i = m /\ j = n ) -> ( ( a ` m ) E ( a ` n ) <-> ( a ` i ) E ( a ` j ) ) )
41 40 rabbidv 
 |-  ( ( i = m /\ j = n ) -> { a e. ( M ^m _om ) | ( a ` m ) E ( a ` n ) } = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } )
42 37 41 syl6bi 
 |-  ( ( ( m e. _om /\ n e. _om ) /\ ( i e. _om /\ j e. _om ) ) -> ( ( i e.g j ) = ( m e.g n ) -> { a e. ( M ^m _om ) | ( a ` m ) E ( a ` n ) } = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) )
43 42 imp 
 |-  ( ( ( ( m e. _om /\ n e. _om ) /\ ( i e. _om /\ j e. _om ) ) /\ ( i e.g j ) = ( m e.g n ) ) -> { a e. ( M ^m _om ) | ( a ` m ) E ( a ` n ) } = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } )
44 eqeq12 
 |-  ( ( y = { a e. ( M ^m _om ) | ( a ` m ) E ( a ` n ) } /\ z = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) -> ( y = z <-> { a e. ( M ^m _om ) | ( a ` m ) E ( a ` n ) } = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) )
45 43 44 syl5ibrcom 
 |-  ( ( ( ( m e. _om /\ n e. _om ) /\ ( i e. _om /\ j e. _om ) ) /\ ( i e.g j ) = ( m e.g n ) ) -> ( ( y = { a e. ( M ^m _om ) | ( a ` m ) E ( a ` n ) } /\ z = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) -> y = z ) )
46 45 exp4b 
 |-  ( ( ( m e. _om /\ n e. _om ) /\ ( i e. _om /\ j e. _om ) ) -> ( ( i e.g j ) = ( m e.g n ) -> ( y = { a e. ( M ^m _om ) | ( a ` m ) E ( a ` n ) } -> ( z = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } -> y = z ) ) ) )
47 46 adantr 
 |-  ( ( ( ( m e. _om /\ n e. _om ) /\ ( i e. _om /\ j e. _om ) ) /\ x = ( i e.g j ) ) -> ( ( i e.g j ) = ( m e.g n ) -> ( y = { a e. ( M ^m _om ) | ( a ` m ) E ( a ` n ) } -> ( z = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } -> y = z ) ) ) )
48 36 47 sylbid 
 |-  ( ( ( ( m e. _om /\ n e. _om ) /\ ( i e. _om /\ j e. _om ) ) /\ x = ( i e.g j ) ) -> ( x = ( m e.g n ) -> ( y = { a e. ( M ^m _om ) | ( a ` m ) E ( a ` n ) } -> ( z = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } -> y = z ) ) ) )
49 48 impd 
 |-  ( ( ( ( m e. _om /\ n e. _om ) /\ ( i e. _om /\ j e. _om ) ) /\ x = ( i e.g j ) ) -> ( ( x = ( m e.g n ) /\ y = { a e. ( M ^m _om ) | ( a ` m ) E ( a ` n ) } ) -> ( z = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } -> y = z ) ) )
50 49 com23 
 |-  ( ( ( ( m e. _om /\ n e. _om ) /\ ( i e. _om /\ j e. _om ) ) /\ x = ( i e.g j ) ) -> ( z = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } -> ( ( x = ( m e.g n ) /\ y = { a e. ( M ^m _om ) | ( a ` m ) E ( a ` n ) } ) -> y = z ) ) )
51 50 expimpd 
 |-  ( ( ( m e. _om /\ n e. _om ) /\ ( i e. _om /\ j e. _om ) ) -> ( ( x = ( i e.g j ) /\ z = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) -> ( ( x = ( m e.g n ) /\ y = { a e. ( M ^m _om ) | ( a ` m ) E ( a ` n ) } ) -> y = z ) ) )
52 51 rexlimdvva 
 |-  ( ( m e. _om /\ n e. _om ) -> ( E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ z = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) -> ( ( x = ( m e.g n ) /\ y = { a e. ( M ^m _om ) | ( a ` m ) E ( a ` n ) } ) -> y = z ) ) )
53 52 com23 
 |-  ( ( m e. _om /\ n e. _om ) -> ( ( x = ( m e.g n ) /\ y = { a e. ( M ^m _om ) | ( a ` m ) E ( a ` n ) } ) -> ( E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ z = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) -> y = z ) ) )
54 53 rexlimivv 
 |-  ( E. m e. _om E. n e. _om ( x = ( m e.g n ) /\ y = { a e. ( M ^m _om ) | ( a ` m ) E ( a ` n ) } ) -> ( E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ z = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) -> y = z ) )
55 34 54 sylbi 
 |-  ( E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) -> ( E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ z = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) -> y = z ) )
56 55 imp 
 |-  ( ( E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) /\ E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ z = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) ) -> y = z )
57 56 gen2 
 |-  A. y A. z ( ( E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) /\ E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ z = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) ) -> y = z )
58 eqeq1 
 |-  ( y = z -> ( y = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } <-> z = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) )
59 58 anbi2d 
 |-  ( y = z -> ( ( x = ( i e.g j ) /\ y = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) <-> ( x = ( i e.g j ) /\ z = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) ) )
60 59 2rexbidv 
 |-  ( y = z -> ( E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) <-> E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ z = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) ) )
61 60 mo4 
 |-  ( E* 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 ) } ) <-> A. y A. z ( ( E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) /\ E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ z = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) ) -> y = z ) )
62 57 61 mpbir 
 |-  E* 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 ) } )
63 moabex 
 |-  ( E* 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 ) } ) -> { 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 ) } ) } e. _V )
64 62 63 mp1i 
 |-  ( ( ( _om e. _V /\ ( _om X. _om ) e. _V ) /\ x e. ( _om X. ( _om X. _om ) ) ) -> { 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 ) } ) } e. _V )
65 19 64 opabex3d 
 |-  ( ( _om e. _V /\ ( _om X. _om ) e. _V ) -> { <. x , y >. | ( x e. ( _om X. ( _om X. _om ) ) /\ E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) ) } e. _V )
66 17 18 65 mp2an 
 |-  { <. x , y >. | ( x e. ( _om X. ( _om X. _om ) ) /\ E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) ) } e. _V
67 16 66 eqeltri 
 |-  { <. 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 ) } ) } e. _V
68 67 rdg0 
 |-  ( rec ( ( f e. _V |-> ( f u. { <. x , y >. | E. u e. f ( E. v e. f ( 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 ) } ) ) } ) ) , { <. 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 ) } ) } ) ` (/) ) = { <. 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 ) } ) }
69 6 68 eqtrdi 
 |-  ( ( M e. V /\ E e. W ) -> ( S ` (/) ) = { <. 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 ) } ) } )