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 biimtrid 
 |-  ( 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 ) ) } ) = (/) )