Metamath Proof Explorer


Theorem fmla0disjsuc

Description: The set of valid Godel formulas of height 0 is disjoint with the formulas constructed from Godel-sets for the Sheffer stroke NAND and Godel-set of universal quantification. (Contributed by AV, 20-Oct-2023)

Ref Expression
Assertion fmla0disjsuc Fmla x | u Fmla v Fmla x = u 𝑔 v i ω x = 𝑔 i u =

Proof

Step Hyp Ref Expression
1 fmla0 Fmla = x V | j ω k ω x = j 𝑔 k
2 rabab x V | j ω k ω x = j 𝑔 k = x | j ω k ω x = j 𝑔 k
3 1 2 eqtri Fmla = x | j ω k ω x = j 𝑔 k
4 3 ineq1i Fmla x | u Fmla v Fmla x = u 𝑔 v i ω x = 𝑔 i u = x | j ω k ω x = j 𝑔 k x | u Fmla v Fmla x = u 𝑔 v i ω x = 𝑔 i u
5 inab x | j ω k ω x = j 𝑔 k x | u Fmla v Fmla x = u 𝑔 v i ω x = 𝑔 i u = x | j ω k ω x = j 𝑔 k u Fmla v Fmla x = u 𝑔 v i ω x = 𝑔 i u
6 goel j ω k ω j 𝑔 k = j k
7 6 eqeq2d j ω k ω x = j 𝑔 k x = j k
8 1n0 1 𝑜
9 8 nesymi ¬ = 1 𝑜
10 9 intnanr ¬ = 1 𝑜 j k = u v
11 gonafv u V v V u 𝑔 v = 1 𝑜 u v
12 11 el2v u 𝑔 v = 1 𝑜 u v
13 12 eqeq2i j k = u 𝑔 v j k = 1 𝑜 u v
14 0ex V
15 opex j k V
16 14 15 opth j k = 1 𝑜 u v = 1 𝑜 j k = u v
17 13 16 bitri j k = u 𝑔 v = 1 𝑜 j k = u v
18 10 17 mtbir ¬ j k = u 𝑔 v
19 eqeq1 x = j k x = u 𝑔 v j k = u 𝑔 v
20 18 19 mtbiri x = j k ¬ x = u 𝑔 v
21 7 20 syl6bi j ω k ω x = j 𝑔 k ¬ x = u 𝑔 v
22 21 imp j ω k ω x = j 𝑔 k ¬ x = u 𝑔 v
23 22 adantr j ω k ω x = j 𝑔 k u Fmla ¬ x = u 𝑔 v
24 23 ralrimivw j ω k ω x = j 𝑔 k u Fmla v Fmla ¬ x = u 𝑔 v
25 2on0 2 𝑜
26 25 nesymi ¬ = 2 𝑜
27 26 orci ¬ = 2 𝑜 ¬ j k = i u
28 14 15 opth j k = 2 𝑜 i u = 2 𝑜 j k = i u
29 28 notbii ¬ j k = 2 𝑜 i u ¬ = 2 𝑜 j k = i u
30 ianor ¬ = 2 𝑜 j k = i u ¬ = 2 𝑜 ¬ j k = i u
31 29 30 bitri ¬ j k = 2 𝑜 i u ¬ = 2 𝑜 ¬ j k = i u
32 27 31 mpbir ¬ j k = 2 𝑜 i u
33 eqeq1 x = j k x = 𝑔 i u j k = 𝑔 i u
34 df-goal 𝑔 i u = 2 𝑜 i u
35 34 eqeq2i j k = 𝑔 i u j k = 2 𝑜 i u
36 33 35 bitrdi x = j k x = 𝑔 i u j k = 2 𝑜 i u
37 32 36 mtbiri x = j k ¬ x = 𝑔 i u
38 7 37 syl6bi j ω k ω x = j 𝑔 k ¬ x = 𝑔 i u
39 38 imp j ω k ω x = j 𝑔 k ¬ x = 𝑔 i u
40 39 adantr j ω k ω x = j 𝑔 k u Fmla ¬ x = 𝑔 i u
41 40 adantr j ω k ω x = j 𝑔 k u Fmla i ω ¬ x = 𝑔 i u
42 41 ralrimiva j ω k ω x = j 𝑔 k u Fmla i ω ¬ x = 𝑔 i u
43 24 42 jca j ω k ω x = j 𝑔 k u Fmla v Fmla ¬ x = u 𝑔 v i ω ¬ x = 𝑔 i u
44 43 ralrimiva j ω k ω x = j 𝑔 k u Fmla v Fmla ¬ x = u 𝑔 v i ω ¬ x = 𝑔 i u
45 ralnex v Fmla ¬ x = u 𝑔 v ¬ v Fmla x = u 𝑔 v
46 ralnex i ω ¬ x = 𝑔 i u ¬ i ω x = 𝑔 i u
47 45 46 anbi12i v Fmla ¬ x = u 𝑔 v i ω ¬ x = 𝑔 i u ¬ v Fmla x = u 𝑔 v ¬ i ω x = 𝑔 i u
48 ioran ¬ v Fmla x = u 𝑔 v i ω x = 𝑔 i u ¬ v Fmla x = u 𝑔 v ¬ i ω x = 𝑔 i u
49 47 48 bitr4i v Fmla ¬ x = u 𝑔 v i ω ¬ x = 𝑔 i u ¬ v Fmla x = u 𝑔 v i ω x = 𝑔 i u
50 49 ralbii u Fmla v Fmla ¬ x = u 𝑔 v i ω ¬ x = 𝑔 i u u Fmla ¬ v Fmla x = u 𝑔 v i ω x = 𝑔 i u
51 ralnex u Fmla ¬ v Fmla x = u 𝑔 v i ω x = 𝑔 i u ¬ u Fmla v Fmla x = u 𝑔 v i ω x = 𝑔 i u
52 50 51 bitri u Fmla v Fmla ¬ x = u 𝑔 v i ω ¬ x = 𝑔 i u ¬ u Fmla v Fmla x = u 𝑔 v i ω x = 𝑔 i u
53 44 52 sylib j ω k ω x = j 𝑔 k ¬ u Fmla v Fmla x = u 𝑔 v i ω x = 𝑔 i u
54 53 ex j ω k ω x = j 𝑔 k ¬ u Fmla v Fmla x = u 𝑔 v i ω x = 𝑔 i u
55 54 rexlimdva j ω k ω x = j 𝑔 k ¬ u Fmla v Fmla x = u 𝑔 v i ω x = 𝑔 i u
56 55 rexlimiv j ω k ω x = j 𝑔 k ¬ u Fmla v Fmla x = u 𝑔 v i ω x = 𝑔 i u
57 56 imori ¬ j ω k ω x = j 𝑔 k ¬ u Fmla v Fmla x = u 𝑔 v i ω x = 𝑔 i u
58 ianor ¬ j ω k ω x = j 𝑔 k u Fmla v Fmla x = u 𝑔 v i ω x = 𝑔 i u ¬ j ω k ω x = j 𝑔 k ¬ u Fmla v Fmla x = u 𝑔 v i ω x = 𝑔 i u
59 57 58 mpbir ¬ j ω k ω x = j 𝑔 k u Fmla v Fmla x = u 𝑔 v i ω x = 𝑔 i u
60 59 abf x | j ω k ω x = j 𝑔 k u Fmla v Fmla x = u 𝑔 v i ω x = 𝑔 i u =
61 5 60 eqtri x | j ω k ω x = j 𝑔 k x | u Fmla v Fmla x = u 𝑔 v i ω x = 𝑔 i u =
62 4 61 eqtri Fmla x | u Fmla v Fmla x = u 𝑔 v i ω x = 𝑔 i u =