Metamath Proof Explorer

Theorem satf0n0

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

Ref Expression
Assertion satf0n0 
|- ( N e. _om -> (/) e/ ( ( (/) Sat (/) ) ` N ) )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( x = (/) -> ( ( (/) Sat (/) ) ` x ) = ( ( (/) Sat (/) ) ` (/) ) )
2 1 eleq2d 
 |-  ( x = (/) -> ( (/) e. ( ( (/) Sat (/) ) ` x ) <-> (/) e. ( ( (/) Sat (/) ) ` (/) ) ) )
3 2 notbid 
 |-  ( x = (/) -> ( -. (/) e. ( ( (/) Sat (/) ) ` x ) <-> -. (/) e. ( ( (/) Sat (/) ) ` (/) ) ) )
4 fveq2 
 |-  ( x = y -> ( ( (/) Sat (/) ) ` x ) = ( ( (/) Sat (/) ) ` y ) )
5 4 eleq2d 
 |-  ( x = y -> ( (/) e. ( ( (/) Sat (/) ) ` x ) <-> (/) e. ( ( (/) Sat (/) ) ` y ) ) )
6 5 notbid 
 |-  ( x = y -> ( -. (/) e. ( ( (/) Sat (/) ) ` x ) <-> -. (/) e. ( ( (/) Sat (/) ) ` y ) ) )
7 fveq2 
 |-  ( x = suc y -> ( ( (/) Sat (/) ) ` x ) = ( ( (/) Sat (/) ) ` suc y ) )
8 7 eleq2d 
 |-  ( x = suc y -> ( (/) e. ( ( (/) Sat (/) ) ` x ) <-> (/) e. ( ( (/) Sat (/) ) ` suc y ) ) )
9 8 notbid 
 |-  ( x = suc y -> ( -. (/) e. ( ( (/) Sat (/) ) ` x ) <-> -. (/) e. ( ( (/) Sat (/) ) ` suc y ) ) )
10 fveq2 
 |-  ( x = N -> ( ( (/) Sat (/) ) ` x ) = ( ( (/) Sat (/) ) ` N ) )
11 10 eleq2d 
 |-  ( x = N -> ( (/) e. ( ( (/) Sat (/) ) ` x ) <-> (/) e. ( ( (/) Sat (/) ) ` N ) ) )
12 11 notbid 
 |-  ( x = N -> ( -. (/) e. ( ( (/) Sat (/) ) ` x ) <-> -. (/) e. ( ( (/) Sat (/) ) ` N ) ) )
13 0nelopab 
 |-  -. (/) e. { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) }
14 satf00 
 |-  ( ( (/) Sat (/) ) ` (/) ) = { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) }
15 14 eleq2i 
 |-  ( (/) e. ( ( (/) Sat (/) ) ` (/) ) <-> (/) e. { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } )
16 13 15 mtbir 
 |-  -. (/) e. ( ( (/) Sat (/) ) ` (/) )
17 simpr 
 |-  ( ( y e. _om /\ -. (/) e. ( ( (/) Sat (/) ) ` y ) ) -> -. (/) e. ( ( (/) Sat (/) ) ` y ) )
18 0nelopab 
 |-  -. (/) e. { <. x , z >. | ( z = (/) /\ E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) }
19 ioran 
 |-  ( -. ( (/) e. ( ( (/) Sat (/) ) ` y ) \/ (/) e. { <. x , z >. | ( z = (/) /\ E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) <-> ( -. (/) e. ( ( (/) Sat (/) ) ` y ) /\ -. (/) e. { <. x , z >. | ( z = (/) /\ E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) )
20 17 18 19 sylanblrc 
 |-  ( ( y e. _om /\ -. (/) e. ( ( (/) Sat (/) ) ` y ) ) -> -. ( (/) e. ( ( (/) Sat (/) ) ` y ) \/ (/) e. { <. x , z >. | ( z = (/) /\ E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) )
21 eqid 
 |-  ( (/) Sat (/) ) = ( (/) Sat (/) )
22 21 satf0suc 
 |-  ( y e. _om -> ( ( (/) Sat (/) ) ` suc y ) = ( ( ( (/) Sat (/) ) ` y ) u. { <. x , z >. | ( z = (/) /\ E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) )
23 22 adantr 
 |-  ( ( y e. _om /\ -. (/) e. ( ( (/) Sat (/) ) ` y ) ) -> ( ( (/) Sat (/) ) ` suc y ) = ( ( ( (/) Sat (/) ) ` y ) u. { <. x , z >. | ( z = (/) /\ E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) )
24 23 eleq2d 
 |-  ( ( y e. _om /\ -. (/) e. ( ( (/) Sat (/) ) ` y ) ) -> ( (/) e. ( ( (/) Sat (/) ) ` suc y ) <-> (/) e. ( ( ( (/) Sat (/) ) ` y ) u. { <. x , z >. | ( z = (/) /\ E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) )
25 elun 
 |-  ( (/) e. ( ( ( (/) Sat (/) ) ` y ) u. { <. x , z >. | ( z = (/) /\ E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) <-> ( (/) e. ( ( (/) Sat (/) ) ` y ) \/ (/) e. { <. x , z >. | ( z = (/) /\ E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) )
26 24 25 bitrdi 
 |-  ( ( y e. _om /\ -. (/) e. ( ( (/) Sat (/) ) ` y ) ) -> ( (/) e. ( ( (/) Sat (/) ) ` suc y ) <-> ( (/) e. ( ( (/) Sat (/) ) ` y ) \/ (/) e. { <. x , z >. | ( z = (/) /\ E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) )
27 20 26 mtbird 
 |-  ( ( y e. _om /\ -. (/) e. ( ( (/) Sat (/) ) ` y ) ) -> -. (/) e. ( ( (/) Sat (/) ) ` suc y ) )
28 27 ex 
 |-  ( y e. _om -> ( -. (/) e. ( ( (/) Sat (/) ) ` y ) -> -. (/) e. ( ( (/) Sat (/) ) ` suc y ) ) )
29 3 6 9 12 16 28 finds 
 |-  ( N e. _om -> -. (/) e. ( ( (/) Sat (/) ) ` N ) )
30 df-nel 
 |-  ( (/) e/ ( ( (/) Sat (/) ) ` N ) <-> -. (/) e. ( ( (/) Sat (/) ) ` N ) )
31 29 30 sylibr 
 |-  ( N e. _om -> (/) e/ ( ( (/) Sat (/) ) ` N ) )