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 =/= (/) )