Metamath Proof Explorer

Theorem goalr

Description: If the "Godel-set of universal quantification" applied to a class is a Godel formula, the class is also a Godel formula. Remark: The reverse is not valid for A being of the same height as the "Godel-set of universal quantification". (Contributed by AV, 22-Oct-2023)

Ref Expression
Assertion goalr 
|- ( ( N e. _om /\ A.g i a e. ( Fmla ` N ) ) -> a e. ( Fmla ` N ) )

Proof

Step Hyp Ref Expression
1 goaln0 
 |-  ( A.g i a e. ( Fmla ` N ) -> N =/= (/) )
2 1 adantl 
 |-  ( ( N e. _om /\ A.g i a e. ( Fmla ` N ) ) -> N =/= (/) )
3 nnsuc 
 |-  ( ( N e. _om /\ N =/= (/) ) -> E. n e. _om N = suc n )
4 suceq 
 |-  ( x = (/) -> suc x = suc (/) )
5 4 fveq2d 
 |-  ( x = (/) -> ( Fmla ` suc x ) = ( Fmla ` suc (/) ) )
6 5 eleq2d 
 |-  ( x = (/) -> ( A.g i a e. ( Fmla ` suc x ) <-> A.g i a e. ( Fmla ` suc (/) ) ) )
7 5 eleq2d 
 |-  ( x = (/) -> ( a e. ( Fmla ` suc x ) <-> a e. ( Fmla ` suc (/) ) ) )
8 6 7 imbi12d 
 |-  ( x = (/) -> ( ( A.g i a e. ( Fmla ` suc x ) -> a e. ( Fmla ` suc x ) ) <-> ( A.g i a e. ( Fmla ` suc (/) ) -> a e. ( Fmla ` suc (/) ) ) ) )
9 suceq 
 |-  ( x = y -> suc x = suc y )
10 9 fveq2d 
 |-  ( x = y -> ( Fmla ` suc x ) = ( Fmla ` suc y ) )
11 10 eleq2d 
 |-  ( x = y -> ( A.g i a e. ( Fmla ` suc x ) <-> A.g i a e. ( Fmla ` suc y ) ) )
12 10 eleq2d 
 |-  ( x = y -> ( a e. ( Fmla ` suc x ) <-> a e. ( Fmla ` suc y ) ) )
13 11 12 imbi12d 
 |-  ( x = y -> ( ( A.g i a e. ( Fmla ` suc x ) -> a e. ( Fmla ` suc x ) ) <-> ( A.g i a e. ( Fmla ` suc y ) -> a e. ( Fmla ` suc y ) ) ) )
14 suceq 
 |-  ( x = suc y -> suc x = suc suc y )
15 14 fveq2d 
 |-  ( x = suc y -> ( Fmla ` suc x ) = ( Fmla ` suc suc y ) )
16 15 eleq2d 
 |-  ( x = suc y -> ( A.g i a e. ( Fmla ` suc x ) <-> A.g i a e. ( Fmla ` suc suc y ) ) )
17 15 eleq2d 
 |-  ( x = suc y -> ( a e. ( Fmla ` suc x ) <-> a e. ( Fmla ` suc suc y ) ) )
18 16 17 imbi12d 
 |-  ( x = suc y -> ( ( A.g i a e. ( Fmla ` suc x ) -> a e. ( Fmla ` suc x ) ) <-> ( A.g i a e. ( Fmla ` suc suc y ) -> a e. ( Fmla ` suc suc y ) ) ) )
19 suceq 
 |-  ( x = n -> suc x = suc n )
20 19 fveq2d 
 |-  ( x = n -> ( Fmla ` suc x ) = ( Fmla ` suc n ) )
21 20 eleq2d 
 |-  ( x = n -> ( A.g i a e. ( Fmla ` suc x ) <-> A.g i a e. ( Fmla ` suc n ) ) )
22 20 eleq2d 
 |-  ( x = n -> ( a e. ( Fmla ` suc x ) <-> a e. ( Fmla ` suc n ) ) )
