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