Metamath Proof Explorer


Theorem fmla1

Description: The valid Godel formulas of height 1 is the set of all formulas of the form ( a |g b ) and A.g k a with atoms a , b of the form x e. y . (Contributed by AV, 20-Sep-2023)

Ref Expression
Assertion fmla1 Fmla 1 𝑜 = × ω × ω x | i ω j ω k ω l ω x = i 𝑔 j 𝑔 k 𝑔 l x = 𝑔 k i 𝑔 j

Proof

Step Hyp Ref Expression
1 df-1o 1 𝑜 = suc
2 1 fveq2i Fmla 1 𝑜 = Fmla suc
3 peano1 ω
4 fmlasuc ω Fmla suc = Fmla x | p Fmla q Fmla x = p 𝑔 q k ω x = 𝑔 k p
5 3 4 ax-mp Fmla suc = Fmla x | p Fmla q Fmla x = p 𝑔 q k ω x = 𝑔 k p
6 fmla0xp Fmla = × ω × ω
7 fmla0 Fmla = y V | i ω j ω y = i 𝑔 j
8 7 rexeqi p Fmla q Fmla x = p 𝑔 q k ω x = 𝑔 k p p y V | i ω j ω y = i 𝑔 j q Fmla x = p 𝑔 q k ω x = 𝑔 k p
9 eqeq1 y = p y = i 𝑔 j p = i 𝑔 j
10 9 2rexbidv y = p i ω j ω y = i 𝑔 j i ω j ω p = i 𝑔 j
11 10 elrab p y V | i ω j ω y = i 𝑔 j p V i ω j ω p = i 𝑔 j
12 oveq1 p = i 𝑔 j p 𝑔 q = i 𝑔 j 𝑔 q
13 12 eqeq2d p = i 𝑔 j x = p 𝑔 q x = i 𝑔 j 𝑔 q
14 13 rexbidv p = i 𝑔 j q Fmla x = p 𝑔 q q Fmla x = i 𝑔 j 𝑔 q
15 eqidd p = i 𝑔 j k = k
16 id p = i 𝑔 j p = i 𝑔 j
17 15 16 goaleq12d p = i 𝑔 j 𝑔 k p = 𝑔 k i 𝑔 j
18 17 eqeq2d p = i 𝑔 j x = 𝑔 k p x = 𝑔 k i 𝑔 j
19 18 rexbidv p = i 𝑔 j k ω x = 𝑔 k p k ω x = 𝑔 k i 𝑔 j
20 14 19 orbi12d p = i 𝑔 j q Fmla x = p 𝑔 q k ω x = 𝑔 k p q Fmla x = i 𝑔 j 𝑔 q k ω x = 𝑔 k i 𝑔 j
21 eqeq1 z = q z = k 𝑔 l q = k 𝑔 l
22 21 2rexbidv z = q k ω l ω z = k 𝑔 l k ω l ω q = k 𝑔 l
23 fmla0 Fmla = z V | k ω l ω z = k 𝑔 l
24 22 23 elrab2 q Fmla q V k ω l ω q = k 𝑔 l
25 oveq2 q = k 𝑔 l i 𝑔 j 𝑔 q = i 𝑔 j 𝑔 k 𝑔 l
26 25 eqeq2d q = k 𝑔 l x = i 𝑔 j 𝑔 q x = i 𝑔 j 𝑔 k 𝑔 l
27 26 biimpcd x = i 𝑔 j 𝑔 q q = k 𝑔 l x = i 𝑔 j 𝑔 k 𝑔 l
28 27 reximdv x = i 𝑔 j 𝑔 q l ω q = k 𝑔 l l ω x = i 𝑔 j 𝑔 k 𝑔 l
29 28 reximdv x = i 𝑔 j 𝑔 q k ω l ω q = k 𝑔 l k ω l ω x = i 𝑔 j 𝑔 k 𝑔 l
30 29 com12 k ω l ω q = k 𝑔 l x = i 𝑔 j 𝑔 q k ω l ω x = i 𝑔 j 𝑔 k 𝑔 l
31 24 30 simplbiim q Fmla x = i 𝑔 j 𝑔 q k ω l ω x = i 𝑔 j 𝑔 k 𝑔 l
32 31 rexlimiv q Fmla x = i 𝑔 j 𝑔 q k ω l ω x = i 𝑔 j 𝑔 k 𝑔 l
33 32 orim1i q Fmla x = i 𝑔 j 𝑔 q k ω x = 𝑔 k i 𝑔 j k ω l ω x = i 𝑔 j 𝑔 k 𝑔 l k ω x = 𝑔 k i 𝑔 j
34 r19.43 k ω l ω x = i 𝑔 j 𝑔 k 𝑔 l x = 𝑔 k i 𝑔 j k ω l ω x = i 𝑔 j 𝑔 k 𝑔 l k ω x = 𝑔 k i 𝑔 j
35 33 34 sylibr q Fmla x = i 𝑔 j 𝑔 q k ω x = 𝑔 k i 𝑔 j k ω l ω x = i 𝑔 j 𝑔 k 𝑔 l x = 𝑔 k i 𝑔 j
36 20 35 syl6bi p = i 𝑔 j q Fmla x = p 𝑔 q k ω x = 𝑔 k p k ω l ω x = i 𝑔 j 𝑔 k 𝑔 l x = 𝑔 k i 𝑔 j
37 36 com12 q Fmla x = p 𝑔 q k ω x = 𝑔 k p p = i 𝑔 j k ω l ω x = i 𝑔 j 𝑔 k 𝑔 l x = 𝑔 k i 𝑔 j
38 37 reximdv q Fmla x = p 𝑔 q k ω x = 𝑔 k p j ω p = i 𝑔 j j ω k ω l ω x = i 𝑔 j 𝑔 k 𝑔 l x = 𝑔 k i 𝑔 j
39 38 reximdv q Fmla x = p 𝑔 q k ω x = 𝑔 k p i ω j ω p = i 𝑔 j i ω j ω k ω l ω x = i 𝑔 j 𝑔 k 𝑔 l x = 𝑔 k i 𝑔 j
40 39 com12 i ω j ω p = i 𝑔 j q Fmla x = p 𝑔 q k ω x = 𝑔 k p i ω j ω k ω l ω x = i 𝑔 j 𝑔 k 𝑔 l x = 𝑔 k i 𝑔 j
41 11 40 simplbiim p y V | i ω j ω y = i 𝑔 j q Fmla x = p 𝑔 q k ω x = 𝑔 k p i ω j ω k ω l ω x = i 𝑔 j 𝑔 k 𝑔 l x = 𝑔 k i 𝑔 j
42 41 rexlimiv p y V | i ω j ω y = i 𝑔 j q Fmla x = p 𝑔 q k ω x = 𝑔 k p i ω j ω k ω l ω x = i 𝑔 j 𝑔 k 𝑔 l x = 𝑔 k i 𝑔 j
43 oveq1 i = m i 𝑔 j = m 𝑔 j
44 43 oveq1d i = m i 𝑔 j 𝑔 k 𝑔 l = m 𝑔 j 𝑔 k 𝑔 l
45 44 eqeq2d i = m x = i 𝑔 j 𝑔 k 𝑔 l x = m 𝑔 j 𝑔 k 𝑔 l
46 45 rexbidv i = m l ω x = i 𝑔 j 𝑔 k 𝑔 l l ω x = m 𝑔 j 𝑔 k 𝑔 l
47 eqidd i = m k = k
48 47 43 goaleq12d i = m 𝑔 k i 𝑔 j = 𝑔 k m 𝑔 j
49 48 eqeq2d i = m x = 𝑔 k i 𝑔 j x = 𝑔 k m 𝑔 j
50 46 49 orbi12d i = m l ω x = i 𝑔 j 𝑔 k 𝑔 l x = 𝑔 k i 𝑔 j l ω x = m 𝑔 j 𝑔 k 𝑔 l x = 𝑔 k m 𝑔 j
51 50 rexbidv i = m k ω l ω x = i 𝑔 j 𝑔 k 𝑔 l x = 𝑔 k i 𝑔 j k ω l ω x = m 𝑔 j 𝑔 k 𝑔 l x = 𝑔 k m 𝑔 j
52 oveq2 j = n m 𝑔 j = m 𝑔 n
53 52 oveq1d j = n m 𝑔 j 𝑔 k 𝑔 l = m 𝑔 n 𝑔 k 𝑔 l
54 53 eqeq2d j = n x = m 𝑔 j 𝑔 k 𝑔 l x = m 𝑔 n 𝑔 k 𝑔 l
55 54 rexbidv j = n l ω x = m 𝑔 j 𝑔 k 𝑔 l l ω x = m 𝑔 n 𝑔 k 𝑔 l
56 eqidd j = n k = k
57 56 52 goaleq12d j = n 𝑔 k m 𝑔 j = 𝑔 k m 𝑔 n
58 57 eqeq2d j = n x = 𝑔 k m 𝑔 j x = 𝑔 k m 𝑔 n
59 55 58 orbi12d j = n l ω x = m 𝑔 j 𝑔 k 𝑔 l x = 𝑔 k m 𝑔 j l ω x = m 𝑔 n 𝑔 k 𝑔 l x = 𝑔 k m 𝑔 n
60 59 rexbidv j = n k ω l ω x = m 𝑔 j 𝑔 k 𝑔 l x = 𝑔 k m 𝑔 j k ω l ω x = m 𝑔 n 𝑔 k 𝑔 l x = 𝑔 k m 𝑔 n
61 51 60 cbvrex2vw i ω j ω k ω l ω x = i 𝑔 j 𝑔 k 𝑔 l x = 𝑔 k i 𝑔 j m ω n ω k ω l ω x = m 𝑔 n 𝑔 k 𝑔 l x = 𝑔 k m 𝑔 n
62 oveq1 k = o k 𝑔 l = o 𝑔 l
63 62 oveq2d k = o m 𝑔 n 𝑔 k 𝑔 l = m 𝑔 n 𝑔 o 𝑔 l
64 63 eqeq2d k = o x = m 𝑔 n 𝑔 k 𝑔 l x = m 𝑔 n 𝑔 o 𝑔 l
65 64 rexbidv k = o l ω x = m 𝑔 n 𝑔 k 𝑔 l l ω x = m 𝑔 n 𝑔 o 𝑔 l
66 id k = o k = o
67 eqidd k = o m 𝑔 n = m 𝑔 n
68 66 67 goaleq12d k = o 𝑔 k m 𝑔 n = 𝑔 o m 𝑔 n
69 68 eqeq2d k = o x = 𝑔 k m 𝑔 n x = 𝑔 o m 𝑔 n
70 65 69 orbi12d k = o l ω x = m 𝑔 n 𝑔 k 𝑔 l x = 𝑔 k m 𝑔 n l ω x = m 𝑔 n 𝑔 o 𝑔 l x = 𝑔 o m 𝑔 n
71 70 cbvrexvw k ω l ω x = m 𝑔 n 𝑔 k 𝑔 l x = 𝑔 k m 𝑔 n o ω l ω x = m 𝑔 n 𝑔 o 𝑔 l x = 𝑔 o m 𝑔 n
72 3 ne0ii ω
73 r19.44zv ω l ω x = m 𝑔 n 𝑔 o 𝑔 l x = 𝑔 o m 𝑔 n l ω x = m 𝑔 n 𝑔 o 𝑔 l x = 𝑔 o m 𝑔 n
74 72 73 ax-mp l ω x = m 𝑔 n 𝑔 o 𝑔 l x = 𝑔 o m 𝑔 n l ω x = m 𝑔 n 𝑔 o 𝑔 l x = 𝑔 o m 𝑔 n
75 eqeq1 y = m 𝑔 n y = i 𝑔 j m 𝑔 n = i 𝑔 j
76 75 2rexbidv y = m 𝑔 n i ω j ω y = i 𝑔 j i ω j ω m 𝑔 n = i 𝑔 j
77 ovexd m ω n ω o ω l ω x = m 𝑔 n 𝑔 o 𝑔 l x = 𝑔 o m 𝑔 n m 𝑔 n V
78 simpl m ω n ω m ω
79 43 eqeq2d i = m m 𝑔 n = i 𝑔 j m 𝑔 n = m 𝑔 j
80 79 rexbidv i = m j ω m 𝑔 n = i 𝑔 j j ω m 𝑔 n = m 𝑔 j
81 80 adantl m ω n ω i = m j ω m 𝑔 n = i 𝑔 j j ω m 𝑔 n = m 𝑔 j
82 simpr m ω n ω n ω
83 52 eqeq2d j = n m 𝑔 n = m 𝑔 j m 𝑔 n = m 𝑔 n
84 83 adantl m ω n ω j = n m 𝑔 n = m 𝑔 j m 𝑔 n = m 𝑔 n
85 eqidd m ω n ω m 𝑔 n = m 𝑔 n
86 82 84 85 rspcedvd m ω n ω j ω m 𝑔 n = m 𝑔 j
87 78 81 86 rspcedvd m ω n ω i ω j ω m 𝑔 n = i 𝑔 j
88 87 ad5ant12 m ω n ω o ω l ω x = m 𝑔 n 𝑔 o 𝑔 l x = 𝑔 o m 𝑔 n i ω j ω m 𝑔 n = i 𝑔 j
89 76 77 88 elrabd m ω n ω o ω l ω x = m 𝑔 n 𝑔 o 𝑔 l x = 𝑔 o m 𝑔 n m 𝑔 n y V | i ω j ω y = i 𝑔 j
90 oveq1 p = m 𝑔 n p 𝑔 q = m 𝑔 n 𝑔 q
91 90 eqeq2d p = m 𝑔 n x = p 𝑔 q x = m 𝑔 n 𝑔 q
92 91 rexbidv p = m 𝑔 n q Fmla x = p 𝑔 q q Fmla x = m 𝑔 n 𝑔 q
93 eqidd p = m 𝑔 n k = k
94 id p = m 𝑔 n p = m 𝑔 n
95 93 94 goaleq12d p = m 𝑔 n 𝑔 k p = 𝑔 k m 𝑔 n
96 95 eqeq2d p = m 𝑔 n x = 𝑔 k p x = 𝑔 k m 𝑔 n
97 96 rexbidv p = m 𝑔 n k ω x = 𝑔 k p k ω x = 𝑔 k m 𝑔 n
98 92 97 orbi12d p = m 𝑔 n q Fmla x = p 𝑔 q k ω x = 𝑔 k p q Fmla x = m 𝑔 n 𝑔 q k ω x = 𝑔 k m 𝑔 n
99 98 adantl m ω n ω o ω l ω x = m 𝑔 n 𝑔 o 𝑔 l x = 𝑔 o m 𝑔 n p = m 𝑔 n q Fmla x = p 𝑔 q k ω x = 𝑔 k p q Fmla x = m 𝑔 n 𝑔 q k ω x = 𝑔 k m 𝑔 n
100 ovexd m ω n ω o ω l ω o 𝑔 l V
101 simpr m ω n ω o ω o ω
102 101 adantr m ω n ω o ω l ω o ω
103 oveq1 i = o i 𝑔 j = o 𝑔 j
104 103 eqeq2d i = o o 𝑔 l = i 𝑔 j o 𝑔 l = o 𝑔 j
105 104 rexbidv i = o j ω o 𝑔 l = i 𝑔 j j ω o 𝑔 l = o 𝑔 j
106 105 adantl m ω n ω o ω l ω i = o j ω o 𝑔 l = i 𝑔 j j ω o 𝑔 l = o 𝑔 j
107 simpr m ω n ω o ω l ω l ω
108 oveq2 j = l o 𝑔 j = o 𝑔 l
109 108 eqeq2d j = l o 𝑔 l = o 𝑔 j o 𝑔 l = o 𝑔 l
110 109 adantl m ω n ω o ω l ω j = l o 𝑔 l = o 𝑔 j o 𝑔 l = o 𝑔 l
111 eqidd m ω n ω o ω l ω o 𝑔 l = o 𝑔 l
112 107 110 111 rspcedvd m ω n ω o ω l ω j ω o 𝑔 l = o 𝑔 j
113 102 106 112 rspcedvd m ω n ω o ω l ω i ω j ω o 𝑔 l = i 𝑔 j
114 eqeq1 p = o 𝑔 l p = i 𝑔 j o 𝑔 l = i 𝑔 j
115 114 2rexbidv p = o 𝑔 l i ω j ω p = i 𝑔 j i ω j ω o 𝑔 l = i 𝑔 j
116 fmla0 Fmla = p V | i ω j ω p = i 𝑔 j
117 115 116 elrab2 o 𝑔 l Fmla o 𝑔 l V i ω j ω o 𝑔 l = i 𝑔 j
118 100 113 117 sylanbrc m ω n ω o ω l ω o 𝑔 l Fmla
119 118 adantr m ω n ω o ω l ω x = m 𝑔 n 𝑔 o 𝑔 l o 𝑔 l Fmla
120 oveq2 q = o 𝑔 l m 𝑔 n 𝑔 q = m 𝑔 n 𝑔 o 𝑔 l
121 120 eqeq2d q = o 𝑔 l x = m 𝑔 n 𝑔 q x = m 𝑔 n 𝑔 o 𝑔 l
122 121 adantl m ω n ω o ω l ω x = m 𝑔 n 𝑔 o 𝑔 l q = o 𝑔 l x = m 𝑔 n 𝑔 q x = m 𝑔 n 𝑔 o 𝑔 l
123 simpr m ω n ω o ω l ω x = m 𝑔 n 𝑔 o 𝑔 l x = m 𝑔 n 𝑔 o 𝑔 l
124 119 122 123 rspcedvd m ω n ω o ω l ω x = m 𝑔 n 𝑔 o 𝑔 l q Fmla x = m 𝑔 n 𝑔 q
125 124 ex m ω n ω o ω l ω x = m 𝑔 n 𝑔 o 𝑔 l q Fmla x = m 𝑔 n 𝑔 q
126 102 adantr m ω n ω o ω l ω x = 𝑔 o m 𝑔 n o ω
127 69 adantl m ω n ω o ω l ω x = 𝑔 o m 𝑔 n k = o x = 𝑔 k m 𝑔 n x = 𝑔 o m 𝑔 n
128 simpr m ω n ω o ω l ω x = 𝑔 o m 𝑔 n x = 𝑔 o m 𝑔 n
129 126 127 128 rspcedvd m ω n ω o ω l ω x = 𝑔 o m 𝑔 n k ω x = 𝑔 k m 𝑔 n
130 129 ex m ω n ω o ω l ω x = 𝑔 o m 𝑔 n k ω x = 𝑔 k m 𝑔 n
131 125 130 orim12d m ω n ω o ω l ω x = m 𝑔 n 𝑔 o 𝑔 l x = 𝑔 o m 𝑔 n q Fmla x = m 𝑔 n 𝑔 q k ω x = 𝑔 k m 𝑔 n
132 131 imp m ω n ω o ω l ω x = m 𝑔 n 𝑔 o 𝑔 l x = 𝑔 o m 𝑔 n q Fmla x = m 𝑔 n 𝑔 q k ω x = 𝑔 k m 𝑔 n
133 89 99 132 rspcedvd m ω n ω o ω l ω x = m 𝑔 n 𝑔 o 𝑔 l x = 𝑔 o m 𝑔 n p y V | i ω j ω y = i 𝑔 j q Fmla x = p 𝑔 q k ω x = 𝑔 k p
134 133 ex m ω n ω o ω l ω x = m 𝑔 n 𝑔 o 𝑔 l x = 𝑔 o m 𝑔 n p y V | i ω j ω y = i 𝑔 j q Fmla x = p 𝑔 q k ω x = 𝑔 k p
135 134 rexlimdva m ω n ω o ω l ω x = m 𝑔 n 𝑔 o 𝑔 l x = 𝑔 o m 𝑔 n p y V | i ω j ω y = i 𝑔 j q Fmla x = p 𝑔 q k ω x = 𝑔 k p
136 74 135 syl5bir m ω n ω o ω l ω x = m 𝑔 n 𝑔 o 𝑔 l x = 𝑔 o m 𝑔 n p y V | i ω j ω y = i 𝑔 j q Fmla x = p 𝑔 q k ω x = 𝑔 k p
137 136 rexlimdva m ω n ω o ω l ω x = m 𝑔 n 𝑔 o 𝑔 l x = 𝑔 o m 𝑔 n p y V | i ω j ω y = i 𝑔 j q Fmla x = p 𝑔 q k ω x = 𝑔 k p
138 71 137 syl5bi m ω n ω k ω l ω x = m 𝑔 n 𝑔 k 𝑔 l x = 𝑔 k m 𝑔 n p y V | i ω j ω y = i 𝑔 j q Fmla x = p 𝑔 q k ω x = 𝑔 k p
139 138 rexlimivv m ω n ω k ω l ω x = m 𝑔 n 𝑔 k 𝑔 l x = 𝑔 k m 𝑔 n p y V | i ω j ω y = i 𝑔 j q Fmla x = p 𝑔 q k ω x = 𝑔 k p
140 61 139 sylbi i ω j ω k ω l ω x = i 𝑔 j 𝑔 k 𝑔 l x = 𝑔 k i 𝑔 j p y V | i ω j ω y = i 𝑔 j q Fmla x = p 𝑔 q k ω x = 𝑔 k p
141 42 140 impbii p y V | i ω j ω y = i 𝑔 j q Fmla x = p 𝑔 q k ω x = 𝑔 k p i ω j ω k ω l ω x = i 𝑔 j 𝑔 k 𝑔 l x = 𝑔 k i 𝑔 j
142 8 141 bitri p Fmla q Fmla x = p 𝑔 q k ω x = 𝑔 k p i ω j ω k ω l ω x = i 𝑔 j 𝑔 k 𝑔 l x = 𝑔 k i 𝑔 j
143 142 abbii x | p Fmla q Fmla x = p 𝑔 q k ω x = 𝑔 k p = x | i ω j ω k ω l ω x = i 𝑔 j 𝑔 k 𝑔 l x = 𝑔 k i 𝑔 j
144 6 143 uneq12i Fmla x | p Fmla q Fmla x = p 𝑔 q k ω x = 𝑔 k p = × ω × ω x | i ω j ω k ω l ω x = i 𝑔 j 𝑔 k 𝑔 l x = 𝑔 k i 𝑔 j
145 2 5 144 3eqtri Fmla 1 𝑜 = × ω × ω x | i ω j ω k ω l ω x = i 𝑔 j 𝑔 k 𝑔 l x = 𝑔 k i 𝑔 j