This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem satf0

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

Ref Expression
Assertion satf0 
|- ( (/) 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 ) ) } ) |` suc _om )

Proof

Step Hyp Ref Expression
1 0ex 
 |-  (/) e. _V
2 satf 
 |-  ( ( (/) e. _V /\ (/) e. _V ) -> ( (/) Sat (/) ) = ( rec ( ( f e. _V |-> ( f u. { <. x , y >. | E. u e. f ( E. v e. f ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( (/) ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( (/) ^m _om ) | A. z e. (/) ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) ) , { <. x , y >. | E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { a e. ( (/) ^m _om ) | ( a ` i ) (/) ( a ` j ) } ) } ) |` suc _om ) )
3 1 1 2 mp2an 
 |-  ( (/) Sat (/) ) = ( rec ( ( f e. _V |-> ( f u. { <. x , y >. | E. u e. f ( E. v e. f ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( (/) ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( (/) ^m _om ) | A. z e. (/) ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) ) , { <. x , y >. | E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { a e. ( (/) ^m _om ) | ( a ` i ) (/) ( a ` j ) } ) } ) |` suc _om )
4 peano1 
 |-  (/) e. _om
5 4 ne0ii 
 |-  _om =/= (/)
6 map0b 
 |-  ( _om =/= (/) -> ( (/) ^m _om ) = (/) )
7 5 6 ax-mp 
 |-  ( (/) ^m _om ) = (/)
8 7 difeq1i 
 |-  ( ( (/) ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) = ( (/) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) )
9 0dif 
 |-  ( (/) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) = (/)
10 8 9 eqtri 
 |-  ( ( (/) ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) = (/)
11 10 eqeq2i 
 |-  ( y = ( ( (/) ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) <-> y = (/) )
12 11 anbi2i 
 |-  ( ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( (/) ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) <-> ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = (/) ) )
13 12 rexbii 
 |-  ( E. v e. f ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( (/) ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) <-> E. v e. f ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = (/) ) )
14 r19.41v 
 |-  ( E. v e. f ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = (/) ) <-> ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = (/) ) )
15 13 14 bitri 
 |-  ( E. v e. f ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( (/) ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) <-> ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = (/) ) )
16 7 rabeqi 
 |-  { a e. ( (/) ^m _om ) | A. z e. (/) ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } = { a e. (/) | A. z e. (/) ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) }
17 rab0 
 |-  { a e. (/) | A. z e. (/) ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } = (/)
18 16 17 eqtri 
 |-  { a e. ( (/) ^m _om ) | A. z e. (/) ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } = (/)
19 18 eqeq2i 
 |-  ( y = { a e. ( (/) ^m _om ) | A. z e. (/) ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } <-> y = (/) )
20 19 anbi2i 
 |-  ( ( x = A.g i ( 1st ` u ) /\ y = { a e. ( (/) ^m _om ) | A. z e. (/) ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) <-> ( x = A.g i ( 1st ` u ) /\ y = (/) ) )
21 20 rexbii 
 |-  ( E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( (/) ^m _om ) | A. z e. (/) ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) <-> E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = (/) ) )
22 r19.41v 
 |-  ( E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = (/) ) <-> ( E. i e. _om x = A.g i ( 1st ` u ) /\ y = (/) ) )
23 21 22 bitri 
 |-  ( E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( (/) ^m _om ) | A. z e. (/) ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) <-> ( E. i e. _om x = A.g i ( 1st ` u ) /\ y = (/) ) )
24 15 23 orbi12i 
 |-  ( ( E. v e. f ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( (/) ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( (/) ^m _om ) | A. z e. (/) ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) <-> ( ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = (/) ) \/ ( E. i e. _om x = A.g i ( 1st ` u ) /\ y = (/) ) ) )
25 24 rexbii 
 |-  ( E. u e. f ( E. v e. f ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( (/) ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( (/) ^m _om ) | A. z e. (/) ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) <-> E. u e. f ( ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = (/) ) \/ ( E. i e. _om x = A.g i ( 1st ` u ) /\ y = (/) ) ) )
26 andir 
 |-  ( ( ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) /\ y = (/) ) <-> ( ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = (/) ) \/ ( E. i e. _om x = A.g i ( 1st ` u ) /\ y = (/) ) ) )
27 26 bicomi 
 |-  ( ( ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = (/) ) \/ ( E. i e. _om x = A.g i ( 1st ` u ) /\ y = (/) ) ) <-> ( ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) /\ y = (/) ) )
28 27 rexbii 
 |-  ( E. u e. f ( ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = (/) ) \/ ( E. i e. _om x = A.g i ( 1st ` u ) /\ 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 = (/) ) )
