Step |
Hyp |
Ref |
Expression |
1 |
|
onssi.1 |
|- A e. On |
2 |
1
|
onirri |
|- -. A e. A |
3 |
|
id |
|- ( A = U. A -> A = U. A ) |
4 |
|
df-suc |
|- suc x = ( x u. { x } ) |
5 |
4
|
eqeq2i |
|- ( A = suc x <-> A = ( x u. { x } ) ) |
6 |
|
unieq |
|- ( A = ( x u. { x } ) -> U. A = U. ( x u. { x } ) ) |
7 |
5 6
|
sylbi |
|- ( A = suc x -> U. A = U. ( x u. { x } ) ) |
8 |
|
uniun |
|- U. ( x u. { x } ) = ( U. x u. U. { x } ) |
9 |
|
unisnv |
|- U. { x } = x |
10 |
9
|
uneq2i |
|- ( U. x u. U. { x } ) = ( U. x u. x ) |
11 |
8 10
|
eqtri |
|- U. ( x u. { x } ) = ( U. x u. x ) |
12 |
7 11
|
eqtrdi |
|- ( A = suc x -> U. A = ( U. x u. x ) ) |
13 |
|
tron |
|- Tr On |
14 |
|
eleq1 |
|- ( A = suc x -> ( A e. On <-> suc x e. On ) ) |
15 |
1 14
|
mpbii |
|- ( A = suc x -> suc x e. On ) |
16 |
|
trsuc |
|- ( ( Tr On /\ suc x e. On ) -> x e. On ) |
17 |
13 15 16
|
sylancr |
|- ( A = suc x -> x e. On ) |
18 |
|
ontr |
|- ( x e. On -> Tr x ) |
19 |
|
df-tr |
|- ( Tr x <-> U. x C_ x ) |
20 |
18 19
|
sylib |
|- ( x e. On -> U. x C_ x ) |
21 |
17 20
|
syl |
|- ( A = suc x -> U. x C_ x ) |
22 |
|
ssequn1 |
|- ( U. x C_ x <-> ( U. x u. x ) = x ) |
23 |
21 22
|
sylib |
|- ( A = suc x -> ( U. x u. x ) = x ) |
24 |
12 23
|
eqtrd |
|- ( A = suc x -> U. A = x ) |
25 |
3 24
|
sylan9eqr |
|- ( ( A = suc x /\ A = U. A ) -> A = x ) |
26 |
|
vex |
|- x e. _V |
27 |
26
|
sucid |
|- x e. suc x |
28 |
|
eleq2 |
|- ( A = suc x -> ( x e. A <-> x e. suc x ) ) |
29 |
27 28
|
mpbiri |
|- ( A = suc x -> x e. A ) |
30 |
29
|
adantr |
|- ( ( A = suc x /\ A = U. A ) -> x e. A ) |
31 |
25 30
|
eqeltrd |
|- ( ( A = suc x /\ A = U. A ) -> A e. A ) |
32 |
2 31
|
mto |
|- -. ( A = suc x /\ A = U. A ) |
33 |
32
|
imnani |
|- ( A = suc x -> -. A = U. A ) |
34 |
33
|
rexlimivw |
|- ( E. x e. On A = suc x -> -. A = U. A ) |
35 |
|
onuni |
|- ( A e. On -> U. A e. On ) |
36 |
1 35
|
ax-mp |
|- U. A e. On |
37 |
|
onuniorsuc |
|- ( A e. On -> ( A = U. A \/ A = suc U. A ) ) |
38 |
1 37
|
ax-mp |
|- ( A = U. A \/ A = suc U. A ) |
39 |
38
|
ori |
|- ( -. A = U. A -> A = suc U. A ) |
40 |
|
suceq |
|- ( x = U. A -> suc x = suc U. A ) |
41 |
40
|
rspceeqv |
|- ( ( U. A e. On /\ A = suc U. A ) -> E. x e. On A = suc x ) |
42 |
36 39 41
|
sylancr |
|- ( -. A = U. A -> E. x e. On A = suc x ) |
43 |
34 42
|
impbii |
|- ( E. x e. On A = suc x <-> -. A = U. A ) |
44 |
43
|
con2bii |
|- ( A = U. A <-> -. E. x e. On A = suc x ) |