Metamath Proof Explorer

Theorem satf0suc

Description: The value of the satisfaction predicate as function over wff codes in the empty model and the empty binary relation at a successor. (Contributed by AV, 19-Sep-2023)

Ref Expression
Hypothesis satf0suc.s 
|- S = ( (/) Sat (/) )
Assertion satf0suc 
|- ( N e. _om -> ( S ` suc N ) = ( ( S ` N ) u. { <. x , y >. | ( y = (/) /\ E. u e. ( S ` N ) ( E. v e. ( S ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) )

Proof

Step Hyp Ref Expression
1 satf0suc.s 
 |-  S = ( (/) Sat (/) )
2 1 fveq1i 
 |-  ( S ` suc N ) = ( ( (/) Sat (/) ) ` suc N )
3 2 a1i 
 |-  ( N e. _om -> ( S ` suc N ) = ( ( (/) Sat (/) ) ` suc N ) )
4 omsucelsucb 
 |-  ( N e. _om <-> suc N e. suc _om )
5 satf0sucom 
 |-  ( suc N e. suc _om -> ( ( (/) Sat (/) ) ` suc N ) = ( rec ( ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) , { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) ` suc N ) )
6 4 5 sylbi 
 |-  ( N e. _om -> ( ( (/) Sat (/) ) ` suc N ) = ( rec ( ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) , { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) ` suc N ) )
7 nnon 
 |-  ( N e. _om -> N e. On )
8 rdgsuc 
 |-  ( N e. On -> ( rec ( ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) , { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) ` suc N ) = ( ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) ` ( rec ( ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) , { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) ` N ) ) )
9 7 8 syl 
 |-  ( N e. _om -> ( rec ( ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) , { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) ` suc N ) = ( ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) ` ( rec ( ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) , { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) ` N ) ) )
10 elelsuc 
 |-  ( N e. _om -> N e. suc _om )
11 satf0sucom 
 |-  ( N e. suc _om -> ( ( (/) Sat (/) ) ` N ) = ( rec ( ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) , { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) ` N ) )
12 10 11 syl 
 |-  ( N e. _om -> ( ( (/) Sat (/) ) ` N ) = ( rec ( ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) , { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) ` N ) )
13 1 eqcomi 
 |-  ( (/) Sat (/) ) = S
14 13 fveq1i 
 |-  ( ( (/) Sat (/) ) ` N ) = ( S ` N )
15 12 14 eqtr3di 
 |-  ( N e. _om -> ( rec ( ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) , { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) ` N ) = ( S ` N ) )
16 15 fveq2d 
 |-  ( N e. _om -> ( ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) ` ( rec ( ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) , { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) ` N ) ) = ( ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) ` ( S ` N ) ) )
17 eqidd 
 |-  ( N e. _om -> ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) = ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) )
18 id 
 |-  ( f = ( S ` N ) -> f = ( S ` N ) )
19 rexeq 
 |-  ( f = ( S ` N ) -> ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) <-> E. v e. ( S ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) ) )
20 19 orbi1d 
 |-  ( f = ( S ` N ) -> ( ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) <-> ( E. v e. ( S ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) )
21 20 rexeqbi1dv 
 |-  ( f = ( S ` N ) -> ( E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) <-> E. u e. ( S ` N ) ( E. v e. ( S ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) )
22 21 anbi2d 
 |-  ( f = ( S ` N ) -> ( ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) <-> ( y = (/) /\ E. u e. ( S ` N ) ( E. v e. ( S ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) ) )
23 22 opabbidv 
 |-  ( f = ( S ` N ) -> { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } = { <. x , y >. | ( y = (/) /\ E. u e. ( S ` N ) ( E. v e. ( S ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } )
24 18 23 uneq12d 
 |-  ( f = ( S ` N ) -> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) = ( ( S ` N ) u. { <. x , y >. | ( y = (/) /\ E. u e. ( S ` N ) ( E. v e. ( S ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) )
25 24 adantl 
 |-  ( ( N e. _om /\ f = ( S ` N ) ) -> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) = ( ( S ` N ) u. { <. x , y >. | ( y = (/) /\ E. u e. ( S ` N ) ( E. v e. ( S ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) )
26 fvex 
 |-  ( S ` N ) e. _V
27 26 a1i 
 |-  ( N e. _om -> ( S ` N ) e. _V )
28 omex 
 |-  _om e. _V
29 satf0suclem 
 |-  ( ( ( S ` N ) e. _V /\ ( S ` N ) e. _V /\ _om e. _V ) -> { <. x , y >. | ( y = (/) /\ E. u e. ( S ` N ) ( E. v e. ( S ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } e. _V )
30 26 26 28 29 mp3an 
 |-  { <. x , y >. | ( y = (/) /\ E. u e. ( S ` N ) ( E. v e. ( S ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } e. _V
31 26 30 unex 
 |-  ( ( S ` N ) u. { <. x , y >. | ( y = (/) /\ E. u e. ( S ` N ) ( E. v e. ( S ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) e. _V
32 31 a1i 
 |-  ( N e. _om -> ( ( S ` N ) u. { <. x , y >. | ( y = (/) /\ E. u e. ( S ` N ) ( E. v e. ( S ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) e. _V )
33 17 25 27 32 fvmptd 
 |-  ( N e. _om -> ( ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) ` ( S ` N ) ) = ( ( S ` N ) u. { <. x , y >. | ( y = (/) /\ E. u e. ( S ` N ) ( E. v e. ( S ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) )
34 9 16 33 3eqtrd 
 |-  ( N e. _om -> ( rec ( ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) , { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) ` suc N ) = ( ( S ` N ) u. { <. x , y >. | ( y = (/) /\ E. u e. ( S ` N ) ( E. v e. ( S ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) )
35 3 6 34 3eqtrd 
 |-  ( N e. _om -> ( S ` suc N ) = ( ( S ` N ) u. { <. x , y >. | ( y = (/) /\ E. u e. ( S ` N ) ( E. v e. ( S ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) )