Metamath Proof Explorer


Theorem gonan0

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

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

Proof

Step Hyp Ref Expression
1 1n0
 |-  1o =/= (/)
2 1 neii
 |-  -. 1o = (/)
3 2 intnanr
 |-  -. ( 1o = (/) /\ <. A , B >. = <. i , j >. )
4 1oex
 |-  1o e. _V
5 opex
 |-  <. A , B >. e. _V
6 4 5 opth
 |-  ( <. 1o , <. A , B >. >. = <. (/) , <. i , j >. >. <-> ( 1o = (/) /\ <. A , B >. = <. i , j >. ) )
7 3 6 mtbir
 |-  -. <. 1o , <. A , B >. >. = <. (/) , <. i , j >. >.
8 goel
 |-  ( ( i e. _om /\ j e. _om ) -> ( i e.g j ) = <. (/) , <. i , j >. >. )
9 8 eqeq2d
 |-  ( ( i e. _om /\ j e. _om ) -> ( <. 1o , <. A , B >. >. = ( i e.g j ) <-> <. 1o , <. A , B >. >. = <. (/) , <. i , j >. >. ) )
10 7 9 mtbiri
 |-  ( ( i e. _om /\ j e. _om ) -> -. <. 1o , <. A , B >. >. = ( i e.g j ) )
11 10 rgen2
 |-  A. i e. _om A. j e. _om -. <. 1o , <. A , B >. >. = ( i e.g j )
12 ralnex2
 |-  ( A. i e. _om A. j e. _om -. <. 1o , <. A , B >. >. = ( i e.g j ) <-> -. E. i e. _om E. j e. _om <. 1o , <. A , B >. >. = ( i e.g j ) )
13 11 12 mpbi
 |-  -. E. i e. _om E. j e. _om <. 1o , <. A , B >. >. = ( i e.g j )
14 13 intnan
 |-  -. ( <. 1o , <. A , B >. >. e. _V /\ E. i e. _om E. j e. _om <. 1o , <. A , B >. >. = ( i e.g j ) )
15 eqeq1
 |-  ( x = <. 1o , <. A , B >. >. -> ( x = ( i e.g j ) <-> <. 1o , <. A , B >. >. = ( i e.g j ) ) )
16 15 2rexbidv
 |-  ( x = <. 1o , <. A , B >. >. -> ( E. i e. _om E. j e. _om x = ( i e.g j ) <-> E. i e. _om E. j e. _om <. 1o , <. A , B >. >. = ( i e.g j ) ) )
17 fmla0
 |-  ( Fmla ` (/) ) = { x e. _V | E. i e. _om E. j e. _om x = ( i e.g j ) }
18 16 17 elrab2
 |-  ( <. 1o , <. A , B >. >. e. ( Fmla ` (/) ) <-> ( <. 1o , <. A , B >. >. e. _V /\ E. i e. _om E. j e. _om <. 1o , <. A , B >. >. = ( i e.g j ) ) )
19 14 18 mtbir
 |-  -. <. 1o , <. A , B >. >. e. ( Fmla ` (/) )
20 gonafv
 |-  ( ( A e. _V /\ B e. _V ) -> ( A |g B ) = <. 1o , <. A , B >. >. )
21 20 eleq1d
 |-  ( ( A e. _V /\ B e. _V ) -> ( ( A |g B ) e. ( Fmla ` (/) ) <-> <. 1o , <. A , B >. >. e. ( Fmla ` (/) ) ) )
22 19 21 mtbiri
 |-  ( ( A e. _V /\ B e. _V ) -> -. ( A |g B ) e. ( Fmla ` (/) ) )
23 eqid
 |-  ( x e. ( _V X. _V ) |-> <. 1o , x >. ) = ( x e. ( _V X. _V ) |-> <. 1o , x >. )
24 23 dmmptss
 |-  dom ( x e. ( _V X. _V ) |-> <. 1o , x >. ) C_ ( _V X. _V )
25 relxp
 |-  Rel ( _V X. _V )
26 relss
 |-  ( dom ( x e. ( _V X. _V ) |-> <. 1o , x >. ) C_ ( _V X. _V ) -> ( Rel ( _V X. _V ) -> Rel dom ( x e. ( _V X. _V ) |-> <. 1o , x >. ) ) )
27 24 25 26 mp2
 |-  Rel dom ( x e. ( _V X. _V ) |-> <. 1o , x >. )
28 df-gona
 |-  |g = ( x e. ( _V X. _V ) |-> <. 1o , x >. )
29 28 dmeqi
 |-  dom |g = dom ( x e. ( _V X. _V ) |-> <. 1o , x >. )
30 29 releqi
 |-  ( Rel dom |g <-> Rel dom ( x e. ( _V X. _V ) |-> <. 1o , x >. ) )
31 27 30 mpbir
 |-  Rel dom |g
32 31 ovprc
 |-  ( -. ( A e. _V /\ B e. _V ) -> ( A |g B ) = (/) )
33 peano1
 |-  (/) e. _om
34 fmlaomn0
 |-  ( (/) e. _om -> (/) e/ ( Fmla ` (/) ) )
35 33 34 ax-mp
 |-  (/) e/ ( Fmla ` (/) )
36 35 neli
 |-  -. (/) e. ( Fmla ` (/) )
37 eleq1
 |-  ( ( A |g B ) = (/) -> ( ( A |g B ) e. ( Fmla ` (/) ) <-> (/) e. ( Fmla ` (/) ) ) )
38 36 37 mtbiri
 |-  ( ( A |g B ) = (/) -> -. ( A |g B ) e. ( Fmla ` (/) ) )
39 32 38 syl
 |-  ( -. ( A e. _V /\ B e. _V ) -> -. ( A |g B ) e. ( Fmla ` (/) ) )
40 22 39 pm2.61i
 |-  -. ( A |g B ) e. ( Fmla ` (/) )
41 fveq2
 |-  ( N = (/) -> ( Fmla ` N ) = ( Fmla ` (/) ) )
42 41 eleq2d
 |-  ( N = (/) -> ( ( A |g B ) e. ( Fmla ` N ) <-> ( A |g B ) e. ( Fmla ` (/) ) ) )
43 40 42 mtbiri
 |-  ( N = (/) -> -. ( A |g B ) e. ( Fmla ` N ) )
44 43 necon2ai
 |-  ( ( A |g B ) e. ( Fmla ` N ) -> N =/= (/) )