Step |
Hyp |
Ref |
Expression |
1 |
|
df-goal |
|- A.g i A = <. 2o , <. i , A >. >. |
2 |
|
2on0 |
|- 2o =/= (/) |
3 |
2
|
neii |
|- -. 2o = (/) |
4 |
3
|
intnanr |
|- -. ( 2o = (/) /\ <. i , A >. = <. k , j >. ) |
5 |
|
2oex |
|- 2o e. _V |
6 |
|
opex |
|- <. i , A >. e. _V |
7 |
5 6
|
opth |
|- ( <. 2o , <. i , A >. >. = <. (/) , <. k , j >. >. <-> ( 2o = (/) /\ <. i , A >. = <. k , j >. ) ) |
8 |
4 7
|
mtbir |
|- -. <. 2o , <. i , A >. >. = <. (/) , <. k , j >. >. |
9 |
|
goel |
|- ( ( k e. _om /\ j e. _om ) -> ( k e.g j ) = <. (/) , <. k , j >. >. ) |
10 |
9
|
eqeq2d |
|- ( ( k e. _om /\ j e. _om ) -> ( <. 2o , <. i , A >. >. = ( k e.g j ) <-> <. 2o , <. i , A >. >. = <. (/) , <. k , j >. >. ) ) |
11 |
8 10
|
mtbiri |
|- ( ( k e. _om /\ j e. _om ) -> -. <. 2o , <. i , A >. >. = ( k e.g j ) ) |
12 |
11
|
rgen2 |
|- A. k e. _om A. j e. _om -. <. 2o , <. i , A >. >. = ( k e.g j ) |
13 |
|
ralnex2 |
|- ( A. k e. _om A. j e. _om -. <. 2o , <. i , A >. >. = ( k e.g j ) <-> -. E. k e. _om E. j e. _om <. 2o , <. i , A >. >. = ( k e.g j ) ) |
14 |
12 13
|
mpbi |
|- -. E. k e. _om E. j e. _om <. 2o , <. i , A >. >. = ( k e.g j ) |
15 |
14
|
intnan |
|- -. ( <. 2o , <. i , A >. >. e. _V /\ E. k e. _om E. j e. _om <. 2o , <. i , A >. >. = ( k e.g j ) ) |
16 |
|
eqeq1 |
|- ( x = <. 2o , <. i , A >. >. -> ( x = ( k e.g j ) <-> <. 2o , <. i , A >. >. = ( k e.g j ) ) ) |
17 |
16
|
2rexbidv |
|- ( x = <. 2o , <. i , A >. >. -> ( E. k e. _om E. j e. _om x = ( k e.g j ) <-> E. k e. _om E. j e. _om <. 2o , <. i , A >. >. = ( k e.g j ) ) ) |
18 |
|
fmla0 |
|- ( Fmla ` (/) ) = { x e. _V | E. k e. _om E. j e. _om x = ( k e.g j ) } |
19 |
17 18
|
elrab2 |
|- ( <. 2o , <. i , A >. >. e. ( Fmla ` (/) ) <-> ( <. 2o , <. i , A >. >. e. _V /\ E. k e. _om E. j e. _om <. 2o , <. i , A >. >. = ( k e.g j ) ) ) |
20 |
15 19
|
mtbir |
|- -. <. 2o , <. i , A >. >. e. ( Fmla ` (/) ) |
21 |
1 20
|
eqneltri |
|- -. A.g i A e. ( Fmla ` (/) ) |
22 |
|
fveq2 |
|- ( N = (/) -> ( Fmla ` N ) = ( Fmla ` (/) ) ) |
23 |
22
|
eleq2d |
|- ( N = (/) -> ( A.g i A e. ( Fmla ` N ) <-> A.g i A e. ( Fmla ` (/) ) ) ) |
24 |
21 23
|
mtbiri |
|- ( N = (/) -> -. A.g i A e. ( Fmla ` N ) ) |
25 |
24
|
necon2ai |
|- ( A.g i A e. ( Fmla ` N ) -> N =/= (/) ) |