Metamath Proof Explorer


Theorem fmlaomn0

Description: The empty set is not a Godel formula of any height. (Contributed by AV, 21-Oct-2023)

Ref Expression
Assertion fmlaomn0 N ω Fmla N

Proof

Step Hyp Ref Expression
1 fveq2 x = Fmla x = Fmla
2 1 eleq2d x = Fmla x Fmla
3 2 notbid x = ¬ Fmla x ¬ Fmla
4 fveq2 x = y Fmla x = Fmla y
5 4 eleq2d x = y Fmla x Fmla y
6 5 notbid x = y ¬ Fmla x ¬ Fmla y
7 fveq2 x = suc y Fmla x = Fmla suc y
8 7 eleq2d x = suc y Fmla x Fmla suc y
9 8 notbid x = suc y ¬ Fmla x ¬ Fmla suc y
10 fveq2 x = N Fmla x = Fmla N
11 10 eleq2d x = N Fmla x Fmla N
12 11 notbid x = N ¬ Fmla x ¬ Fmla N
13 0ex V
14 opex i j V
15 13 14 pm3.2i V i j V
16 15 a1i i ω j ω V i j V
17 necom i j i j
18 opnz i j V i j V
19 17 18 bitri i j V i j V
20 16 19 sylibr i ω j ω i j
21 20 neneqd i ω j ω ¬ = i j
22 goel i ω j ω i 𝑔 j = i j
23 22 eqeq2d i ω j ω = i 𝑔 j = i j
24 21 23 mtbird i ω j ω ¬ = i 𝑔 j
25 24 rgen2 i ω j ω ¬ = i 𝑔 j
26 ralnex2 i ω j ω ¬ = i 𝑔 j ¬ i ω j ω = i 𝑔 j
27 25 26 mpbi ¬ i ω j ω = i 𝑔 j
28 27 intnan ¬ V i ω j ω = i 𝑔 j
29 fmla0 Fmla = x V | i ω j ω x = i 𝑔 j
30 29 eleq2i Fmla x V | i ω j ω x = i 𝑔 j
31 eqeq1 x = x = i 𝑔 j = i 𝑔 j
32 31 2rexbidv x = i ω j ω x = i 𝑔 j i ω j ω = i 𝑔 j
33 32 elrab x V | i ω j ω x = i 𝑔 j V i ω j ω = i 𝑔 j
34 30 33 bitri Fmla V i ω j ω = i 𝑔 j
35 28 34 mtbir ¬ Fmla
36 simpr y ω ¬ Fmla y ¬ Fmla y
37 1oex 1 𝑜 V
38 opex u v V
39 37 38 opnzi 1 𝑜 u v
40 39 nesymi ¬ = 1 𝑜 u v
41 gonafv u Fmla y v Fmla y u 𝑔 v = 1 𝑜 u v
42 41 adantll y ω u Fmla y v Fmla y u 𝑔 v = 1 𝑜 u v
43 42 eqeq2d y ω u Fmla y v Fmla y = u 𝑔 v = 1 𝑜 u v
44 40 43 mtbiri y ω u Fmla y v Fmla y ¬ = u 𝑔 v
45 44 ralrimiva y ω u Fmla y v Fmla y ¬ = u 𝑔 v
46 2oex 2 𝑜 V
47 opex i u V
48 46 47 opnzi 2 𝑜 i u
49 48 nesymi ¬ = 2 𝑜 i u
50 df-goal 𝑔 i u = 2 𝑜 i u
51 50 eqeq2i = 𝑔 i u = 2 𝑜 i u
52 49 51 mtbir ¬ = 𝑔 i u
53 52 a1i y ω u Fmla y i ω ¬ = 𝑔 i u
54 53 ralrimiva y ω u Fmla y i ω ¬ = 𝑔 i u
55 45 54 jca y ω u Fmla y v Fmla y ¬ = u 𝑔 v i ω ¬ = 𝑔 i u
56 55 ralrimiva y ω u Fmla y v Fmla y ¬ = u 𝑔 v i ω ¬ = 𝑔 i u
57 56 adantr y ω ¬ Fmla y u Fmla y v Fmla y ¬ = u 𝑔 v i ω ¬ = 𝑔 i u
58 ralnex v Fmla y ¬ = u 𝑔 v ¬ v Fmla y = u 𝑔 v
59 ralnex i ω ¬ = 𝑔 i u ¬ i ω = 𝑔 i u
60 58 59 anbi12i v Fmla y ¬ = u 𝑔 v i ω ¬ = 𝑔 i u ¬ v Fmla y = u 𝑔 v ¬ i ω = 𝑔 i u
61 ioran ¬ v Fmla y = u 𝑔 v i ω = 𝑔 i u ¬ v Fmla y = u 𝑔 v ¬ i ω = 𝑔 i u
62 60 61 bitr4i v Fmla y ¬ = u 𝑔 v i ω ¬ = 𝑔 i u ¬ v Fmla y = u 𝑔 v i ω = 𝑔 i u
63 62 ralbii u Fmla y v Fmla y ¬ = u 𝑔 v i ω ¬ = 𝑔 i u u Fmla y ¬ v Fmla y = u 𝑔 v i ω = 𝑔 i u
64 ralnex u Fmla y ¬ v Fmla y = u 𝑔 v i ω = 𝑔 i u ¬ u Fmla y v Fmla y = u 𝑔 v i ω = 𝑔 i u
65 63 64 bitri u Fmla y v Fmla y ¬ = u 𝑔 v i ω ¬ = 𝑔 i u ¬ u Fmla y v Fmla y = u 𝑔 v i ω = 𝑔 i u
66 57 65 sylib y ω ¬ Fmla y ¬ u Fmla y v Fmla y = u 𝑔 v i ω = 𝑔 i u
67 ioran ¬ Fmla y u Fmla y v Fmla y = u 𝑔 v i ω = 𝑔 i u ¬ Fmla y ¬ u Fmla y v Fmla y = u 𝑔 v i ω = 𝑔 i u
68 36 66 67 sylanbrc y ω ¬ Fmla y ¬ Fmla y u Fmla y v Fmla y = u 𝑔 v i ω = 𝑔 i u
69 fmlasuc y ω Fmla suc y = Fmla y x | u Fmla y v Fmla y x = u 𝑔 v i ω x = 𝑔 i u
70 69 eleq2d y ω Fmla suc y Fmla y x | u Fmla y v Fmla y x = u 𝑔 v i ω x = 𝑔 i u
71 elun Fmla y x | u Fmla y v Fmla y x = u 𝑔 v i ω x = 𝑔 i u Fmla y x | u Fmla y v Fmla y x = u 𝑔 v i ω x = 𝑔 i u
72 eqeq1 x = x = u 𝑔 v = u 𝑔 v
73 72 rexbidv x = v Fmla y x = u 𝑔 v v Fmla y = u 𝑔 v
74 eqeq1 x = x = 𝑔 i u = 𝑔 i u
75 74 rexbidv x = i ω x = 𝑔 i u i ω = 𝑔 i u
76 73 75 orbi12d x = v Fmla y x = u 𝑔 v i ω x = 𝑔 i u v Fmla y = u 𝑔 v i ω = 𝑔 i u
77 76 rexbidv x = u Fmla y v Fmla y x = u 𝑔 v i ω x = 𝑔 i u u Fmla y v Fmla y = u 𝑔 v i ω = 𝑔 i u
78 13 77 elab x | u Fmla y v Fmla y x = u 𝑔 v i ω x = 𝑔 i u u Fmla y v Fmla y = u 𝑔 v i ω = 𝑔 i u
79 78 orbi2i Fmla y x | u Fmla y v Fmla y x = u 𝑔 v i ω x = 𝑔 i u Fmla y u Fmla y v Fmla y = u 𝑔 v i ω = 𝑔 i u
80 71 79 bitri Fmla y x | u Fmla y v Fmla y x = u 𝑔 v i ω x = 𝑔 i u Fmla y u Fmla y v Fmla y = u 𝑔 v i ω = 𝑔 i u
81 70 80 bitrdi y ω Fmla suc y Fmla y u Fmla y v Fmla y = u 𝑔 v i ω = 𝑔 i u
82 81 adantr y ω ¬ Fmla y Fmla suc y Fmla y u Fmla y v Fmla y = u 𝑔 v i ω = 𝑔 i u
83 68 82 mtbird y ω ¬ Fmla y ¬ Fmla suc y
84 83 ex y ω ¬ Fmla y ¬ Fmla suc y
85 3 6 9 12 35 84 finds N ω ¬ Fmla N
86 df-nel Fmla N ¬ Fmla N
87 85 86 sylibr N ω Fmla N