29 r19.41v 
 |-  ( 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. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) /\ y = (/) ) )
30 25 28 29 3bitri 
 |-  ( E. u e. f ( E. v e. f ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( (/) ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( (/) ^m _om ) | A. z e. (/) ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) <-> ( 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 = (/) ) )
31 30 biancomi 
 |-  ( E. u e. f ( E. v e. f ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( (/) ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( (/) ^m _om ) | A. z e. (/) ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) <-> ( 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 ) ) ) )
32 31 opabbii 
 |-  { <. x , y >. | E. u e. f ( E. v e. f ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( (/) ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( (/) ^m _om ) | A. z e. (/) ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` 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 ) ) ) }
33 32 uneq2i 
 |-  ( f u. { <. x , y >. | E. u e. f ( E. v e. f ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( (/) ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( (/) ^m _om ) | A. z e. (/) ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) = ( 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 ) ) ) } )
34 33 mpteq2i 
 |-  ( f e. _V |-> ( f u. { <. x , y >. | E. u e. f ( E. v e. f ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( (/) ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( (/) ^m _om ) | A. z e. (/) ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` 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 ) ) ) } ) )
35 7 rabeqi 
 |-  { a e. ( (/) ^m _om ) | ( a ` i ) (/) ( a ` j ) } = { a e. (/) | ( a ` i ) (/) ( a ` j ) }
36 rab0 
 |-  { a e. (/) | ( a ` i ) (/) ( a ` j ) } = (/)
37 35 36 eqtri 
 |-  { a e. ( (/) ^m _om ) | ( a ` i ) (/) ( a ` j ) } = (/)
38 37 eqeq2i 
 |-  ( y = { a e. ( (/) ^m _om ) | ( a ` i ) (/) ( a ` j ) } <-> y = (/) )
39 38 anbi2i 
 |-  ( ( x = ( i e.g j ) /\ y = { a e. ( (/) ^m _om ) | ( a ` i ) (/) ( a ` j ) } ) <-> ( x = ( i e.g j ) /\ y = (/) ) )
40 39 2rexbii 
 |-  ( E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { a e. ( (/) ^m _om ) | ( a ` i ) (/) ( a ` j ) } ) <-> E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = (/) ) )
41 r19.41vv 
 |-  ( E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = (/) ) <-> ( E. i e. _om E. j e. _om x = ( i e.g j ) /\ y = (/) ) )
42 40 41 bitri 
 |-  ( E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { a e. ( (/) ^m _om ) | ( a ` i ) (/) ( a ` j ) } ) <-> ( E. i e. _om E. j e. _om x = ( i e.g j ) /\ y = (/) ) )
43 42 biancomi 
 |-  ( E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { a e. ( (/) ^m _om ) | ( a ` i ) (/) ( a ` j ) } ) <-> ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) )
44 43 opabbii 
 |-  { <. x , y >. | E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { a e. ( (/) ^m _om ) | ( a ` i ) (/) ( a ` j ) } ) } = { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) }
45 rdgeq12 
 |-  ( ( ( f e. _V |-> ( f u. { <. x , y >. | E. u e. f ( E. v e. f ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( (/) ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( (/) ^m _om ) | A. z e. (/) ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` 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 ) ) ) } ) ) /\ { <. x , y >. | E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { a e. ( (/) ^m _om ) | ( a ` i ) (/) ( a ` j ) } ) } = { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) -> rec ( ( f e. _V |-> ( f u. { <. x , y >. | E. u e. f ( E. v e. f ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( (/) ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( (/) ^m _om ) | A. z e. (/) ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) ) , { <. x , y >. | E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { a e. ( (/) ^m _om ) | ( a ` i ) (/) ( a ` j ) } ) } ) = 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 ) ) } ) )
46 34 44 45 mp2an 
 |-  rec ( ( f e. _V |-> ( f u. { <. x , y >. | E. u e. f ( E. v e. f ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( (/) ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( (/) ^m _om ) | A. z e. (/) ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) ) , { <. x , y >. | E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { a e. ( (/) ^m _om ) | ( a ` i ) (/) ( a ` j ) } ) } ) = 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 ) ) } )
47 46 reseq1i 
 |-  ( rec ( ( f e. _V |-> ( f u. { <. x , y >. | E. u e. f ( E. v e. f ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( (/) ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( (/) ^m _om ) | A. z e. (/) ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) ) , { <. x , y >. | E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { a e. ( (/) ^m _om ) | ( a ` i ) (/) ( a ` j ) } ) } ) |` suc _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 _om )
48 3 47 eqtri 
 |-  ( (/) 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 ) ) } ) |` suc _om )