Step |
Hyp |
Ref |
Expression |
1 |
|
en2eleq |
|- ( ( X e. P /\ P ~~ 2o ) -> P = { X , U. ( P \ { X } ) } ) |
2 |
|
prcom |
|- { X , U. ( P \ { X } ) } = { U. ( P \ { X } ) , X } |
3 |
1 2
|
eqtrdi |
|- ( ( X e. P /\ P ~~ 2o ) -> P = { U. ( P \ { X } ) , X } ) |
4 |
3
|
difeq1d |
|- ( ( X e. P /\ P ~~ 2o ) -> ( P \ { U. ( P \ { X } ) } ) = ( { U. ( P \ { X } ) , X } \ { U. ( P \ { X } ) } ) ) |
5 |
|
difprsnss |
|- ( { U. ( P \ { X } ) , X } \ { U. ( P \ { X } ) } ) C_ { X } |
6 |
4 5
|
eqsstrdi |
|- ( ( X e. P /\ P ~~ 2o ) -> ( P \ { U. ( P \ { X } ) } ) C_ { X } ) |
7 |
|
simpl |
|- ( ( X e. P /\ P ~~ 2o ) -> X e. P ) |
8 |
|
1onn |
|- 1o e. _om |
9 |
|
simpr |
|- ( ( X e. P /\ P ~~ 2o ) -> P ~~ 2o ) |
10 |
|
df-2o |
|- 2o = suc 1o |
11 |
9 10
|
breqtrdi |
|- ( ( X e. P /\ P ~~ 2o ) -> P ~~ suc 1o ) |
12 |
|
dif1en |
|- ( ( 1o e. _om /\ P ~~ suc 1o /\ X e. P ) -> ( P \ { X } ) ~~ 1o ) |
13 |
8 11 7 12
|
mp3an2i |
|- ( ( X e. P /\ P ~~ 2o ) -> ( P \ { X } ) ~~ 1o ) |
14 |
|
en1uniel |
|- ( ( P \ { X } ) ~~ 1o -> U. ( P \ { X } ) e. ( P \ { X } ) ) |
15 |
|
eldifsni |
|- ( U. ( P \ { X } ) e. ( P \ { X } ) -> U. ( P \ { X } ) =/= X ) |
16 |
13 14 15
|
3syl |
|- ( ( X e. P /\ P ~~ 2o ) -> U. ( P \ { X } ) =/= X ) |
17 |
16
|
necomd |
|- ( ( X e. P /\ P ~~ 2o ) -> X =/= U. ( P \ { X } ) ) |
18 |
|
eldifsn |
|- ( X e. ( P \ { U. ( P \ { X } ) } ) <-> ( X e. P /\ X =/= U. ( P \ { X } ) ) ) |
19 |
7 17 18
|
sylanbrc |
|- ( ( X e. P /\ P ~~ 2o ) -> X e. ( P \ { U. ( P \ { X } ) } ) ) |
20 |
19
|
snssd |
|- ( ( X e. P /\ P ~~ 2o ) -> { X } C_ ( P \ { U. ( P \ { X } ) } ) ) |
21 |
6 20
|
eqssd |
|- ( ( X e. P /\ P ~~ 2o ) -> ( P \ { U. ( P \ { X } ) } ) = { X } ) |
22 |
21
|
unieqd |
|- ( ( X e. P /\ P ~~ 2o ) -> U. ( P \ { U. ( P \ { X } ) } ) = U. { X } ) |
23 |
|
unisng |
|- ( X e. P -> U. { X } = X ) |
24 |
23
|
adantr |
|- ( ( X e. P /\ P ~~ 2o ) -> U. { X } = X ) |
25 |
22 24
|
eqtrd |
|- ( ( X e. P /\ P ~~ 2o ) -> U. ( P \ { U. ( P \ { X } ) } ) = X ) |