Step |
Hyp |
Ref |
Expression |
1 |
|
nodmon |
|- ( A e. No -> dom A e. On ) |
2 |
1
|
3ad2ant1 |
|- ( ( A e. No /\ B e. No /\ dom A e. dom B ) -> dom A e. On ) |
3 |
|
nodmord |
|- ( A e. No -> Ord dom A ) |
4 |
|
ordirr |
|- ( Ord dom A -> -. dom A e. dom A ) |
5 |
3 4
|
syl |
|- ( A e. No -> -. dom A e. dom A ) |
6 |
5
|
3ad2ant1 |
|- ( ( A e. No /\ B e. No /\ dom A e. dom B ) -> -. dom A e. dom A ) |
7 |
|
ndmfv |
|- ( -. dom A e. dom A -> ( A ` dom A ) = (/) ) |
8 |
6 7
|
syl |
|- ( ( A e. No /\ B e. No /\ dom A e. dom B ) -> ( A ` dom A ) = (/) ) |
9 |
|
nosgnn0 |
|- -. (/) e. { 1o , 2o } |
10 |
|
elno3 |
|- ( B e. No <-> ( B : dom B --> { 1o , 2o } /\ dom B e. On ) ) |
11 |
10
|
simplbi |
|- ( B e. No -> B : dom B --> { 1o , 2o } ) |
12 |
11
|
3ad2ant2 |
|- ( ( A e. No /\ B e. No /\ dom A e. dom B ) -> B : dom B --> { 1o , 2o } ) |
13 |
|
simp3 |
|- ( ( A e. No /\ B e. No /\ dom A e. dom B ) -> dom A e. dom B ) |
14 |
12 13
|
ffvelrnd |
|- ( ( A e. No /\ B e. No /\ dom A e. dom B ) -> ( B ` dom A ) e. { 1o , 2o } ) |
15 |
|
eleq1 |
|- ( ( B ` dom A ) = (/) -> ( ( B ` dom A ) e. { 1o , 2o } <-> (/) e. { 1o , 2o } ) ) |
16 |
14 15
|
syl5ibcom |
|- ( ( A e. No /\ B e. No /\ dom A e. dom B ) -> ( ( B ` dom A ) = (/) -> (/) e. { 1o , 2o } ) ) |
17 |
9 16
|
mtoi |
|- ( ( A e. No /\ B e. No /\ dom A e. dom B ) -> -. ( B ` dom A ) = (/) ) |
18 |
17
|
neqned |
|- ( ( A e. No /\ B e. No /\ dom A e. dom B ) -> ( B ` dom A ) =/= (/) ) |
19 |
18
|
necomd |
|- ( ( A e. No /\ B e. No /\ dom A e. dom B ) -> (/) =/= ( B ` dom A ) ) |
20 |
8 19
|
eqnetrd |
|- ( ( A e. No /\ B e. No /\ dom A e. dom B ) -> ( A ` dom A ) =/= ( B ` dom A ) ) |
21 |
|
fveq2 |
|- ( x = dom A -> ( A ` x ) = ( A ` dom A ) ) |
22 |
|
fveq2 |
|- ( x = dom A -> ( B ` x ) = ( B ` dom A ) ) |
23 |
21 22
|
neeq12d |
|- ( x = dom A -> ( ( A ` x ) =/= ( B ` x ) <-> ( A ` dom A ) =/= ( B ` dom A ) ) ) |
24 |
23
|
rspcev |
|- ( ( dom A e. On /\ ( A ` dom A ) =/= ( B ` dom A ) ) -> E. x e. On ( A ` x ) =/= ( B ` x ) ) |
25 |
2 20 24
|
syl2anc |
|- ( ( A e. No /\ B e. No /\ dom A e. dom B ) -> E. x e. On ( A ` x ) =/= ( B ` x ) ) |
26 |
|
df-ne |
|- ( ( A ` x ) =/= ( B ` x ) <-> -. ( A ` x ) = ( B ` x ) ) |
27 |
26
|
rexbii |
|- ( E. x e. On ( A ` x ) =/= ( B ` x ) <-> E. x e. On -. ( A ` x ) = ( B ` x ) ) |
28 |
|
rexnal |
|- ( E. x e. On -. ( A ` x ) = ( B ` x ) <-> -. A. x e. On ( A ` x ) = ( B ` x ) ) |
29 |
27 28
|
bitri |
|- ( E. x e. On ( A ` x ) =/= ( B ` x ) <-> -. A. x e. On ( A ` x ) = ( B ` x ) ) |
30 |
25 29
|
sylib |
|- ( ( A e. No /\ B e. No /\ dom A e. dom B ) -> -. A. x e. On ( A ` x ) = ( B ` x ) ) |