Metamath Proof Explorer

Theorem satfv0fun

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

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

Proof

Step Hyp Ref Expression
1 funopab 
 |-  ( Fun { <. x , y >. | E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) } <-> A. x E* y E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) )
2 oveq1 
 |-  ( i = k -> ( i e.g j ) = ( k e.g j ) )
3 2 eqeq2d 
 |-  ( i = k -> ( x = ( i e.g j ) <-> x = ( k e.g j ) ) )
4 fveq2 
 |-  ( i = k -> ( f ` i ) = ( f ` k ) )
5 4 breq1d 
 |-  ( i = k -> ( ( f ` i ) E ( f ` j ) <-> ( f ` k ) E ( f ` j ) ) )
6 5 rabbidv 
 |-  ( i = k -> { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } = { f e. ( M ^m _om ) | ( f ` k ) E ( f ` j ) } )
7 6 eqeq2d 
 |-  ( i = k -> ( y = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } <-> y = { f e. ( M ^m _om ) | ( f ` k ) E ( f ` j ) } ) )
8 3 7 anbi12d 
 |-  ( i = k -> ( ( x = ( i e.g j ) /\ y = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) <-> ( x = ( k e.g j ) /\ y = { f e. ( M ^m _om ) | ( f ` k ) E ( f ` j ) } ) ) )
9 oveq2 
 |-  ( j = l -> ( k e.g j ) = ( k e.g l ) )
10 9 eqeq2d 
 |-  ( j = l -> ( x = ( k e.g j ) <-> x = ( k e.g l ) ) )
11 fveq2 
 |-  ( j = l -> ( f ` j ) = ( f ` l ) )
12 11 breq2d 
 |-  ( j = l -> ( ( f ` k ) E ( f ` j ) <-> ( f ` k ) E ( f ` l ) ) )
13 12 rabbidv 
 |-  ( j = l -> { f e. ( M ^m _om ) | ( f ` k ) E ( f ` j ) } = { f e. ( M ^m _om ) | ( f ` k ) E ( f ` l ) } )
14 13 eqeq2d 
 |-  ( j = l -> ( y = { f e. ( M ^m _om ) | ( f ` k ) E ( f ` j ) } <-> y = { f e. ( M ^m _om ) | ( f ` k ) E ( f ` l ) } ) )
15 10 14 anbi12d 
 |-  ( j = l -> ( ( x = ( k e.g j ) /\ y = { f e. ( M ^m _om ) | ( f ` k ) E ( f ` j ) } ) <-> ( x = ( k e.g l ) /\ y = { f e. ( M ^m _om ) | ( f ` k ) E ( f ` l ) } ) ) )
16 8 15 cbvrex2vw 
 |-  ( E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) <-> E. k e. _om E. l e. _om ( x = ( k e.g l ) /\ y = { f e. ( M ^m _om ) | ( f ` k ) E ( f ` l ) } ) )
17 eqtr2 
 |-  ( ( x = ( i e.g j ) /\ x = ( k e.g l ) ) -> ( i e.g j ) = ( k e.g l ) )
18 goeleq12bg 
 |-  ( ( ( k e. _om /\ l e. _om ) /\ ( i e. _om /\ j e. _om ) ) -> ( ( i e.g j ) = ( k e.g l ) <-> ( i = k /\ j = l ) ) )
19 4 adantr 
 |-  ( ( i = k /\ j = l ) -> ( f ` i ) = ( f ` k ) )
20 19 eqcomd 
 |-  ( ( i = k /\ j = l ) -> ( f ` k ) = ( f ` i ) )
21 11 adantl 
 |-  ( ( i = k /\ j = l ) -> ( f ` j ) = ( f ` l ) )
22 21 eqcomd 
 |-  ( ( i = k /\ j = l ) -> ( f ` l ) = ( f ` j ) )
23 20 22 breq12d 
 |-  ( ( i = k /\ j = l ) -> ( ( f ` k ) E ( f ` l ) <-> ( f ` i ) E ( f ` j ) ) )
24 23 rabbidv 
 |-  ( ( i = k /\ j = l ) -> { f e. ( M ^m _om ) | ( f ` k ) E ( f ` l ) } = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } )
25 eqeq12 
 |-  ( ( y = { f e. ( M ^m _om ) | ( f ` k ) E ( f ` l ) } /\ z = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) -> ( y = z <-> { f e. ( M ^m _om ) | ( f ` k ) E ( f ` l ) } = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) )
26 24 25 syl5ibrcom 
 |-  ( ( i = k /\ j = l ) -> ( ( y = { f e. ( M ^m _om ) | ( f ` k ) E ( f ` l ) } /\ z = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) -> y = z ) )
