Step |
Hyp |
Ref |
Expression |
1 |
|
df-rmo |
|- ( E* x e. A y e. x <-> E* x ( x e. A /\ y e. x ) ) |
2 |
1
|
albii |
|- ( A. y E* x e. A y e. x <-> A. y E* x ( x e. A /\ y e. x ) ) |
3 |
|
undif2 |
|- ( { (/) } u. ( A \ { (/) } ) ) = ( { (/) } u. A ) |
4 |
|
omex |
|- _om e. _V |
5 |
|
peano1 |
|- (/) e. _om |
6 |
|
snssi |
|- ( (/) e. _om -> { (/) } C_ _om ) |
7 |
5 6
|
ax-mp |
|- { (/) } C_ _om |
8 |
|
ssdomg |
|- ( _om e. _V -> ( { (/) } C_ _om -> { (/) } ~<_ _om ) ) |
9 |
4 7 8
|
mp2 |
|- { (/) } ~<_ _om |
10 |
|
id |
|- ( J e. 2ndc -> J e. 2ndc ) |
11 |
|
ssdif |
|- ( A C_ J -> ( A \ { (/) } ) C_ ( J \ { (/) } ) ) |
12 |
|
dfss3 |
|- ( ( A \ { (/) } ) C_ ( J \ { (/) } ) <-> A. x e. ( A \ { (/) } ) x e. ( J \ { (/) } ) ) |
13 |
11 12
|
sylib |
|- ( A C_ J -> A. x e. ( A \ { (/) } ) x e. ( J \ { (/) } ) ) |
14 |
|
eldifi |
|- ( x e. ( A \ { (/) } ) -> x e. A ) |
15 |
14
|
anim1i |
|- ( ( x e. ( A \ { (/) } ) /\ y e. x ) -> ( x e. A /\ y e. x ) ) |
16 |
15
|
moimi |
|- ( E* x ( x e. A /\ y e. x ) -> E* x ( x e. ( A \ { (/) } ) /\ y e. x ) ) |
17 |
16
|
alimi |
|- ( A. y E* x ( x e. A /\ y e. x ) -> A. y E* x ( x e. ( A \ { (/) } ) /\ y e. x ) ) |
18 |
|
df-rmo |
|- ( E* x e. ( A \ { (/) } ) y e. x <-> E* x ( x e. ( A \ { (/) } ) /\ y e. x ) ) |
19 |
18
|
albii |
|- ( A. y E* x e. ( A \ { (/) } ) y e. x <-> A. y E* x ( x e. ( A \ { (/) } ) /\ y e. x ) ) |
20 |
|
2ndcdisj |
|- ( ( J e. 2ndc /\ A. x e. ( A \ { (/) } ) x e. ( J \ { (/) } ) /\ A. y E* x e. ( A \ { (/) } ) y e. x ) -> ( A \ { (/) } ) ~<_ _om ) |
21 |
19 20
|
syl3an3br |
|- ( ( J e. 2ndc /\ A. x e. ( A \ { (/) } ) x e. ( J \ { (/) } ) /\ A. y E* x ( x e. ( A \ { (/) } ) /\ y e. x ) ) -> ( A \ { (/) } ) ~<_ _om ) |
22 |
10 13 17 21
|
syl3an |
|- ( ( J e. 2ndc /\ A C_ J /\ A. y E* x ( x e. A /\ y e. x ) ) -> ( A \ { (/) } ) ~<_ _om ) |
23 |
|
unctb |
|- ( ( { (/) } ~<_ _om /\ ( A \ { (/) } ) ~<_ _om ) -> ( { (/) } u. ( A \ { (/) } ) ) ~<_ _om ) |
24 |
9 22 23
|
sylancr |
|- ( ( J e. 2ndc /\ A C_ J /\ A. y E* x ( x e. A /\ y e. x ) ) -> ( { (/) } u. ( A \ { (/) } ) ) ~<_ _om ) |
25 |
3 24
|
eqbrtrrid |
|- ( ( J e. 2ndc /\ A C_ J /\ A. y E* x ( x e. A /\ y e. x ) ) -> ( { (/) } u. A ) ~<_ _om ) |
26 |
|
ctex |
|- ( ( { (/) } u. A ) ~<_ _om -> ( { (/) } u. A ) e. _V ) |
27 |
25 26
|
syl |
|- ( ( J e. 2ndc /\ A C_ J /\ A. y E* x ( x e. A /\ y e. x ) ) -> ( { (/) } u. A ) e. _V ) |
28 |
|
ssun2 |
|- A C_ ( { (/) } u. A ) |
29 |
|
ssdomg |
|- ( ( { (/) } u. A ) e. _V -> ( A C_ ( { (/) } u. A ) -> A ~<_ ( { (/) } u. A ) ) ) |
30 |
27 28 29
|
mpisyl |
|- ( ( J e. 2ndc /\ A C_ J /\ A. y E* x ( x e. A /\ y e. x ) ) -> A ~<_ ( { (/) } u. A ) ) |
31 |
|
domtr |
|- ( ( A ~<_ ( { (/) } u. A ) /\ ( { (/) } u. A ) ~<_ _om ) -> A ~<_ _om ) |
32 |
30 25 31
|
syl2anc |
|- ( ( J e. 2ndc /\ A C_ J /\ A. y E* x ( x e. A /\ y e. x ) ) -> A ~<_ _om ) |
33 |
2 32
|
syl3an3b |
|- ( ( J e. 2ndc /\ A C_ J /\ A. y E* x e. A y e. x ) -> A ~<_ _om ) |