Metamath Proof Explorer

Theorem gonar

Description: If the "Godel-set of NAND" applied to classes is a Godel formula, the classes are also Godel formulas. Remark: The reverse is not valid for A or B being of the same height as the "Godel-set of NAND". (Contributed by AV, 21-Oct-2023)

Ref Expression
Assertion gonar 
|- ( ( N e. _om /\ ( a |g b ) e. ( Fmla ` N ) ) -> ( a e. ( Fmla ` N ) /\ b e. ( Fmla ` N ) ) )

Proof

Step Hyp Ref Expression
1 gonan0 
 |-  ( ( a |g b ) e. ( Fmla ` N ) -> N =/= (/) )
2 1 adantl 
 |-  ( ( N e. _om /\ ( a |g b ) e. ( Fmla ` N ) ) -> N =/= (/) )
3 nnsuc 
 |-  ( ( N e. _om /\ N =/= (/) ) -> E. x e. _om N = suc x )
4 suceq 
 |-  ( d = (/) -> suc d = suc (/) )
5 4 fveq2d 
 |-  ( d = (/) -> ( Fmla ` suc d ) = ( Fmla ` suc (/) ) )
6 5 eleq2d 
 |-  ( d = (/) -> ( ( a |g b ) e. ( Fmla ` suc d ) <-> ( a |g b ) e. ( Fmla ` suc (/) ) ) )
7 5 eleq2d 
 |-  ( d = (/) -> ( a e. ( Fmla ` suc d ) <-> a e. ( Fmla ` suc (/) ) ) )
8 5 eleq2d 
 |-  ( d = (/) -> ( b e. ( Fmla ` suc d ) <-> b e. ( Fmla ` suc (/) ) ) )
9 7 8 anbi12d 
 |-  ( d = (/) -> ( ( a e. ( Fmla ` suc d ) /\ b e. ( Fmla ` suc d ) ) <-> ( a e. ( Fmla ` suc (/) ) /\ b e. ( Fmla ` suc (/) ) ) ) )
10 6 9 imbi12d 
 |-  ( d = (/) -> ( ( ( a |g b ) e. ( Fmla ` suc d ) -> ( a e. ( Fmla ` suc d ) /\ b e. ( Fmla ` suc d ) ) ) <-> ( ( a |g b ) e. ( Fmla ` suc (/) ) -> ( a e. ( Fmla ` suc (/) ) /\ b e. ( Fmla ` suc (/) ) ) ) ) )
11 suceq 
 |-  ( d = c -> suc d = suc c )
12 11 fveq2d 
 |-  ( d = c -> ( Fmla ` suc d ) = ( Fmla ` suc c ) )
13 12 eleq2d 
 |-  ( d = c -> ( ( a |g b ) e. ( Fmla ` suc d ) <-> ( a |g b ) e. ( Fmla ` suc c ) ) )
14 12 eleq2d 
 |-  ( d = c -> ( a e. ( Fmla ` suc d ) <-> a e. ( Fmla ` suc c ) ) )
15 12 eleq2d 
 |-  ( d = c -> ( b e. ( Fmla ` suc d ) <-> b e. ( Fmla ` suc c ) ) )
16 14 15 anbi12d 
 |-  ( d = c -> ( ( a e. ( Fmla ` suc d ) /\ b e. ( Fmla ` suc d ) ) <-> ( a e. ( Fmla ` suc c ) /\ b e. ( Fmla ` suc c ) ) ) )
17 13 16 imbi12d 
 |-  ( d = c -> ( ( ( a |g b ) e. ( Fmla ` suc d ) -> ( a e. ( Fmla ` suc d ) /\ b e. ( Fmla ` suc d ) ) ) <-> ( ( a |g b ) e. ( Fmla ` suc c ) -> ( a e. ( Fmla ` suc c ) /\ b e. ( Fmla ` suc c ) ) ) ) )
18 suceq 
 |-  ( d = suc c -> suc d = suc suc c )
19 18 fveq2d 
 |-  ( d = suc c -> ( Fmla ` suc d ) = ( Fmla ` suc suc c ) )
20 19 eleq2d 
 |-  ( d = suc c -> ( ( a |g b ) e. ( Fmla ` suc d ) <-> ( a |g b ) e. ( Fmla ` suc suc c ) ) )
21 19 eleq2d 
 |-  ( d = suc c -> ( a e. ( Fmla ` suc d ) <-> a e. ( Fmla ` suc suc c ) ) )
22 19 eleq2d 
 |-  ( d = suc c -> ( b e. ( Fmla ` suc d ) <-> b e. ( Fmla ` suc suc c ) ) )
23 21 22 anbi12d 
 |-  ( d = suc c -> ( ( a e. ( Fmla ` suc d ) /\ b e. ( Fmla ` suc d ) ) <-> ( a e. ( Fmla ` suc suc c ) /\ b e. ( Fmla ` suc suc c ) ) ) )
24 20 23 imbi12d 
 |-  ( d = suc c -> ( ( ( a |g b ) e. ( Fmla ` suc d ) -> ( a e. ( Fmla ` suc d ) /\ b e. ( Fmla ` suc d ) ) ) <-> ( ( a |g b ) e. ( Fmla ` suc suc c ) -> ( a e. ( Fmla ` suc suc c ) /\ b e. ( Fmla ` suc suc c ) ) ) ) )
25 suceq 
 |-  ( d = x -> suc d = suc x )
26 25 fveq2d 
 |-  ( d = x -> ( Fmla ` suc d ) = ( Fmla ` suc x ) )
27 26 eleq2d 
 |-  ( d = x -> ( ( a |g b ) e. ( Fmla ` suc d ) <-> ( a |g b ) e. ( Fmla ` suc x ) ) )
28 26 eleq2d 
 |-  ( d = x -> ( a e. ( Fmla ` suc d ) <-> a e. ( Fmla ` suc x ) ) )
29 26 eleq2d 
 |-  ( d = x -> ( b e. ( Fmla ` suc d ) <-> b e. ( Fmla ` suc x ) ) )
30 28 29 anbi12d 
 |-  ( d = x -> ( ( a e. ( Fmla ` suc d ) /\ b e. ( Fmla ` suc d ) ) <-> ( a e. ( Fmla ` suc x ) /\ b e. ( Fmla ` suc x ) ) ) )
31 27 30 imbi12d 
 |-  ( d = x -> ( ( ( a |g b ) e. ( Fmla ` suc d ) -> ( a e. ( Fmla ` suc d ) /\ b e. ( Fmla ` suc d ) ) ) <-> ( ( a |g b ) e. ( Fmla ` suc x ) -> ( a e. ( Fmla ` suc x ) /\ b e. ( Fmla ` suc x ) ) ) ) )
32 peano1 
 |-  (/) e. _om
33 ovex 
 |-  ( a |g b ) e. _V
34 isfmlasuc 
 |-  ( ( (/) e. _om /\ ( a |g b ) e. _V ) -> ( ( a |g b ) e. ( Fmla ` suc (/) ) <-> ( ( a |g b ) e. ( Fmla ` (/) ) \/ E. u e. ( Fmla ` (/) ) ( E. v e. ( Fmla ` (/) ) ( a |g b ) = ( u |g v ) \/ E. i e. _om ( a |g b ) = A.g i u ) ) ) )
35 32 33 34 mp2an 
 |-  ( ( a |g b ) e. ( Fmla ` suc (/) ) <-> ( ( a |g b ) e. ( Fmla ` (/) ) \/ E. u e. ( Fmla ` (/) ) ( E. v e. ( Fmla ` (/) ) ( a |g b ) = ( u |g v ) \/ E. i e. _om ( a |g b ) = A.g i u ) ) )
36 eqeq1 
 |-  ( x = ( a |g b ) -> ( x = ( i e.g j ) <-> ( a |g b ) = ( i e.g j ) ) )
37 36 2rexbidv 
 |-  ( x = ( a |g b ) -> ( E. i e. _om E. j e. _om x = ( i e.g j ) <-> E. i e. _om E. j e. _om ( a |g b ) = ( i e.g j ) ) )
38 fmla0 
 |-  ( Fmla ` (/) ) = { x e. _V | E. i e. _om E. j e. _om x = ( i e.g j ) }
39 37 38 elrab2 
 |-  ( ( a |g b ) e. ( Fmla ` (/) ) <-> ( ( a |g b ) e. _V /\ E. i e. _om E. j e. _om ( a |g b ) = ( i e.g j ) ) )
40 gonafv 
 |-  ( ( a e. _V /\ b e. _V ) -> ( a |g b ) = <. 1o , <. a , b >. >. )
41 40 el2v 
 |-  ( a |g b ) = <. 1o , <. a , b >. >.
42 41 a1i 
 |-  ( ( i e. _om /\ j e. _om ) -> ( a |g b ) = <. 1o , <. a , b >. >. )
43 goel 
 |-  ( ( i e. _om /\ j e. _om ) -> ( i e.g j ) = <. (/) , <. i , j >. >. )
44 42 43 eqeq12d 
 |-  ( ( i e. _om /\ j e. _om ) -> ( ( a |g b ) = ( i e.g j ) <-> <. 1o , <. a , b >. >. = <. (/) , <. i , j >. >. ) )
45 1oex 
 |-  1o e. _V
46 opex 
 |-  <. a , b >. e. _V
47 45 46 opth 
 |-  ( <. 1o , <. a , b >. >. = <. (/) , <. i , j >. >. <-> ( 1o = (/) /\ <. a , b >. = <. i , j >. ) )
48 1n0 
 |-  1o =/= (/)
49 eqneqall 
 |-  ( 1o = (/) -> ( 1o =/= (/) -> ( a e. ( Fmla ` suc (/) ) /\ b e. ( Fmla ` suc (/) ) ) ) )
50 48 49 mpi 
 |-  ( 1o = (/) -> ( a e. ( Fmla ` suc (/) ) /\ b e. ( Fmla ` suc (/) ) ) )
51 50 adantr 
 |-  ( ( 1o = (/) /\ <. a , b >. = <. i , j >. ) -> ( a e. ( Fmla ` suc (/) ) /\ b e. ( Fmla ` suc (/) ) ) )
52 47 51 sylbi 
 |-  ( <. 1o , <. a , b >. >. = <. (/) , <. i , j >. >. -> ( a e. ( Fmla ` suc (/) ) /\ b e. ( Fmla ` suc (/) ) ) )
53 44 52 biimtrdi 
 |-  ( ( i e. _om /\ j e. _om ) -> ( ( a |g b ) = ( i e.g j ) -> ( a e. ( Fmla ` suc (/) ) /\ b e. ( Fmla ` suc (/) ) ) ) )
54 53 rexlimdva 
 |-  ( i e. _om -> ( E. j e. _om ( a |g b ) = ( i e.g j ) -> ( a e. ( Fmla ` suc (/) ) /\ b e. ( Fmla ` suc (/) ) ) ) )
55 54 rexlimiv 
 |-  ( E. i e. _om E. j e. _om ( a |g b ) = ( i e.g j ) -> ( a e. ( Fmla ` suc (/) ) /\ b e. ( Fmla ` suc (/) ) ) )
56 55 adantl 
 |-  ( ( ( a |g b ) e. _V /\ E. i e. _om E. j e. _om ( a |g b ) = ( i e.g j ) ) -> ( a e. ( Fmla ` suc (/) ) /\ b e. ( Fmla ` suc (/) ) ) )
57 39 56 sylbi 
 |-  ( ( a |g b ) e. ( Fmla ` (/) ) -> ( a e. ( Fmla ` suc (/) ) /\ b e. ( Fmla ` suc (/) ) ) )
58 41 a1i 
 |-  ( ( u e. ( Fmla ` (/) ) /\ v e. ( Fmla ` (/) ) ) -> ( a |g b ) = <. 1o , <. a , b >. >. )
59 gonafv 
 |-  ( ( u e. ( Fmla ` (/) ) /\ v e. ( Fmla ` (/) ) ) -> ( u |g v ) = <. 1o , <. u , v >. >. )
60 58 59 eqeq12d 
 |-  ( ( u e. ( Fmla ` (/) ) /\ v e. ( Fmla ` (/) ) ) -> ( ( a |g b ) = ( u |g v ) <-> <. 1o , <. a , b >. >. = <. 1o , <. u , v >. >. ) )
61 45 46 opth 
 |-  ( <. 1o , <. a , b >. >. = <. 1o , <. u , v >. >. <-> ( 1o = 1o /\ <. a , b >. = <. u , v >. ) )
62 vex 
 |-  a e. _V
63 vex 
 |-  b e. _V
64 62 63 opth 
 |-  ( <. a , b >. = <. u , v >. <-> ( a = u /\ b = v ) )
65 simpl 
 |-  ( ( a = u /\ b = v ) -> a = u )
66 65 equcomd 
 |-  ( ( a = u /\ b = v ) -> u = a )
67 66 eleq1d 
 |-  ( ( a = u /\ b = v ) -> ( u e. ( Fmla ` (/) ) <-> a e. ( Fmla ` (/) ) ) )
68 simpr 
 |-  ( ( a = u /\ b = v ) -> b = v )
69 68 equcomd 
 |-  ( ( a = u /\ b = v ) -> v = b )
70 69 eleq1d 
 |-  ( ( a = u /\ b = v ) -> ( v e. ( Fmla ` (/) ) <-> b e. ( Fmla ` (/) ) ) )
71 67 70 anbi12d 
 |-  ( ( a = u /\ b = v ) -> ( ( u e. ( Fmla ` (/) ) /\ v e. ( Fmla ` (/) ) ) <-> ( a e. ( Fmla ` (/) ) /\ b e. ( Fmla ` (/) ) ) ) )
72 64 71 sylbi 
 |-  ( <. a , b >. = <. u , v >. -> ( ( u e. ( Fmla ` (/) ) /\ v e. ( Fmla ` (/) ) ) <-> ( a e. ( Fmla ` (/) ) /\ b e. ( Fmla ` (/) ) ) ) )
73 72 adantl 
 |-  ( ( 1o = 1o /\ <. a , b >. = <. u , v >. ) -> ( ( u e. ( Fmla ` (/) ) /\ v e. ( Fmla ` (/) ) ) <-> ( a e. ( Fmla ` (/) ) /\ b e. ( Fmla ` (/) ) ) ) )
74 61 73 sylbi 
 |-  ( <. 1o , <. a , b >. >. = <. 1o , <. u , v >. >. -> ( ( u e. ( Fmla ` (/) ) /\ v e. ( Fmla ` (/) ) ) <-> ( a e. ( Fmla ` (/) ) /\ b e. ( Fmla ` (/) ) ) ) )
75 fmlasssuc 
 |-  ( (/) e. _om -> ( Fmla ` (/) ) C_ ( Fmla ` suc (/) ) )
76 32 75 ax-mp 
 |-  ( Fmla ` (/) ) C_ ( Fmla ` suc (/) )
77 76 sseli 
 |-  ( a e. ( Fmla ` (/) ) -> a e. ( Fmla ` suc (/) ) )
78 76 sseli 
 |-  ( b e. ( Fmla ` (/) ) -> b e. ( Fmla ` suc (/) ) )
79 77 78 anim12i 
 |-  ( ( a e. ( Fmla ` (/) ) /\ b e. ( Fmla ` (/) ) ) -> ( a e. ( Fmla ` suc (/) ) /\ b e. ( Fmla ` suc (/) ) ) )
80 74 79 biimtrdi 
 |-  ( <. 1o , <. a , b >. >. = <. 1o , <. u , v >. >. -> ( ( u e. ( Fmla ` (/) ) /\ v e. ( Fmla ` (/) ) ) -> ( a e. ( Fmla ` suc (/) ) /\ b e. ( Fmla ` suc (/) ) ) ) )
81 80 com12 
 |-  ( ( u e. ( Fmla ` (/) ) /\ v e. ( Fmla ` (/) ) ) -> ( <. 1o , <. a , b >. >. = <. 1o , <. u , v >. >. -> ( a e. ( Fmla ` suc (/) ) /\ b e. ( Fmla ` suc (/) ) ) ) )
82 60 81 sylbid 
 |-  ( ( u e. ( Fmla ` (/) ) /\ v e. ( Fmla ` (/) ) ) -> ( ( a |g b ) = ( u |g v ) -> ( a e. ( Fmla ` suc (/) ) /\ b e. ( Fmla ` suc (/) ) ) ) )
83 82 rexlimdva 
 |-  ( u e. ( Fmla ` (/) ) -> ( E. v e. ( Fmla ` (/) ) ( a |g b ) = ( u |g v ) -> ( a e. ( Fmla ` suc (/) ) /\ b e. ( Fmla ` suc (/) ) ) ) )
84 gonanegoal 
 |-  ( a |g b ) =/= A.g i u
85 eqneqall 
 |-  ( ( a |g b ) = A.g i u -> ( ( a |g b ) =/= A.g i u -> ( a e. ( Fmla ` suc (/) ) /\ b e. ( Fmla ` suc (/) ) ) ) )
86 84 85 mpi 
 |-  ( ( a |g b ) = A.g i u -> ( a e. ( Fmla ` suc (/) ) /\ b e. ( Fmla ` suc (/) ) ) )
87 86 a1i 
 |-  ( ( u e. ( Fmla ` (/) ) /\ i e. _om ) -> ( ( a |g b ) = A.g i u -> ( a e. ( Fmla ` suc (/) ) /\ b e. ( Fmla ` suc (/) ) ) ) )
88 87 rexlimdva 
 |-  ( u e. ( Fmla ` (/) ) -> ( E. i e. _om ( a |g b ) = A.g i u -> ( a e. ( Fmla ` suc (/) ) /\ b e. ( Fmla ` suc (/) ) ) ) )
89 83 88 jaod 
 |-  ( u e. ( Fmla ` (/) ) -> ( ( E. v e. ( Fmla ` (/) ) ( a |g b ) = ( u |g v ) \/ E. i e. _om ( a |g b ) = A.g i u ) -> ( a e. ( Fmla ` suc (/) ) /\ b e. ( Fmla ` suc (/) ) ) ) )
90 89 rexlimiv 
 |-  ( E. u e. ( Fmla ` (/) ) ( E. v e. ( Fmla ` (/) ) ( a |g b ) = ( u |g v ) \/ E. i e. _om ( a |g b ) = A.g i u ) -> ( a e. ( Fmla ` suc (/) ) /\ b e. ( Fmla ` suc (/) ) ) )
91 57 90 jaoi 
 |-  ( ( ( a |g b ) e. ( Fmla ` (/) ) \/ E. u e. ( Fmla ` (/) ) ( E. v e. ( Fmla ` (/) ) ( a |g b ) = ( u |g v ) \/ E. i e. _om ( a |g b ) = A.g i u ) ) -> ( a e. ( Fmla ` suc (/) ) /\ b e. ( Fmla ` suc (/) ) ) )
92 35 91 sylbi 
 |-  ( ( a |g b ) e. ( Fmla ` suc (/) ) -> ( a e. ( Fmla ` suc (/) ) /\ b e. ( Fmla ` suc (/) ) ) )
93 gonarlem 
 |-  ( c e. _om -> ( ( ( a |g b ) e. ( Fmla ` suc c ) -> ( a e. ( Fmla ` suc c ) /\ b e. ( Fmla ` suc c ) ) ) -> ( ( a |g b ) e. ( Fmla ` suc suc c ) -> ( a e. ( Fmla ` suc suc c ) /\ b e. ( Fmla ` suc suc c ) ) ) ) )
94 10 17 24 31 92 93 finds 
 |-  ( x e. _om -> ( ( a |g b ) e. ( Fmla ` suc x ) -> ( a e. ( Fmla ` suc x ) /\ b e. ( Fmla ` suc x ) ) ) )
95 94 adantr 
 |-  ( ( x e. _om /\ N = suc x ) -> ( ( a |g b ) e. ( Fmla ` suc x ) -> ( a e. ( Fmla ` suc x ) /\ b e. ( Fmla ` suc x ) ) ) )
96 fveq2 
 |-  ( N = suc x -> ( Fmla ` N ) = ( Fmla ` suc x ) )
97 96 eleq2d 
 |-  ( N = suc x -> ( ( a |g b ) e. ( Fmla ` N ) <-> ( a |g b ) e. ( Fmla ` suc x ) ) )
98 96 eleq2d 
 |-  ( N = suc x -> ( a e. ( Fmla ` N ) <-> a e. ( Fmla ` suc x ) ) )
99 96 eleq2d 
 |-  ( N = suc x -> ( b e. ( Fmla ` N ) <-> b e. ( Fmla ` suc x ) ) )
100 98 99 anbi12d 
 |-  ( N = suc x -> ( ( a e. ( Fmla ` N ) /\ b e. ( Fmla ` N ) ) <-> ( a e. ( Fmla ` suc x ) /\ b e. ( Fmla ` suc x ) ) ) )
101 97 100 imbi12d 
 |-  ( N = suc x -> ( ( ( a |g b ) e. ( Fmla ` N ) -> ( a e. ( Fmla ` N ) /\ b e. ( Fmla ` N ) ) ) <-> ( ( a |g b ) e. ( Fmla ` suc x ) -> ( a e. ( Fmla ` suc x ) /\ b e. ( Fmla ` suc x ) ) ) ) )
102 101 adantl 
 |-  ( ( x e. _om /\ N = suc x ) -> ( ( ( a |g b ) e. ( Fmla ` N ) -> ( a e. ( Fmla ` N ) /\ b e. ( Fmla ` N ) ) ) <-> ( ( a |g b ) e. ( Fmla ` suc x ) -> ( a e. ( Fmla ` suc x ) /\ b e. ( Fmla ` suc x ) ) ) ) )
103 95 102 mpbird 
 |-  ( ( x e. _om /\ N = suc x ) -> ( ( a |g b ) e. ( Fmla ` N ) -> ( a e. ( Fmla ` N ) /\ b e. ( Fmla ` N ) ) ) )
104 103 rexlimiva 
 |-  ( E. x e. _om N = suc x -> ( ( a |g b ) e. ( Fmla ` N ) -> ( a e. ( Fmla ` N ) /\ b e. ( Fmla ` N ) ) ) )
105 3 104 syl 
 |-  ( ( N e. _om /\ N =/= (/) ) -> ( ( a |g b ) e. ( Fmla ` N ) -> ( a e. ( Fmla ` N ) /\ b e. ( Fmla ` N ) ) ) )
106 105 impancom 
 |-  ( ( N e. _om /\ ( a |g b ) e. ( Fmla ` N ) ) -> ( N =/= (/) -> ( a e. ( Fmla ` N ) /\ b e. ( Fmla ` N ) ) ) )
107 2 106 mpd 
 |-  ( ( N e. _om /\ ( a |g b ) e. ( Fmla ` N ) ) -> ( a e. ( Fmla ` N ) /\ b e. ( Fmla ` N ) ) )