27 26 expd 
 |-  ( ( i = k /\ j = l ) -> ( y = { f e. ( M ^m _om ) | ( f ` k ) E ( f ` l ) } -> ( z = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } -> y = z ) ) )
28 18 27 biimtrdi 
 |-  ( ( ( k e. _om /\ l e. _om ) /\ ( i e. _om /\ j e. _om ) ) -> ( ( i e.g j ) = ( k e.g l ) -> ( y = { f e. ( M ^m _om ) | ( f ` k ) E ( f ` l ) } -> ( z = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } -> y = z ) ) ) )
29 17 28 syl5 
 |-  ( ( ( k e. _om /\ l e. _om ) /\ ( i e. _om /\ j e. _om ) ) -> ( ( x = ( i e.g j ) /\ x = ( k e.g l ) ) -> ( y = { f e. ( M ^m _om ) | ( f ` k ) E ( f ` l ) } -> ( z = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } -> y = z ) ) ) )
30 29 expd 
 |-  ( ( ( k e. _om /\ l e. _om ) /\ ( i e. _om /\ j e. _om ) ) -> ( x = ( i e.g j ) -> ( x = ( k e.g l ) -> ( y = { f e. ( M ^m _om ) | ( f ` k ) E ( f ` l ) } -> ( z = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } -> y = z ) ) ) ) )
31 30 imp4a 
 |-  ( ( ( k e. _om /\ l e. _om ) /\ ( i e. _om /\ j e. _om ) ) -> ( x = ( i e.g j ) -> ( ( x = ( k e.g l ) /\ y = { f e. ( M ^m _om ) | ( f ` k ) E ( f ` l ) } ) -> ( z = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } -> y = z ) ) ) )
32 31 com34 
 |-  ( ( ( k e. _om /\ l e. _om ) /\ ( i e. _om /\ j e. _om ) ) -> ( x = ( i e.g j ) -> ( z = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } -> ( ( x = ( k e.g l ) /\ y = { f e. ( M ^m _om ) | ( f ` k ) E ( f ` l ) } ) -> y = z ) ) ) )
33 32 impd 
 |-  ( ( ( k e. _om /\ l e. _om ) /\ ( i e. _om /\ j e. _om ) ) -> ( ( x = ( i e.g j ) /\ z = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) -> ( ( x = ( k e.g l ) /\ y = { f e. ( M ^m _om ) | ( f ` k ) E ( f ` l ) } ) -> y = z ) ) )
34 33 rexlimdvva 
 |-  ( ( k e. _om /\ l e. _om ) -> ( E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ z = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) -> ( ( x = ( k e.g l ) /\ y = { f e. ( M ^m _om ) | ( f ` k ) E ( f ` l ) } ) -> y = z ) ) )
35 34 com23 
 |-  ( ( k e. _om /\ l e. _om ) -> ( ( x = ( k e.g l ) /\ y = { f e. ( M ^m _om ) | ( f ` k ) E ( f ` l ) } ) -> ( E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ z = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) -> y = z ) ) )
36 35 rexlimivv 
 |-  ( E. k e. _om E. l e. _om ( x = ( k e.g l ) /\ y = { f e. ( M ^m _om ) | ( f ` k ) E ( f ` l ) } ) -> ( E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ z = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) -> y = z ) )
37 16 36 sylbi 
 |-  ( E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) -> ( E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ z = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) -> y = z ) )
38 37 imp 
 |-  ( ( E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) /\ E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ z = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) ) -> y = z )
39 38 gen2 
 |-  A. y A. z ( ( E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) /\ E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ z = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) ) -> y = z )
40 eqeq1 
 |-  ( y = z -> ( y = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } <-> z = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) )
41 40 anbi2d 
 |-  ( y = z -> ( ( x = ( i e.g j ) /\ y = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) <-> ( x = ( i e.g j ) /\ z = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) ) )
42 41 2rexbidv 
 |-  ( y = z -> ( E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) <-> E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ z = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) ) )
43 42 mo4 
 |-  ( E* y E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) <-> A. y A. z ( ( E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) /\ E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ z = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) ) -> y = z ) )
44 39 43 mpbir 
 |-  E* y E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } )
45 1 44 mpgbir 
 |-  Fun { <. x , y >. | E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) }
46 eqid 
 |-  ( M Sat E ) = ( M Sat E )
47 46 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 = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) } )
48 47 funeqd 
 |-  ( ( M e. V /\ E e. W ) -> ( Fun ( ( M Sat E ) ` (/) ) <-> Fun { <. x , y >. | E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) } ) )
49 45 48 mpbiri 
 |-  ( ( M e. V /\ E e. W ) -> Fun ( ( M Sat E ) ` (/) ) )