Step |
Hyp |
Ref |
Expression |
1 |
|
1n0 |
|- 1o =/= (/) |
2 |
1
|
neii |
|- -. 1o = (/) |
3 |
2
|
intnanr |
|- -. ( 1o = (/) /\ <. A , B >. = <. i , j >. ) |
4 |
|
1oex |
|- 1o e. _V |
5 |
|
opex |
|- <. A , B >. e. _V |
6 |
4 5
|
opth |
|- ( <. 1o , <. A , B >. >. = <. (/) , <. i , j >. >. <-> ( 1o = (/) /\ <. A , B >. = <. i , j >. ) ) |
7 |
3 6
|
mtbir |
|- -. <. 1o , <. A , B >. >. = <. (/) , <. i , j >. >. |
8 |
|
goel |
|- ( ( i e. _om /\ j e. _om ) -> ( i e.g j ) = <. (/) , <. i , j >. >. ) |
9 |
8
|
eqeq2d |
|- ( ( i e. _om /\ j e. _om ) -> ( <. 1o , <. A , B >. >. = ( i e.g j ) <-> <. 1o , <. A , B >. >. = <. (/) , <. i , j >. >. ) ) |
10 |
7 9
|
mtbiri |
|- ( ( i e. _om /\ j e. _om ) -> -. <. 1o , <. A , B >. >. = ( i e.g j ) ) |
11 |
10
|
rgen2 |
|- A. i e. _om A. j e. _om -. <. 1o , <. A , B >. >. = ( i e.g j ) |
12 |
|
ralnex2 |
|- ( A. i e. _om A. j e. _om -. <. 1o , <. A , B >. >. = ( i e.g j ) <-> -. E. i e. _om E. j e. _om <. 1o , <. A , B >. >. = ( i e.g j ) ) |
13 |
11 12
|
mpbi |
|- -. E. i e. _om E. j e. _om <. 1o , <. A , B >. >. = ( i e.g j ) |
14 |
13
|
intnan |
|- -. ( <. 1o , <. A , B >. >. e. _V /\ E. i e. _om E. j e. _om <. 1o , <. A , B >. >. = ( i e.g j ) ) |
15 |
|
eqeq1 |
|- ( x = <. 1o , <. A , B >. >. -> ( x = ( i e.g j ) <-> <. 1o , <. A , B >. >. = ( i e.g j ) ) ) |
16 |
15
|
2rexbidv |
|- ( x = <. 1o , <. A , B >. >. -> ( E. i e. _om E. j e. _om x = ( i e.g j ) <-> E. i e. _om E. j e. _om <. 1o , <. A , B >. >. = ( i e.g j ) ) ) |
17 |
|
fmla0 |
|- ( Fmla ` (/) ) = { x e. _V | E. i e. _om E. j e. _om x = ( i e.g j ) } |
18 |
16 17
|
elrab2 |
|- ( <. 1o , <. A , B >. >. e. ( Fmla ` (/) ) <-> ( <. 1o , <. A , B >. >. e. _V /\ E. i e. _om E. j e. _om <. 1o , <. A , B >. >. = ( i e.g j ) ) ) |
19 |
14 18
|
mtbir |
|- -. <. 1o , <. A , B >. >. e. ( Fmla ` (/) ) |
20 |
|
gonafv |
|- ( ( A e. _V /\ B e. _V ) -> ( A |g B ) = <. 1o , <. A , B >. >. ) |
21 |
20
|
eleq1d |
|- ( ( A e. _V /\ B e. _V ) -> ( ( A |g B ) e. ( Fmla ` (/) ) <-> <. 1o , <. A , B >. >. e. ( Fmla ` (/) ) ) ) |
22 |
19 21
|
mtbiri |
|- ( ( A e. _V /\ B e. _V ) -> -. ( A |g B ) e. ( Fmla ` (/) ) ) |
23 |
|
eqid |
|- ( x e. ( _V X. _V ) |-> <. 1o , x >. ) = ( x e. ( _V X. _V ) |-> <. 1o , x >. ) |
24 |
23
|
dmmptss |
|- dom ( x e. ( _V X. _V ) |-> <. 1o , x >. ) C_ ( _V X. _V ) |
25 |
|
relxp |
|- Rel ( _V X. _V ) |
26 |
|
relss |
|- ( dom ( x e. ( _V X. _V ) |-> <. 1o , x >. ) C_ ( _V X. _V ) -> ( Rel ( _V X. _V ) -> Rel dom ( x e. ( _V X. _V ) |-> <. 1o , x >. ) ) ) |
27 |
24 25 26
|
mp2 |
|- Rel dom ( x e. ( _V X. _V ) |-> <. 1o , x >. ) |
28 |
|
df-gona |
|- |g = ( x e. ( _V X. _V ) |-> <. 1o , x >. ) |
29 |
28
|
dmeqi |
|- dom |g = dom ( x e. ( _V X. _V ) |-> <. 1o , x >. ) |
30 |
29
|
releqi |
|- ( Rel dom |g <-> Rel dom ( x e. ( _V X. _V ) |-> <. 1o , x >. ) ) |
31 |
27 30
|
mpbir |
|- Rel dom |g |
32 |
31
|
ovprc |
|- ( -. ( A e. _V /\ B e. _V ) -> ( A |g B ) = (/) ) |
33 |
|
peano1 |
|- (/) e. _om |
34 |
|
fmlaomn0 |
|- ( (/) e. _om -> (/) e/ ( Fmla ` (/) ) ) |
35 |
33 34
|
ax-mp |
|- (/) e/ ( Fmla ` (/) ) |
36 |
35
|
neli |
|- -. (/) e. ( Fmla ` (/) ) |
37 |
|
eleq1 |
|- ( ( A |g B ) = (/) -> ( ( A |g B ) e. ( Fmla ` (/) ) <-> (/) e. ( Fmla ` (/) ) ) ) |
38 |
36 37
|
mtbiri |
|- ( ( A |g B ) = (/) -> -. ( A |g B ) e. ( Fmla ` (/) ) ) |
39 |
32 38
|
syl |
|- ( -. ( A e. _V /\ B e. _V ) -> -. ( A |g B ) e. ( Fmla ` (/) ) ) |
40 |
22 39
|
pm2.61i |
|- -. ( A |g B ) e. ( Fmla ` (/) ) |
41 |
|
fveq2 |
|- ( N = (/) -> ( Fmla ` N ) = ( Fmla ` (/) ) ) |
42 |
41
|
eleq2d |
|- ( N = (/) -> ( ( A |g B ) e. ( Fmla ` N ) <-> ( A |g B ) e. ( Fmla ` (/) ) ) ) |
43 |
40 42
|
mtbiri |
|- ( N = (/) -> -. ( A |g B ) e. ( Fmla ` N ) ) |
44 |
43
|
necon2ai |
|- ( ( A |g B ) e. ( Fmla ` N ) -> N =/= (/) ) |