Metamath Proof Explorer

Theorem satffun

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

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

Proof

Step Hyp Ref Expression
1 satfv0fun 
 |-  ( ( M e. V /\ E e. W ) -> Fun ( ( M Sat E ) ` (/) ) )
2 1 3adant3 
 |-  ( ( M e. V /\ E e. W /\ N e. _om ) -> Fun ( ( M Sat E ) ` (/) ) )
3 fveq2 
 |-  ( N = (/) -> ( ( M Sat E ) ` N ) = ( ( M Sat E ) ` (/) ) )
4 3 funeqd 
 |-  ( N = (/) -> ( Fun ( ( M Sat E ) ` N ) <-> Fun ( ( M Sat E ) ` (/) ) ) )
5 2 4 syl5ibr 
 |-  ( N = (/) -> ( ( M e. V /\ E e. W /\ N e. _om ) -> Fun ( ( M Sat E ) ` N ) ) )
6 df-ne 
 |-  ( N =/= (/) <-> -. N = (/) )
7 nnsuc 
 |-  ( ( N e. _om /\ N =/= (/) ) -> E. n e. _om N = suc n )
8 suceq 
 |-  ( x = (/) -> suc x = suc (/) )
9 8 fveq2d 
 |-  ( x = (/) -> ( ( M Sat E ) ` suc x ) = ( ( M Sat E ) ` suc (/) ) )
10 9 funeqd 
 |-  ( x = (/) -> ( Fun ( ( M Sat E ) ` suc x ) <-> Fun ( ( M Sat E ) ` suc (/) ) ) )
11 10 imbi2d 
 |-  ( x = (/) -> ( ( ( M e. V /\ E e. W ) -> Fun ( ( M Sat E ) ` suc x ) ) <-> ( ( M e. V /\ E e. W ) -> Fun ( ( M Sat E ) ` suc (/) ) ) ) )
12 suceq 
 |-  ( x = y -> suc x = suc y )
13 12 fveq2d 
 |-  ( x = y -> ( ( M Sat E ) ` suc x ) = ( ( M Sat E ) ` suc y ) )
14 13 funeqd 
 |-  ( x = y -> ( Fun ( ( M Sat E ) ` suc x ) <-> Fun ( ( M Sat E ) ` suc y ) ) )
15 14 imbi2d 
 |-  ( x = y -> ( ( ( M e. V /\ E e. W ) -> Fun ( ( M Sat E ) ` suc x ) ) <-> ( ( M e. V /\ E e. W ) -> Fun ( ( M Sat E ) ` suc y ) ) ) )
16 suceq 
 |-  ( x = suc y -> suc x = suc suc y )
17 16 fveq2d 
 |-  ( x = suc y -> ( ( M Sat E ) ` suc x ) = ( ( M Sat E ) ` suc suc y ) )
18 17 funeqd 
 |-  ( x = suc y -> ( Fun ( ( M Sat E ) ` suc x ) <-> Fun ( ( M Sat E ) ` suc suc y ) ) )
19 18 imbi2d 
 |-  ( x = suc y -> ( ( ( M e. V /\ E e. W ) -> Fun ( ( M Sat E ) ` suc x ) ) <-> ( ( M e. V /\ E e. W ) -> Fun ( ( M Sat E ) ` suc suc y ) ) ) )
20 suceq 
 |-  ( x = n -> suc x = suc n )
21 20 fveq2d 
 |-  ( x = n -> ( ( M Sat E ) ` suc x ) = ( ( M Sat E ) ` suc n ) )
22 21 funeqd 
 |-  ( x = n -> ( Fun ( ( M Sat E ) ` suc x ) <-> Fun ( ( M Sat E ) ` suc n ) ) )
23 22 imbi2d 
 |-  ( x = n -> ( ( ( M e. V /\ E e. W ) -> Fun ( ( M Sat E ) ` suc x ) ) <-> ( ( M e. V /\ E e. W ) -> Fun ( ( M Sat E ) ` suc n ) ) ) )
24 satffunlem1 
 |-  ( ( M e. V /\ E e. W ) -> Fun ( ( M Sat E ) ` suc (/) ) )
25 pm2.27 
 |-  ( ( M e. V /\ E e. W ) -> ( ( ( M e. V /\ E e. W ) -> Fun ( ( M Sat E ) ` suc y ) ) -> Fun ( ( M Sat E ) ` suc y ) ) )
26 satffunlem2 
 |-  ( ( y e. _om /\ ( M e. V /\ E e. W ) ) -> ( Fun ( ( M Sat E ) ` suc y ) -> Fun ( ( M Sat E ) ` suc suc y ) ) )
27 26 expcom 
 |-  ( ( M e. V /\ E e. W ) -> ( y e. _om -> ( Fun ( ( M Sat E ) ` suc y ) -> Fun ( ( M Sat E ) ` suc suc y ) ) ) )
28 27 com23 
 |-  ( ( M e. V /\ E e. W ) -> ( Fun ( ( M Sat E ) ` suc y ) -> ( y e. _om -> Fun ( ( M Sat E ) ` suc suc y ) ) ) )
29 25 28 syld 
 |-  ( ( M e. V /\ E e. W ) -> ( ( ( M e. V /\ E e. W ) -> Fun ( ( M Sat E ) ` suc y ) ) -> ( y e. _om -> Fun ( ( M Sat E ) ` suc suc y ) ) ) )
30 29 com13 
 |-  ( y e. _om -> ( ( ( M e. V /\ E e. W ) -> Fun ( ( M Sat E ) ` suc y ) ) -> ( ( M e. V /\ E e. W ) -> Fun ( ( M Sat E ) ` suc suc y ) ) ) )
31 11 15 19 23 24 30 finds 
 |-  ( n e. _om -> ( ( M e. V /\ E e. W ) -> Fun ( ( M Sat E ) ` suc n ) ) )
32 31 adantr 
 |-  ( ( n e. _om /\ N = suc n ) -> ( ( M e. V /\ E e. W ) -> Fun ( ( M Sat E ) ` suc n ) ) )
33 fveq2 
 |-  ( N = suc n -> ( ( M Sat E ) ` N ) = ( ( M Sat E ) ` suc n ) )
34 33 funeqd 
 |-  ( N = suc n -> ( Fun ( ( M Sat E ) ` N ) <-> Fun ( ( M Sat E ) ` suc n ) ) )
35 34 imbi2d 
 |-  ( N = suc n -> ( ( ( M e. V /\ E e. W ) -> Fun ( ( M Sat E ) ` N ) ) <-> ( ( M e. V /\ E e. W ) -> Fun ( ( M Sat E ) ` suc n ) ) ) )
36 35 adantl 
 |-  ( ( n e. _om /\ N = suc n ) -> ( ( ( M e. V /\ E e. W ) -> Fun ( ( M Sat E ) ` N ) ) <-> ( ( M e. V /\ E e. W ) -> Fun ( ( M Sat E ) ` suc n ) ) ) )
37 32 36 mpbird 
 |-  ( ( n e. _om /\ N = suc n ) -> ( ( M e. V /\ E e. W ) -> Fun ( ( M Sat E ) ` N ) ) )
38 37 rexlimiva 
 |-  ( E. n e. _om N = suc n -> ( ( M e. V /\ E e. W ) -> Fun ( ( M Sat E ) ` N ) ) )
39 7 38 syl 
 |-  ( ( N e. _om /\ N =/= (/) ) -> ( ( M e. V /\ E e. W ) -> Fun ( ( M Sat E ) ` N ) ) )
40 39 expcom 
 |-  ( N =/= (/) -> ( N e. _om -> ( ( M e. V /\ E e. W ) -> Fun ( ( M Sat E ) ` N ) ) ) )
41 6 40 sylbir 
 |-  ( -. N = (/) -> ( N e. _om -> ( ( M e. V /\ E e. W ) -> Fun ( ( M Sat E ) ` N ) ) ) )
42 41 com13 
 |-  ( ( M e. V /\ E e. W ) -> ( N e. _om -> ( -. N = (/) -> Fun ( ( M Sat E ) ` N ) ) ) )
43 42 3impia 
 |-  ( ( M e. V /\ E e. W /\ N e. _om ) -> ( -. N = (/) -> Fun ( ( M Sat E ) ` N ) ) )
44 43 com12 
 |-  ( -. N = (/) -> ( ( M e. V /\ E e. W /\ N e. _om ) -> Fun ( ( M Sat E ) ` N ) ) )
45 5 44 pm2.61i 
 |-  ( ( M e. V /\ E e. W /\ N e. _om ) -> Fun ( ( M Sat E ) ` N ) )