23 21 22 imbi12d 
 |-  ( x = n -> ( ( A.g i a e. ( Fmla ` suc x ) -> a e. ( Fmla ` suc x ) ) <-> ( A.g i a e. ( Fmla ` suc n ) -> a e. ( Fmla ` suc n ) ) ) )
24 peano1 
 |-  (/) e. _om
25 df-goal 
 |-  A.g i a = <. 2o , <. i , a >. >.
26 opex 
 |-  <. 2o , <. i , a >. >. e. _V
27 25 26 eqeltri 
 |-  A.g i a e. _V
28 isfmlasuc 
 |-  ( ( (/) e. _om /\ A.g i a e. _V ) -> ( A.g i a e. ( Fmla ` suc (/) ) <-> ( A.g i a e. ( Fmla ` (/) ) \/ E. u e. ( Fmla ` (/) ) ( E. v e. ( Fmla ` (/) ) A.g i a = ( u |g v ) \/ E. k e. _om A.g i a = A.g k u ) ) ) )
29 24 27 28 mp2an 
 |-  ( A.g i a e. ( Fmla ` suc (/) ) <-> ( A.g i a e. ( Fmla ` (/) ) \/ E. u e. ( Fmla ` (/) ) ( E. v e. ( Fmla ` (/) ) A.g i a = ( u |g v ) \/ E. k e. _om A.g i a = A.g k u ) ) )
30 eqeq1 
 |-  ( x = A.g i a -> ( x = ( k e.g j ) <-> A.g i a = ( k e.g j ) ) )
31 30 2rexbidv 
 |-  ( x = A.g i a -> ( E. k e. _om E. j e. _om x = ( k e.g j ) <-> E. k e. _om E. j e. _om A.g i a = ( k e.g j ) ) )
32 fmla0 
 |-  ( Fmla ` (/) ) = { x e. _V | E. k e. _om E. j e. _om x = ( k e.g j ) }
33 31 32 elrab2 
 |-  ( A.g i a e. ( Fmla ` (/) ) <-> ( A.g i a e. _V /\ E. k e. _om E. j e. _om A.g i a = ( k e.g j ) ) )
34 25 a1i 
 |-  ( ( k e. _om /\ j e. _om ) -> A.g i a = <. 2o , <. i , a >. >. )
35 goel 
 |-  ( ( k e. _om /\ j e. _om ) -> ( k e.g j ) = <. (/) , <. k , j >. >. )
36 34 35 eqeq12d 
 |-  ( ( k e. _om /\ j e. _om ) -> ( A.g i a = ( k e.g j ) <-> <. 2o , <. i , a >. >. = <. (/) , <. k , j >. >. ) )
37 2oex 
 |-  2o e. _V
38 opex 
 |-  <. i , a >. e. _V
39 37 38 opth 
 |-  ( <. 2o , <. i , a >. >. = <. (/) , <. k , j >. >. <-> ( 2o = (/) /\ <. i , a >. = <. k , j >. ) )
40 2on0 
 |-  2o =/= (/)
41 eqneqall 
 |-  ( 2o = (/) -> ( 2o =/= (/) -> a e. ( Fmla ` suc (/) ) ) )
42 40 41 mpi 
 |-  ( 2o = (/) -> a e. ( Fmla ` suc (/) ) )
43 42 adantr 
 |-  ( ( 2o = (/) /\ <. i , a >. = <. k , j >. ) -> a e. ( Fmla ` suc (/) ) )
44 39 43 sylbi 
 |-  ( <. 2o , <. i , a >. >. = <. (/) , <. k , j >. >. -> a e. ( Fmla ` suc (/) ) )
45 36 44 syl6bi 
 |-  ( ( k e. _om /\ j e. _om ) -> ( A.g i a = ( k e.g j ) -> a e. ( Fmla ` suc (/) ) ) )
46 45 rexlimdva 
 |-  ( k e. _om -> ( E. j e. _om A.g i a = ( k e.g j ) -> a e. ( Fmla ` suc (/) ) ) )
47 46 rexlimiv 
 |-  ( E. k e. _om E. j e. _om A.g i a = ( k e.g j ) -> a e. ( Fmla ` suc (/) ) )
48 33 47 simplbiim 
 |-  ( A.g i a e. ( Fmla ` (/) ) -> a e. ( Fmla ` suc (/) ) )
49 gonanegoal 
 |-  ( u |g v ) =/= A.g i a
50 eqneqall 
 |-  ( ( u |g v ) = A.g i a -> ( ( u |g v ) =/= A.g i a -> a e. ( Fmla ` suc (/) ) ) )
