Metamath Proof Explorer


Theorem fmlasucdisj

Description: The valid Godel formulas of height ( N + 1 ) is disjoint with the difference ( ( Fmlasuc suc N ) \ ( Fmlasuc N ) ) , expressed by formulas constructed from Godel-sets for the Sheffer stroke NAND and Godel-set of universal quantification based on the valid Godel formulas of height ( N + 1 ) . (Contributed by AV, 20-Oct-2023)

Ref Expression
Assertion fmlasucdisj N ω Fmla suc N x | u Fmla suc N Fmla N v Fmla suc N x = u 𝑔 v i ω x = 𝑔 i u u Fmla N v Fmla suc N Fmla N x = u 𝑔 v =

Proof

Step Hyp Ref Expression
1 vex f V
2 eqeq1 x = f x = u 𝑔 v f = u 𝑔 v
3 2 rexbidv x = f v Fmla suc N x = u 𝑔 v v Fmla suc N f = u 𝑔 v
4 eqeq1 x = f x = 𝑔 i u f = 𝑔 i u
5 4 rexbidv x = f i ω x = 𝑔 i u i ω f = 𝑔 i u
6 3 5 orbi12d x = f v Fmla suc N x = u 𝑔 v i ω x = 𝑔 i u v Fmla suc N f = u 𝑔 v i ω f = 𝑔 i u
7 6 rexbidv x = f u Fmla suc N Fmla N v Fmla suc N x = u 𝑔 v i ω x = 𝑔 i u u Fmla suc N Fmla N v Fmla suc N f = u 𝑔 v i ω f = 𝑔 i u
8 2 2rexbidv x = f u Fmla N v Fmla suc N Fmla N x = u 𝑔 v u Fmla N v Fmla suc N Fmla N f = u 𝑔 v
9 7 8 orbi12d x = f u Fmla suc N Fmla N v Fmla suc N x = u 𝑔 v i ω x = 𝑔 i u u Fmla N v Fmla suc N Fmla N x = u 𝑔 v u Fmla suc N Fmla N v Fmla suc N f = u 𝑔 v i ω f = 𝑔 i u u Fmla N v Fmla suc N Fmla N f = u 𝑔 v
10 1 9 elab f x | u Fmla suc N Fmla N v Fmla suc N x = u 𝑔 v i ω x = 𝑔 i u u Fmla N v Fmla suc N Fmla N x = u 𝑔 v u Fmla suc N Fmla N v Fmla suc N f = u 𝑔 v i ω f = 𝑔 i u u Fmla N v Fmla suc N Fmla N f = u 𝑔 v
11 gonar N ω u 𝑔 v Fmla N u Fmla N v Fmla N
12 elndif u Fmla N ¬ u Fmla suc N Fmla N
13 12 adantr u Fmla N v Fmla N ¬ u Fmla suc N Fmla N
14 13 intnanrd u Fmla N v Fmla N ¬ u Fmla suc N Fmla N v Fmla suc N
15 11 14 syl N ω u 𝑔 v Fmla N ¬ u Fmla suc N Fmla N v Fmla suc N
16 15 ex N ω u 𝑔 v Fmla N ¬ u Fmla suc N Fmla N v Fmla suc N
17 16 con2d N ω u Fmla suc N Fmla N v Fmla suc N ¬ u 𝑔 v Fmla N
18 17 impl N ω u Fmla suc N Fmla N v Fmla suc N ¬ u 𝑔 v Fmla N
19 elneeldif a Fmla N u Fmla suc N Fmla N a u
20 19 necomd a Fmla N u Fmla suc N Fmla N u a
21 20 ancoms u Fmla suc N Fmla N a Fmla N u a
22 21 neneqd u Fmla suc N Fmla N a Fmla N ¬ u = a
23 22 orcd u Fmla suc N Fmla N a Fmla N ¬ u = a ¬ v = b
24 ianor ¬ u = a v = b ¬ u = a ¬ v = b
25 vex u V
26 vex v V
27 25 26 opth u v = a b u = a v = b
28 24 27 xchnxbir ¬ u v = a b ¬ u = a ¬ v = b
29 23 28 sylibr u Fmla suc N Fmla N a Fmla N ¬ u v = a b
30 29 olcd u Fmla suc N Fmla N a Fmla N ¬ 1 𝑜 = 1 𝑜 ¬ u v = a b
31 ianor ¬ 1 𝑜 = 1 𝑜 u v = a b ¬ 1 𝑜 = 1 𝑜 ¬ u v = a b
32 gonafv u V v V u 𝑔 v = 1 𝑜 u v
33 32 el2v u 𝑔 v = 1 𝑜 u v
34 gonafv a V b V a 𝑔 b = 1 𝑜 a b
35 34 el2v a 𝑔 b = 1 𝑜 a b
36 33 35 eqeq12i u 𝑔 v = a 𝑔 b 1 𝑜 u v = 1 𝑜 a b
37 1oex 1 𝑜 V
38 opex u v V
39 37 38 opth 1 𝑜 u v = 1 𝑜 a b 1 𝑜 = 1 𝑜 u v = a b
40 36 39 bitri u 𝑔 v = a 𝑔 b 1 𝑜 = 1 𝑜 u v = a b
41 31 40 xchnxbir ¬ u 𝑔 v = a 𝑔 b ¬ 1 𝑜 = 1 𝑜 ¬ u v = a b
42 30 41 sylibr u Fmla suc N Fmla N a Fmla N ¬ u 𝑔 v = a 𝑔 b
43 42 ralrimivw u Fmla suc N Fmla N a Fmla N b Fmla N ¬ u 𝑔 v = a 𝑔 b
44 43 ralrimiva u Fmla suc N Fmla N a Fmla N b Fmla N ¬ u 𝑔 v = a 𝑔 b
45 44 adantl N ω u Fmla suc N Fmla N a Fmla N b Fmla N ¬ u 𝑔 v = a 𝑔 b
46 45 adantr N ω u Fmla suc N Fmla N v Fmla suc N a Fmla N b Fmla N ¬ u 𝑔 v = a 𝑔 b
47 gonanegoal u 𝑔 v 𝑔 j a
48 47 neii ¬ u 𝑔 v = 𝑔 j a
49 48 a1i N ω u Fmla suc N Fmla N v Fmla suc N ¬ u 𝑔 v = 𝑔 j a
50 49 ralrimivw N ω u Fmla suc N Fmla N v Fmla suc N j ω ¬ u 𝑔 v = 𝑔 j a
51 50 ralrimivw N ω u Fmla suc N Fmla N v Fmla suc N a Fmla N j ω ¬ u 𝑔 v = 𝑔 j a
52 r19.26 a Fmla N b Fmla N ¬ u 𝑔 v = a 𝑔 b j ω ¬ u 𝑔 v = 𝑔 j a a Fmla N b Fmla N ¬ u 𝑔 v = a 𝑔 b a Fmla N j ω ¬ u 𝑔 v = 𝑔 j a
53 46 51 52 sylanbrc N ω u Fmla suc N Fmla N v Fmla suc N a Fmla N b Fmla N ¬ u 𝑔 v = a 𝑔 b j ω ¬ u 𝑔 v = 𝑔 j a
54 18 53 jca N ω u Fmla suc N Fmla N v Fmla suc N ¬ u 𝑔 v Fmla N a Fmla N b Fmla N ¬ u 𝑔 v = a 𝑔 b j ω ¬ u 𝑔 v = 𝑔 j a
55 eleq1 f = u 𝑔 v f Fmla N u 𝑔 v Fmla N
56 55 notbid f = u 𝑔 v ¬ f Fmla N ¬ u 𝑔 v Fmla N
57 eqeq1 f = u 𝑔 v f = a 𝑔 b u 𝑔 v = a 𝑔 b
58 57 notbid f = u 𝑔 v ¬ f = a 𝑔 b ¬ u 𝑔 v = a 𝑔 b
59 58 ralbidv f = u 𝑔 v b Fmla N ¬ f = a 𝑔 b b Fmla N ¬ u 𝑔 v = a 𝑔 b
60 eqeq1 f = u 𝑔 v f = 𝑔 j a u 𝑔 v = 𝑔 j a
61 60 notbid f = u 𝑔 v ¬ f = 𝑔 j a ¬ u 𝑔 v = 𝑔 j a
62 61 ralbidv f = u 𝑔 v j ω ¬ f = 𝑔 j a j ω ¬ u 𝑔 v = 𝑔 j a
63 59 62 anbi12d f = u 𝑔 v b Fmla N ¬ f = a 𝑔 b j ω ¬ f = 𝑔 j a b Fmla N ¬ u 𝑔 v = a 𝑔 b j ω ¬ u 𝑔 v = 𝑔 j a
64 63 ralbidv f = u 𝑔 v a Fmla N b Fmla N ¬ f = a 𝑔 b j ω ¬ f = 𝑔 j a a Fmla N b Fmla N ¬ u 𝑔 v = a 𝑔 b j ω ¬ u 𝑔 v = 𝑔 j a
65 56 64 anbi12d f = u 𝑔 v ¬ f Fmla N a Fmla N b Fmla N ¬ f = a 𝑔 b j ω ¬ f = 𝑔 j a ¬ u 𝑔 v Fmla N a Fmla N b Fmla N ¬ u 𝑔 v = a 𝑔 b j ω ¬ u 𝑔 v = 𝑔 j a
66 54 65 syl5ibrcom N ω u Fmla suc N Fmla N v Fmla suc N f = u 𝑔 v ¬ f Fmla N a Fmla N b Fmla N ¬ f = a 𝑔 b j ω ¬ f = 𝑔 j a
67 66 rexlimdva N ω u Fmla suc N Fmla N v Fmla suc N f = u 𝑔 v ¬ f Fmla N a Fmla N b Fmla N ¬ f = a 𝑔 b j ω ¬ f = 𝑔 j a
68 goalr N ω 𝑔 i u Fmla N u Fmla N
69 68 12 syl N ω 𝑔 i u Fmla N ¬ u Fmla suc N Fmla N
70 69 ex N ω 𝑔 i u Fmla N ¬ u Fmla suc N Fmla N
71 70 con2d N ω u Fmla suc N Fmla N ¬ 𝑔 i u Fmla N
72 71 imp N ω u Fmla suc N Fmla N ¬ 𝑔 i u Fmla N
73 72 adantr N ω u Fmla suc N Fmla N i ω ¬ 𝑔 i u Fmla N
74 gonanegoal a 𝑔 b 𝑔 i u
75 74 nesymi ¬ 𝑔 i u = a 𝑔 b
76 75 a1i N ω u Fmla suc N Fmla N i ω ¬ 𝑔 i u = a 𝑔 b
77 76 ralrimivw N ω u Fmla suc N Fmla N i ω b Fmla N ¬ 𝑔 i u = a 𝑔 b
78 77 ralrimivw N ω u Fmla suc N Fmla N i ω a Fmla N b Fmla N ¬ 𝑔 i u = a 𝑔 b
79 22 olcd u Fmla suc N Fmla N a Fmla N ¬ i = j ¬ u = a
80 ianor ¬ i = j u = a ¬ i = j ¬ u = a
81 vex i V
82 81 25 opth i u = j a i = j u = a
83 80 82 xchnxbir ¬ i u = j a ¬ i = j ¬ u = a
84 79 83 sylibr u Fmla suc N Fmla N a Fmla N ¬ i u = j a
85 84 olcd u Fmla suc N Fmla N a Fmla N ¬ 2 𝑜 = 2 𝑜 ¬ i u = j a
86 ianor ¬ 2 𝑜 = 2 𝑜 i u = j a ¬ 2 𝑜 = 2 𝑜 ¬ i u = j a
87 2oex 2 𝑜 V
88 opex i u V
89 87 88 opth 2 𝑜 i u = 2 𝑜 j a 2 𝑜 = 2 𝑜 i u = j a
90 86 89 xchnxbir ¬ 2 𝑜 i u = 2 𝑜 j a ¬ 2 𝑜 = 2 𝑜 ¬ i u = j a
91 df-goal 𝑔 i u = 2 𝑜 i u
92 df-goal 𝑔 j a = 2 𝑜 j a
93 91 92 eqeq12i 𝑔 i u = 𝑔 j a 2 𝑜 i u = 2 𝑜 j a
94 90 93 xchnxbir ¬ 𝑔 i u = 𝑔 j a ¬ 2 𝑜 = 2 𝑜 ¬ i u = j a
95 85 94 sylibr u Fmla suc N Fmla N a Fmla N ¬ 𝑔 i u = 𝑔 j a
96 95 ralrimivw u Fmla suc N Fmla N a Fmla N j ω ¬ 𝑔 i u = 𝑔 j a
97 96 ralrimiva u Fmla suc N Fmla N a Fmla N j ω ¬ 𝑔 i u = 𝑔 j a
98 97 adantl N ω u Fmla suc N Fmla N a Fmla N j ω ¬ 𝑔 i u = 𝑔 j a
99 98 adantr N ω u Fmla suc N Fmla N i ω a Fmla N j ω ¬ 𝑔 i u = 𝑔 j a
100 r19.26 a Fmla N b Fmla N ¬ 𝑔 i u = a 𝑔 b j ω ¬ 𝑔 i u = 𝑔 j a a Fmla N b Fmla N ¬ 𝑔 i u = a 𝑔 b a Fmla N j ω ¬ 𝑔 i u = 𝑔 j a
101 78 99 100 sylanbrc N ω u Fmla suc N Fmla N i ω a Fmla N b Fmla N ¬ 𝑔 i u = a 𝑔 b j ω ¬ 𝑔 i u = 𝑔 j a
102 73 101 jca N ω u Fmla suc N Fmla N i ω ¬ 𝑔 i u Fmla N a Fmla N b Fmla N ¬ 𝑔 i u = a 𝑔 b j ω ¬ 𝑔 i u = 𝑔 j a
103 eleq1 𝑔 i u = f 𝑔 i u Fmla N f Fmla N
104 103 notbid 𝑔 i u = f ¬ 𝑔 i u Fmla N ¬ f Fmla N
105 eqeq1 𝑔 i u = f 𝑔 i u = a 𝑔 b f = a 𝑔 b
106 105 notbid 𝑔 i u = f ¬ 𝑔 i u = a 𝑔 b ¬ f = a 𝑔 b
107 106 ralbidv 𝑔 i u = f b Fmla N ¬ 𝑔 i u = a 𝑔 b b Fmla N ¬ f = a 𝑔 b
108 eqeq1 𝑔 i u = f 𝑔 i u = 𝑔 j a f = 𝑔 j a
109 108 notbid 𝑔 i u = f ¬ 𝑔 i u = 𝑔 j a ¬ f = 𝑔 j a
110 109 ralbidv 𝑔 i u = f j ω ¬ 𝑔 i u = 𝑔 j a j ω ¬ f = 𝑔 j a
111 107 110 anbi12d 𝑔 i u = f b Fmla N ¬ 𝑔 i u = a 𝑔 b j ω ¬ 𝑔 i u = 𝑔 j a b Fmla N ¬ f = a 𝑔 b j ω ¬ f = 𝑔 j a
112 111 ralbidv 𝑔 i u = f a Fmla N b Fmla N ¬ 𝑔 i u = a 𝑔 b j ω ¬ 𝑔 i u = 𝑔 j a a Fmla N b Fmla N ¬ f = a 𝑔 b j ω ¬ f = 𝑔 j a
113 104 112 anbi12d 𝑔 i u = f ¬ 𝑔 i u Fmla N a Fmla N b Fmla N ¬ 𝑔 i u = a 𝑔 b j ω ¬ 𝑔 i u = 𝑔 j a ¬ f Fmla N a Fmla N b Fmla N ¬ f = a 𝑔 b j ω ¬ f = 𝑔 j a
114 113 eqcoms f = 𝑔 i u ¬ 𝑔 i u Fmla N a Fmla N b Fmla N ¬ 𝑔 i u = a 𝑔 b j ω ¬ 𝑔 i u = 𝑔 j a ¬ f Fmla N a Fmla N b Fmla N ¬ f = a 𝑔 b j ω ¬ f = 𝑔 j a
115 102 114 syl5ibcom N ω u Fmla suc N Fmla N i ω f = 𝑔 i u ¬ f Fmla N a Fmla N b Fmla N ¬ f = a 𝑔 b j ω ¬ f = 𝑔 j a
116 115 rexlimdva N ω u Fmla suc N Fmla N i ω f = 𝑔 i u ¬ f Fmla N a Fmla N b Fmla N ¬ f = a 𝑔 b j ω ¬ f = 𝑔 j a
117 67 116 jaod N ω u Fmla suc N Fmla N v Fmla suc N f = u 𝑔 v i ω f = 𝑔 i u ¬ f Fmla N a Fmla N b Fmla N ¬ f = a 𝑔 b j ω ¬ f = 𝑔 j a
118 117 rexlimdva N ω u Fmla suc N Fmla N v Fmla suc N f = u 𝑔 v i ω f = 𝑔 i u ¬ f Fmla N a Fmla N b Fmla N ¬ f = a 𝑔 b j ω ¬ f = 𝑔 j a
119 elndif v Fmla N ¬ v Fmla suc N Fmla N
120 119 adantl u Fmla N v Fmla N ¬ v Fmla suc N Fmla N
121 120 intnand u Fmla N v Fmla N ¬ u Fmla N v Fmla suc N Fmla N
122 11 121 syl N ω u 𝑔 v Fmla N ¬ u Fmla N v Fmla suc N Fmla N
123 122 ex N ω u 𝑔 v Fmla N ¬ u Fmla N v Fmla suc N Fmla N
124 123 con2d N ω u Fmla N v Fmla suc N Fmla N ¬ u 𝑔 v Fmla N
125 124 impl N ω u Fmla N v Fmla suc N Fmla N ¬ u 𝑔 v Fmla N
126 elneeldif b Fmla N v Fmla suc N Fmla N b v
127 126 necomd b Fmla N v Fmla suc N Fmla N v b
128 127 ancoms v Fmla suc N Fmla N b Fmla N v b
129 128 neneqd v Fmla suc N Fmla N b Fmla N ¬ v = b
130 129 olcd v Fmla suc N Fmla N b Fmla N ¬ u = a ¬ v = b
131 130 28 sylibr v Fmla suc N Fmla N b Fmla N ¬ u v = a b
132 131 intnand v Fmla suc N Fmla N b Fmla N ¬ 1 𝑜 = 1 𝑜 u v = a b
133 132 40 sylnibr v Fmla suc N Fmla N b Fmla N ¬ u 𝑔 v = a 𝑔 b
134 133 ralrimiva v Fmla suc N Fmla N b Fmla N ¬ u 𝑔 v = a 𝑔 b
135 134 ralrimivw v Fmla suc N Fmla N a Fmla N b Fmla N ¬ u 𝑔 v = a 𝑔 b
136 135 adantl N ω u Fmla N v Fmla suc N Fmla N a Fmla N b Fmla N ¬ u 𝑔 v = a 𝑔 b
137 48 a1i N ω u Fmla N v Fmla suc N Fmla N ¬ u 𝑔 v = 𝑔 j a
138 137 ralrimivw N ω u Fmla N v Fmla suc N Fmla N j ω ¬ u 𝑔 v = 𝑔 j a
139 138 ralrimivw N ω u Fmla N v Fmla suc N Fmla N a Fmla N j ω ¬ u 𝑔 v = 𝑔 j a
140 136 139 52 sylanbrc N ω u Fmla N v Fmla suc N Fmla N a Fmla N b Fmla N ¬ u 𝑔 v = a 𝑔 b j ω ¬ u 𝑔 v = 𝑔 j a
141 125 140 jca N ω u Fmla N v Fmla suc N Fmla N ¬ u 𝑔 v Fmla N a Fmla N b Fmla N ¬ u 𝑔 v = a 𝑔 b j ω ¬ u 𝑔 v = 𝑔 j a
142 eleq1 u 𝑔 v = f u 𝑔 v Fmla N f Fmla N
143 142 notbid u 𝑔 v = f ¬ u 𝑔 v Fmla N ¬ f Fmla N
144 eqeq1 u 𝑔 v = f u 𝑔 v = a 𝑔 b f = a 𝑔 b
145 144 notbid u 𝑔 v = f ¬ u 𝑔 v = a 𝑔 b ¬ f = a 𝑔 b
146 145 ralbidv u 𝑔 v = f b Fmla N ¬ u 𝑔 v = a 𝑔 b b Fmla N ¬ f = a 𝑔 b
147 eqeq1 u 𝑔 v = f u 𝑔 v = 𝑔 j a f = 𝑔 j a
148 147 notbid u 𝑔 v = f ¬ u 𝑔 v = 𝑔 j a ¬ f = 𝑔 j a
149 148 ralbidv u 𝑔 v = f j ω ¬ u 𝑔 v = 𝑔 j a j ω ¬ f = 𝑔 j a
150 146 149 anbi12d u 𝑔 v = f b Fmla N ¬ u 𝑔 v = a 𝑔 b j ω ¬ u 𝑔 v = 𝑔 j a b Fmla N ¬ f = a 𝑔 b j ω ¬ f = 𝑔 j a
151 150 ralbidv u 𝑔 v = f a Fmla N b Fmla N ¬ u 𝑔 v = a 𝑔 b j ω ¬ u 𝑔 v = 𝑔 j a a Fmla N b Fmla N ¬ f = a 𝑔 b j ω ¬ f = 𝑔 j a
152 143 151 anbi12d u 𝑔 v = f ¬ u 𝑔 v Fmla N a Fmla N b Fmla N ¬ u 𝑔 v = a 𝑔 b j ω ¬ u 𝑔 v = 𝑔 j a ¬ f Fmla N a Fmla N b Fmla N ¬ f = a 𝑔 b j ω ¬ f = 𝑔 j a
153 152 eqcoms f = u 𝑔 v ¬ u 𝑔 v Fmla N a Fmla N b Fmla N ¬ u 𝑔 v = a 𝑔 b j ω ¬ u 𝑔 v = 𝑔 j a ¬ f Fmla N a Fmla N b Fmla N ¬ f = a 𝑔 b j ω ¬ f = 𝑔 j a
154 141 153 syl5ibcom N ω u Fmla N v Fmla suc N Fmla N f = u 𝑔 v ¬ f Fmla N a Fmla N b Fmla N ¬ f = a 𝑔 b j ω ¬ f = 𝑔 j a
155 154 rexlimdva N ω u Fmla N v Fmla suc N Fmla N f = u 𝑔 v ¬ f Fmla N a Fmla N b Fmla N ¬ f = a 𝑔 b j ω ¬ f = 𝑔 j a
156 155 rexlimdva N ω u Fmla N v Fmla suc N Fmla N f = u 𝑔 v ¬ f Fmla N a Fmla N b Fmla N ¬ f = a 𝑔 b j ω ¬ f = 𝑔 j a
157 118 156 jaod N ω u Fmla suc N Fmla N v Fmla suc N f = u 𝑔 v i ω f = 𝑔 i u u Fmla N v Fmla suc N Fmla N f = u 𝑔 v ¬ f Fmla N a Fmla N b Fmla N ¬ f = a 𝑔 b j ω ¬ f = 𝑔 j a
158 isfmlasuc N ω f V f Fmla suc N f Fmla N a Fmla N b Fmla N f = a 𝑔 b j ω f = 𝑔 j a
159 158 elvd N ω f Fmla suc N f Fmla N a Fmla N b Fmla N f = a 𝑔 b j ω f = 𝑔 j a
160 159 notbid N ω ¬ f Fmla suc N ¬ f Fmla N a Fmla N b Fmla N f = a 𝑔 b j ω f = 𝑔 j a
161 ioran ¬ f Fmla N a Fmla N b Fmla N f = a 𝑔 b j ω f = 𝑔 j a ¬ f Fmla N ¬ a Fmla N b Fmla N f = a 𝑔 b j ω f = 𝑔 j a
162 ralnex b Fmla N ¬ f = a 𝑔 b ¬ b Fmla N f = a 𝑔 b
163 ralnex j ω ¬ f = 𝑔 j a ¬ j ω f = 𝑔 j a
164 162 163 anbi12i b Fmla N ¬ f = a 𝑔 b j ω ¬ f = 𝑔 j a ¬ b Fmla N f = a 𝑔 b ¬ j ω f = 𝑔 j a
165 ioran ¬ b Fmla N f = a 𝑔 b j ω f = 𝑔 j a ¬ b Fmla N f = a 𝑔 b ¬ j ω f = 𝑔 j a
166 164 165 bitr4i b Fmla N ¬ f = a 𝑔 b j ω ¬ f = 𝑔 j a ¬ b Fmla N f = a 𝑔 b j ω f = 𝑔 j a
167 166 ralbii a Fmla N b Fmla N ¬ f = a 𝑔 b j ω ¬ f = 𝑔 j a a Fmla N ¬ b Fmla N f = a 𝑔 b j ω f = 𝑔 j a
168 ralnex a Fmla N ¬ b Fmla N f = a 𝑔 b j ω f = 𝑔 j a ¬ a Fmla N b Fmla N f = a 𝑔 b j ω f = 𝑔 j a
169 167 168 bitr2i ¬ a Fmla N b Fmla N f = a 𝑔 b j ω f = 𝑔 j a a Fmla N b Fmla N ¬ f = a 𝑔 b j ω ¬ f = 𝑔 j a
170 169 anbi2i ¬ f Fmla N ¬ a Fmla N b Fmla N f = a 𝑔 b j ω f = 𝑔 j a ¬ f Fmla N a Fmla N b Fmla N ¬ f = a 𝑔 b j ω ¬ f = 𝑔 j a
171 161 170 bitri ¬ f Fmla N a Fmla N b Fmla N f = a 𝑔 b j ω f = 𝑔 j a ¬ f Fmla N a Fmla N b Fmla N ¬ f = a 𝑔 b j ω ¬ f = 𝑔 j a
172 160 171 bitrdi N ω ¬ f Fmla suc N ¬ f Fmla N a Fmla N b Fmla N ¬ f = a 𝑔 b j ω ¬ f = 𝑔 j a
173 157 172 sylibrd N ω u Fmla suc N Fmla N v Fmla suc N f = u 𝑔 v i ω f = 𝑔 i u u Fmla N v Fmla suc N Fmla N f = u 𝑔 v ¬ f Fmla suc N
174 10 173 syl5bi N ω f x | u Fmla suc N Fmla N v Fmla suc N x = u 𝑔 v i ω x = 𝑔 i u u Fmla N v Fmla suc N Fmla N x = u 𝑔 v ¬ f Fmla suc N
175 174 ralrimiv N ω f x | u Fmla suc N Fmla N v Fmla suc N x = u 𝑔 v i ω x = 𝑔 i u u Fmla N v Fmla suc N Fmla N x = u 𝑔 v ¬ f Fmla suc N
176 disjr Fmla suc N x | u Fmla suc N Fmla N v Fmla suc N x = u 𝑔 v i ω x = 𝑔 i u u Fmla N v Fmla suc N Fmla N x = u 𝑔 v = f x | u Fmla suc N Fmla N v Fmla suc N x = u 𝑔 v i ω x = 𝑔 i u u Fmla N v Fmla suc N Fmla N x = u 𝑔 v ¬ f Fmla suc N
177 175 176 sylibr N ω Fmla suc N x | u Fmla suc N Fmla N v Fmla suc N x = u 𝑔 v i ω x = 𝑔 i u u Fmla N v Fmla suc N Fmla N x = u 𝑔 v =