Metamath Proof Explorer

Theorem fmla0xp

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, 15-Sep-2023)

Ref Expression
Assertion fmla0xp 
|- ( Fmla ` (/) ) = ( { (/) } X. ( _om X. _om ) )

Proof

Step Hyp Ref Expression
1 fmla0 
 |-  ( Fmla ` (/) ) = { x e. _V | E. i e. _om E. j e. _om x = ( i e.g j ) }
2 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 ) }
3 eqabcb 
 |-  ( { x | E. i e. _om E. j e. _om x = ( i e.g j ) } = ( { (/) } X. ( _om X. _om ) ) <-> A. x ( E. i e. _om E. j e. _om x = ( i e.g j ) <-> x e. ( { (/) } X. ( _om X. _om ) ) ) )
4 goel 
 |-  ( ( i e. _om /\ j e. _om ) -> ( i e.g j ) = <. (/) , <. i , j >. >. )
5 4 eqeq2d 
 |-  ( ( i e. _om /\ j e. _om ) -> ( x = ( i e.g j ) <-> x = <. (/) , <. i , j >. >. ) )
6 5 2rexbiia 
 |-  ( E. i e. _om E. j e. _om x = ( i e.g j ) <-> E. i e. _om E. j e. _om x = <. (/) , <. i , j >. >. )
7 0ex 
 |-  (/) e. _V
8 7 snid 
 |-  (/) e. { (/) }
9 8 a1i 
 |-  ( ( i e. _om /\ j e. _om ) -> (/) e. { (/) } )
10 opelxpi 
 |-  ( ( i e. _om /\ j e. _om ) -> <. i , j >. e. ( _om X. _om ) )
11 9 10 opelxpd 
 |-  ( ( i e. _om /\ j e. _om ) -> <. (/) , <. i , j >. >. e. ( { (/) } X. ( _om X. _om ) ) )
12 eleq1 
 |-  ( x = <. (/) , <. i , j >. >. -> ( x e. ( { (/) } X. ( _om X. _om ) ) <-> <. (/) , <. i , j >. >. e. ( { (/) } X. ( _om X. _om ) ) ) )
13 11 12 syl5ibrcom 
 |-  ( ( i e. _om /\ j e. _om ) -> ( x = <. (/) , <. i , j >. >. -> x e. ( { (/) } X. ( _om X. _om ) ) ) )
14 13 rexlimivv 
 |-  ( E. i e. _om E. j e. _om x = <. (/) , <. i , j >. >. -> x e. ( { (/) } X. ( _om X. _om ) ) )
15 elxpi 
 |-  ( x e. ( { (/) } X. ( _om X. _om ) ) -> E. y E. z ( x = <. y , z >. /\ ( y e. { (/) } /\ z e. ( _om X. _om ) ) ) )
16 elsni 
 |-  ( y e. { (/) } -> y = (/) )
17 16 opeq1d 
 |-  ( y e. { (/) } -> <. y , z >. = <. (/) , z >. )
18 17 eqeq2d 
 |-  ( y e. { (/) } -> ( x = <. y , z >. <-> x = <. (/) , z >. ) )
19 18 adantr 
 |-  ( ( y e. { (/) } /\ z e. ( _om X. _om ) ) -> ( x = <. y , z >. <-> x = <. (/) , z >. ) )
20 elxpi 
 |-  ( z e. ( _om X. _om ) -> E. i E. j ( z = <. i , j >. /\ ( i e. _om /\ j e. _om ) ) )
21 simprr 
 |-  ( ( x = <. (/) , z >. /\ ( z = <. i , j >. /\ ( i e. _om /\ j e. _om ) ) ) -> ( i e. _om /\ j e. _om ) )
22 simpl 
 |-  ( ( x = <. (/) , z >. /\ ( z = <. i , j >. /\ ( i e. _om /\ j e. _om ) ) ) -> x = <. (/) , z >. )
23 opeq2 
 |-  ( z = <. i , j >. -> <. (/) , z >. = <. (/) , <. i , j >. >. )
