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 e. _om -> ( ( Fmla ` suc N ) i^i { x | ( E. u e. ( ( Fmla ` suc N ) \ ( Fmla ` N ) ) ( E. v e. ( Fmla ` suc N ) x = ( u |g v ) \/ E. i e. _om x = A.g i u ) \/ E. u e. ( Fmla ` N ) E. v e. ( ( Fmla ` suc N ) \ ( Fmla ` N ) ) x = ( u |g v ) ) } ) = (/) )

Proof

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