Metamath Proof Explorer

Theorem fmla0

Description: The valid Godel formulas of height 0 is the set of all formulas of the form v_i e. v_j ("Godel-set of membership") coded as <. (/) , <. i , j >. >. . (Contributed by AV, 14-Sep-2023)

Ref Expression
Assertion fmla0 
|- ( Fmla ` (/) ) = { x e. _V | 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 fmlafv 
 |-  ( (/) e. suc _om -> ( Fmla ` (/) ) = dom ( ( (/) Sat (/) ) ` (/) ) )
4 1 2 3 mp2b 
 |-  ( Fmla ` (/) ) = dom ( ( (/) Sat (/) ) ` (/) )
5 satf00 
 |-  ( ( (/) Sat (/) ) ` (/) ) = { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) }
6 5 dmeqi 
 |-  dom ( ( (/) Sat (/) ) ` (/) ) = dom { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) }
7 0ex 
 |-  (/) e. _V
8 7 isseti 
 |-  E. y y = (/)
9 19.41v 
 |-  ( E. y ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) <-> ( E. y y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) )
10 8 9 mpbiran 
 |-  ( E. y ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) <-> E. i e. _om E. j e. _om x = ( i e.g j ) )
11 10 abbii 
 |-  { x | E. y ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } = { x | E. i e. _om E. j e. _om x = ( i e.g j ) }
12 dmopab 
 |-  dom { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } = { x | E. y ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) }
13 rabab 
 |-  { x e. _V | E. i e. _om E. j e. _om x = ( i e.g j ) } = { x | E. i e. _om E. j e. _om x = ( i e.g j ) }
14 11 12 13 3eqtr4i 
 |-  dom { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } = { x e. _V | E. i e. _om E. j e. _om x = ( i e.g j ) }
15 4 6 14 3eqtri 
 |-  ( Fmla ` (/) ) = { x e. _V | E. i e. _om E. j e. _om x = ( i e.g j ) }