Metamath Proof Explorer

Theorem goaln0

Description: The "Godel-set of universal quantification" is a Godel formula of at least height 1. (Contributed by AV, 22-Oct-2023)

Ref Expression
Assertion goaln0 
|- ( A.g i A e. ( Fmla ` N ) -> N =/= (/) )

Proof

Step Hyp Ref Expression
1 df-goal 
 |-  A.g i A = <. 2o , <. i , A >. >.
2 2on0 
 |-  2o =/= (/)
3 2 neii 
 |-  -. 2o = (/)
4 3 intnanr 
 |-  -. ( 2o = (/) /\ <. i , A >. = <. k , j >. )
5 2oex 
 |-  2o e. _V
6 opex 
 |-  <. i , A >. e. _V
7 5 6 opth 
 |-  ( <. 2o , <. i , A >. >. = <. (/) , <. k , j >. >. <-> ( 2o = (/) /\ <. i , A >. = <. k , j >. ) )
8 4 7 mtbir 
 |-  -. <. 2o , <. i , A >. >. = <. (/) , <. k , j >. >.
9 goel 
 |-  ( ( k e. _om /\ j e. _om ) -> ( k e.g j ) = <. (/) , <. k , j >. >. )
10 9 eqeq2d 
 |-  ( ( k e. _om /\ j e. _om ) -> ( <. 2o , <. i , A >. >. = ( k e.g j ) <-> <. 2o , <. i , A >. >. = <. (/) , <. k , j >. >. ) )
11 8 10 mtbiri 
 |-  ( ( k e. _om /\ j e. _om ) -> -. <. 2o , <. i , A >. >. = ( k e.g j ) )
12 11 rgen2 
 |-  A. k e. _om A. j e. _om -. <. 2o , <. i , A >. >. = ( k e.g j )
13 ralnex2 
 |-  ( A. k e. _om A. j e. _om -. <. 2o , <. i , A >. >. = ( k e.g j ) <-> -. E. k e. _om E. j e. _om <. 2o , <. i , A >. >. = ( k e.g j ) )
14 12 13 mpbi 
 |-  -. E. k e. _om E. j e. _om <. 2o , <. i , A >. >. = ( k e.g j )
15 14 intnan 
 |-  -. ( <. 2o , <. i , A >. >. e. _V /\ E. k e. _om E. j e. _om <. 2o , <. i , A >. >. = ( k e.g j ) )
16 eqeq1 
 |-  ( x = <. 2o , <. i , A >. >. -> ( x = ( k e.g j ) <-> <. 2o , <. i , A >. >. = ( k e.g j ) ) )
17 16 2rexbidv 
 |-  ( x = <. 2o , <. i , A >. >. -> ( E. k e. _om E. j e. _om x = ( k e.g j ) <-> E. k e. _om E. j e. _om <. 2o , <. i , A >. >. = ( k e.g j ) ) )
18 fmla0 
 |-  ( Fmla ` (/) ) = { x e. _V | E. k e. _om E. j e. _om x = ( k e.g j ) }
19 17 18 elrab2 
 |-  ( <. 2o , <. i , A >. >. e. ( Fmla ` (/) ) <-> ( <. 2o , <. i , A >. >. e. _V /\ E. k e. _om E. j e. _om <. 2o , <. i , A >. >. = ( k e.g j ) ) )
20 15 19 mtbir 
 |-  -. <. 2o , <. i , A >. >. e. ( Fmla ` (/) )
21 1 20 eqneltri 
 |-  -. A.g i A e. ( Fmla ` (/) )
22 fveq2 
 |-  ( N = (/) -> ( Fmla ` N ) = ( Fmla ` (/) ) )
23 22 eleq2d 
 |-  ( N = (/) -> ( A.g i A e. ( Fmla ` N ) <-> A.g i A e. ( Fmla ` (/) ) ) )
24 21 23 mtbiri 
 |-  ( N = (/) -> -. A.g i A e. ( Fmla ` N ) )
25 24 necon2ai 
 |-  ( A.g i A e. ( Fmla ` N ) -> N =/= (/) )