24 23 adantr 
 |-  ( ( z = <. i , j >. /\ ( i e. _om /\ j e. _om ) ) -> <. (/) , z >. = <. (/) , <. i , j >. >. )
25 24 adantl 
 |-  ( ( x = <. (/) , z >. /\ ( z = <. i , j >. /\ ( i e. _om /\ j e. _om ) ) ) -> <. (/) , z >. = <. (/) , <. i , j >. >. )
26 22 25 eqtrd 
 |-  ( ( x = <. (/) , z >. /\ ( z = <. i , j >. /\ ( i e. _om /\ j e. _om ) ) ) -> x = <. (/) , <. i , j >. >. )
27 21 26 jca 
 |-  ( ( x = <. (/) , z >. /\ ( z = <. i , j >. /\ ( i e. _om /\ j e. _om ) ) ) -> ( ( i e. _om /\ j e. _om ) /\ x = <. (/) , <. i , j >. >. ) )
28 27 ex 
 |-  ( x = <. (/) , z >. -> ( ( z = <. i , j >. /\ ( i e. _om /\ j e. _om ) ) -> ( ( i e. _om /\ j e. _om ) /\ x = <. (/) , <. i , j >. >. ) ) )
29 28 2eximdv 
 |-  ( x = <. (/) , z >. -> ( E. i E. j ( z = <. i , j >. /\ ( i e. _om /\ j e. _om ) ) -> E. i E. j ( ( i e. _om /\ j e. _om ) /\ x = <. (/) , <. i , j >. >. ) ) )
30 r2ex 
 |-  ( E. i e. _om E. j e. _om x = <. (/) , <. i , j >. >. <-> E. i E. j ( ( i e. _om /\ j e. _om ) /\ x = <. (/) , <. i , j >. >. ) )
31 29 30 imbitrrdi 
 |-  ( x = <. (/) , z >. -> ( E. i E. j ( z = <. i , j >. /\ ( i e. _om /\ j e. _om ) ) -> E. i e. _om E. j e. _om x = <. (/) , <. i , j >. >. ) )
32 20 31 syl5com 
 |-  ( z e. ( _om X. _om ) -> ( x = <. (/) , z >. -> E. i e. _om E. j e. _om x = <. (/) , <. i , j >. >. ) )
33 32 adantl 
 |-  ( ( y e. { (/) } /\ z e. ( _om X. _om ) ) -> ( x = <. (/) , z >. -> E. i e. _om E. j e. _om x = <. (/) , <. i , j >. >. ) )
34 19 33 sylbid 
 |-  ( ( y e. { (/) } /\ z e. ( _om X. _om ) ) -> ( x = <. y , z >. -> E. i e. _om E. j e. _om x = <. (/) , <. i , j >. >. ) )
35 34 impcom 
 |-  ( ( x = <. y , z >. /\ ( y e. { (/) } /\ z e. ( _om X. _om ) ) ) -> E. i e. _om E. j e. _om x = <. (/) , <. i , j >. >. )
36 35 exlimivv 
 |-  ( E. y E. z ( x = <. y , z >. /\ ( y e. { (/) } /\ z e. ( _om X. _om ) ) ) -> E. i e. _om E. j e. _om x = <. (/) , <. i , j >. >. )
37 15 36 syl 
 |-  ( x e. ( { (/) } X. ( _om X. _om ) ) -> E. i e. _om E. j e. _om x = <. (/) , <. i , j >. >. )
38 14 37 impbii 
 |-  ( E. i e. _om E. j e. _om x = <. (/) , <. i , j >. >. <-> x e. ( { (/) } X. ( _om X. _om ) ) )
39 6 38 bitri 
 |-  ( E. i e. _om E. j e. _om x = ( i e.g j ) <-> x e. ( { (/) } X. ( _om X. _om ) ) )
40 3 39 mpgbir 
 |-  { x | E. i e. _om E. j e. _om x = ( i e.g j ) } = ( { (/) } X. ( _om X. _om ) )
41 1 2 40 3eqtri 
 |-  ( Fmla ` (/) ) = ( { (/) } X. ( _om X. _om ) )