Metamath Proof Explorer

Theorem satf00

Description: The value of the satisfaction predicate as function over wff codes in the empty model with an empty binary relation at (/) . (Contributed by AV, 14-Sep-2023)

Ref Expression
Assertion satf00 
|- ( ( (/) Sat (/) ) ` (/) ) = { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) }

Proof

Step Hyp Ref Expression
1 peano1 
 |-  (/) e. _om
2 elelsuc 
 |-  ( (/) e. _om -> (/) e. suc _om )
3 satf0sucom 
 |-  ( (/) e. suc _om -> ( ( (/) Sat (/) ) ` (/) ) = ( 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 ) ) } ) ` (/) ) )
4 1 2 3 mp2b 
 |-  ( ( (/) Sat (/) ) ` (/) ) = ( 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 ) ) } ) ` (/) )
5 omex 
 |-  _om e. _V
6 5 5 xpex 
 |-  ( _om X. _om ) e. _V
7 xpexg 
 |-  ( ( _om e. _V /\ ( _om X. _om ) e. _V ) -> ( _om X. ( _om X. _om ) ) e. _V )
8 simpl 
 |-  ( ( _om e. _V /\ ( _om X. _om ) e. _V ) -> _om e. _V )
9 goelel3xp 
 |-  ( ( i e. _om /\ j e. _om ) -> ( i e.g j ) e. ( _om X. ( _om X. _om ) ) )
10 eleq1 
 |-  ( x = ( i e.g j ) -> ( x e. ( _om X. ( _om X. _om ) ) <-> ( i e.g j ) e. ( _om X. ( _om X. _om ) ) ) )
11 9 10 syl5ibrcom 
 |-  ( ( i e. _om /\ j e. _om ) -> ( x = ( i e.g j ) -> x e. ( _om X. ( _om X. _om ) ) ) )
12 11 rexlimivv 
 |-  ( E. i e. _om E. j e. _om x = ( i e.g j ) -> x e. ( _om X. ( _om X. _om ) ) )
13 12 ad2antll 
 |-  ( ( ( _om e. _V /\ ( _om X. _om ) e. _V ) /\ ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) ) -> x e. ( _om X. ( _om X. _om ) ) )
14 eleq1 
 |-  ( y = (/) -> ( y e. _om <-> (/) e. _om ) )
15 1 14 mpbiri 
 |-  ( y = (/) -> y e. _om )
16 15 ad2antrl 
 |-  ( ( ( _om e. _V /\ ( _om X. _om ) e. _V ) /\ ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) ) -> y e. _om )
17 7 8 13 16 opabex2 
 |-  ( ( _om e. _V /\ ( _om X. _om ) e. _V ) -> { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } e. _V )
18 5 6 17 mp2an 
 |-  { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } e. _V
19 18 rdg0 
 |-  ( 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 ) ) } ) ` (/) ) = { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) }
20 4 19 eqtri 
 |-  ( ( (/) Sat (/) ) ` (/) ) = { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) }