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