51 49 50 mpi 
 |-  ( ( u |g v ) = A.g i a -> a e. ( Fmla ` suc (/) ) )
52 51 eqcoms 
 |-  ( A.g i a = ( u |g v ) -> a e. ( Fmla ` suc (/) ) )
53 52 a1i 
 |-  ( ( u e. ( Fmla ` (/) ) /\ v e. ( Fmla ` (/) ) ) -> ( A.g i a = ( u |g v ) -> a e. ( Fmla ` suc (/) ) ) )
54 53 rexlimdva 
 |-  ( u e. ( Fmla ` (/) ) -> ( E. v e. ( Fmla ` (/) ) A.g i a = ( u |g v ) -> a e. ( Fmla ` suc (/) ) ) )
55 df-goal 
 |-  A.g k u = <. 2o , <. k , u >. >.
56 25 55 eqeq12i 
 |-  ( A.g i a = A.g k u <-> <. 2o , <. i , a >. >. = <. 2o , <. k , u >. >. )
57 37 38 opth 
 |-  ( <. 2o , <. i , a >. >. = <. 2o , <. k , u >. >. <-> ( 2o = 2o /\ <. i , a >. = <. k , u >. ) )
58 vex 
 |-  i e. _V
59 vex 
 |-  a e. _V
60 58 59 opth 
 |-  ( <. i , a >. = <. k , u >. <-> ( i = k /\ a = u ) )
61 eleq1w 
 |-  ( u = a -> ( u e. ( Fmla ` (/) ) <-> a e. ( Fmla ` (/) ) ) )
62 fmlasssuc 
 |-  ( (/) e. _om -> ( Fmla ` (/) ) C_ ( Fmla ` suc (/) ) )
63 24 62 ax-mp 
 |-  ( Fmla ` (/) ) C_ ( Fmla ` suc (/) )
64 63 sseli 
 |-  ( a e. ( Fmla ` (/) ) -> a e. ( Fmla ` suc (/) ) )
65 61 64 syl6bi 
 |-  ( u = a -> ( u e. ( Fmla ` (/) ) -> a e. ( Fmla ` suc (/) ) ) )
66 65 eqcoms 
 |-  ( a = u -> ( u e. ( Fmla ` (/) ) -> a e. ( Fmla ` suc (/) ) ) )
67 60 66 simplbiim 
 |-  ( <. i , a >. = <. k , u >. -> ( u e. ( Fmla ` (/) ) -> a e. ( Fmla ` suc (/) ) ) )
68 57 67 simplbiim 
 |-  ( <. 2o , <. i , a >. >. = <. 2o , <. k , u >. >. -> ( u e. ( Fmla ` (/) ) -> a e. ( Fmla ` suc (/) ) ) )
69 68 com12 
 |-  ( u e. ( Fmla ` (/) ) -> ( <. 2o , <. i , a >. >. = <. 2o , <. k , u >. >. -> a e. ( Fmla ` suc (/) ) ) )
70 69 adantr 
 |-  ( ( u e. ( Fmla ` (/) ) /\ k e. _om ) -> ( <. 2o , <. i , a >. >. = <. 2o , <. k , u >. >. -> a e. ( Fmla ` suc (/) ) ) )
71 56 70 syl5bi 
 |-  ( ( u e. ( Fmla ` (/) ) /\ k e. _om ) -> ( A.g i a = A.g k u -> a e. ( Fmla ` suc (/) ) ) )
72 71 rexlimdva 
 |-  ( u e. ( Fmla ` (/) ) -> ( E. k e. _om A.g i a = A.g k u -> a e. ( Fmla ` suc (/) ) ) )
73 54 72 jaod 
 |-  ( u e. ( Fmla ` (/) ) -> ( ( E. v e. ( Fmla ` (/) ) A.g i a = ( u |g v ) \/ E. k e. _om A.g i a = A.g k u ) -> a e. ( Fmla ` suc (/) ) ) )
74 73 rexlimiv 
 |-  ( E. u e. ( Fmla ` (/) ) ( E. v e. ( Fmla ` (/) ) A.g i a = ( u |g v ) \/ E. k e. _om A.g i a = A.g k u ) -> a e. ( Fmla ` suc (/) ) )
75 48 74 jaoi 
 |-  ( ( A.g i a e. ( Fmla ` (/) ) \/ E. u e. ( Fmla ` (/) ) ( E. v e. ( Fmla ` (/) ) A.g i a = ( u |g v ) \/ E. k e. _om A.g i a = A.g k u ) ) -> a e. ( Fmla ` suc (/) ) )
76 29 75 sylbi 
 |-  ( A.g i a e. ( Fmla ` suc (/) ) -> a e. ( Fmla ` suc (/) ) )
77 goalrlem 
 |-  ( y e. _om -> ( ( A.g i a e. ( Fmla ` suc y ) -> a e. ( Fmla ` suc y ) ) -> ( A.g i a e. ( Fmla ` suc suc y ) -> a e. ( Fmla ` suc suc y ) ) ) )
78 8 13 18 23 76 77 finds 
 |-  ( n e. _om -> ( A.g i a e. ( Fmla ` suc n ) -> a e. ( Fmla ` suc n ) ) )
79 78 adantr 
 |-  ( ( n e. _om /\ N = suc n ) -> ( A.g i a e. ( Fmla ` suc n ) -> a e. ( Fmla ` suc n ) ) )
80 fveq2 
 |-  ( N = suc n -> ( Fmla ` N ) = ( Fmla ` suc n ) )
81 80 eleq2d 
 |-  ( N = suc n -> ( A.g i a e. ( Fmla ` N ) <-> A.g i a e. ( Fmla ` suc n ) ) )
82 80 eleq2d 
 |-  ( N = suc n -> ( a e. ( Fmla ` N ) <-> a e. ( Fmla ` suc n ) ) )
83 81 82 imbi12d 
 |-  ( N = suc n -> ( ( A.g i a e. ( Fmla ` N ) -> a e. ( Fmla ` N ) ) <-> ( A.g i a e. ( Fmla ` suc n ) -> a e. ( Fmla ` suc n ) ) ) )
84 83 adantl 
 |-  ( ( n e. _om /\ N = suc n ) -> ( ( A.g i a e. ( Fmla ` N ) -> a e. ( Fmla ` N ) ) <-> ( A.g i a e. ( Fmla ` suc n ) -> a e. ( Fmla ` suc n ) ) ) )
85 79 84 mpbird 
 |-  ( ( n e. _om /\ N = suc n ) -> ( A.g i a e. ( Fmla ` N ) -> a e. ( Fmla ` N ) ) )
86 85 rexlimiva 
 |-  ( E. n e. _om N = suc n -> ( A.g i a e. ( Fmla ` N ) -> a e. ( Fmla ` N ) ) )
87 3 86 syl 
 |-  ( ( N e. _om /\ N =/= (/) ) -> ( A.g i a e. ( Fmla ` N ) -> a e. ( Fmla ` N ) ) )
88 87 impancom 
 |-  ( ( N e. _om /\ A.g i a e. ( Fmla ` N ) ) -> ( N =/= (/) -> a e. ( Fmla ` N ) ) )
89 2 88 mpd 
 |-  ( ( N e. _om /\ A.g i a e. ( Fmla ` N ) ) -> a e. ( Fmla ` N ) )