Step |
Hyp |
Ref |
Expression |
1 |
|
1sdom2 |
|- 1o ~< 2o |
2 |
|
djuxpdom |
|- ( ( 1o ~< A /\ 1o ~< 2o ) -> ( A |_| 2o ) ~<_ ( A X. 2o ) ) |
3 |
1 2
|
mpan2 |
|- ( 1o ~< A -> ( A |_| 2o ) ~<_ ( A X. 2o ) ) |
4 |
|
sdom0 |
|- -. 1o ~< (/) |
5 |
|
breq2 |
|- ( A = (/) -> ( 1o ~< A <-> 1o ~< (/) ) ) |
6 |
4 5
|
mtbiri |
|- ( A = (/) -> -. 1o ~< A ) |
7 |
6
|
con2i |
|- ( 1o ~< A -> -. A = (/) ) |
8 |
|
neq0 |
|- ( -. A = (/) <-> E. x x e. A ) |
9 |
7 8
|
sylib |
|- ( 1o ~< A -> E. x x e. A ) |
10 |
|
relsdom |
|- Rel ~< |
11 |
10
|
brrelex2i |
|- ( 1o ~< A -> A e. _V ) |
12 |
11
|
adantr |
|- ( ( 1o ~< A /\ x e. A ) -> A e. _V ) |
13 |
|
enrefg |
|- ( A e. _V -> A ~~ A ) |
14 |
12 13
|
syl |
|- ( ( 1o ~< A /\ x e. A ) -> A ~~ A ) |
15 |
|
df2o2 |
|- 2o = { (/) , { (/) } } |
16 |
|
pwpw0 |
|- ~P { (/) } = { (/) , { (/) } } |
17 |
15 16
|
eqtr4i |
|- 2o = ~P { (/) } |
18 |
|
0ex |
|- (/) e. _V |
19 |
|
vex |
|- x e. _V |
20 |
|
en2sn |
|- ( ( (/) e. _V /\ x e. _V ) -> { (/) } ~~ { x } ) |
21 |
18 19 20
|
mp2an |
|- { (/) } ~~ { x } |
22 |
|
pwen |
|- ( { (/) } ~~ { x } -> ~P { (/) } ~~ ~P { x } ) |
23 |
21 22
|
ax-mp |
|- ~P { (/) } ~~ ~P { x } |
24 |
17 23
|
eqbrtri |
|- 2o ~~ ~P { x } |
25 |
|
xpen |
|- ( ( A ~~ A /\ 2o ~~ ~P { x } ) -> ( A X. 2o ) ~~ ( A X. ~P { x } ) ) |
26 |
14 24 25
|
sylancl |
|- ( ( 1o ~< A /\ x e. A ) -> ( A X. 2o ) ~~ ( A X. ~P { x } ) ) |
27 |
|
snex |
|- { x } e. _V |
28 |
27
|
pwex |
|- ~P { x } e. _V |
29 |
|
uncom |
|- ( ( A \ { x } ) u. { x } ) = ( { x } u. ( A \ { x } ) ) |
30 |
|
simpr |
|- ( ( 1o ~< A /\ x e. A ) -> x e. A ) |
31 |
30
|
snssd |
|- ( ( 1o ~< A /\ x e. A ) -> { x } C_ A ) |
32 |
|
undif |
|- ( { x } C_ A <-> ( { x } u. ( A \ { x } ) ) = A ) |
33 |
31 32
|
sylib |
|- ( ( 1o ~< A /\ x e. A ) -> ( { x } u. ( A \ { x } ) ) = A ) |
34 |
29 33
|
syl5eq |
|- ( ( 1o ~< A /\ x e. A ) -> ( ( A \ { x } ) u. { x } ) = A ) |
35 |
|
difexg |
|- ( A e. _V -> ( A \ { x } ) e. _V ) |
36 |
12 35
|
syl |
|- ( ( 1o ~< A /\ x e. A ) -> ( A \ { x } ) e. _V ) |
37 |
|
canth2g |
|- ( ( A \ { x } ) e. _V -> ( A \ { x } ) ~< ~P ( A \ { x } ) ) |
38 |
|
domunsn |
|- ( ( A \ { x } ) ~< ~P ( A \ { x } ) -> ( ( A \ { x } ) u. { x } ) ~<_ ~P ( A \ { x } ) ) |
39 |
36 37 38
|
3syl |
|- ( ( 1o ~< A /\ x e. A ) -> ( ( A \ { x } ) u. { x } ) ~<_ ~P ( A \ { x } ) ) |
40 |
34 39
|
eqbrtrrd |
|- ( ( 1o ~< A /\ x e. A ) -> A ~<_ ~P ( A \ { x } ) ) |
41 |
|
xpdom1g |
|- ( ( ~P { x } e. _V /\ A ~<_ ~P ( A \ { x } ) ) -> ( A X. ~P { x } ) ~<_ ( ~P ( A \ { x } ) X. ~P { x } ) ) |
42 |
28 40 41
|
sylancr |
|- ( ( 1o ~< A /\ x e. A ) -> ( A X. ~P { x } ) ~<_ ( ~P ( A \ { x } ) X. ~P { x } ) ) |
43 |
|
endomtr |
|- ( ( ( A X. 2o ) ~~ ( A X. ~P { x } ) /\ ( A X. ~P { x } ) ~<_ ( ~P ( A \ { x } ) X. ~P { x } ) ) -> ( A X. 2o ) ~<_ ( ~P ( A \ { x } ) X. ~P { x } ) ) |
44 |
26 42 43
|
syl2anc |
|- ( ( 1o ~< A /\ x e. A ) -> ( A X. 2o ) ~<_ ( ~P ( A \ { x } ) X. ~P { x } ) ) |
45 |
|
pwdjuen |
|- ( ( ( A \ { x } ) e. _V /\ { x } e. _V ) -> ~P ( ( A \ { x } ) |_| { x } ) ~~ ( ~P ( A \ { x } ) X. ~P { x } ) ) |
46 |
36 27 45
|
sylancl |
|- ( ( 1o ~< A /\ x e. A ) -> ~P ( ( A \ { x } ) |_| { x } ) ~~ ( ~P ( A \ { x } ) X. ~P { x } ) ) |
47 |
46
|
ensymd |
|- ( ( 1o ~< A /\ x e. A ) -> ( ~P ( A \ { x } ) X. ~P { x } ) ~~ ~P ( ( A \ { x } ) |_| { x } ) ) |
48 |
|
domentr |
|- ( ( ( A X. 2o ) ~<_ ( ~P ( A \ { x } ) X. ~P { x } ) /\ ( ~P ( A \ { x } ) X. ~P { x } ) ~~ ~P ( ( A \ { x } ) |_| { x } ) ) -> ( A X. 2o ) ~<_ ~P ( ( A \ { x } ) |_| { x } ) ) |
49 |
44 47 48
|
syl2anc |
|- ( ( 1o ~< A /\ x e. A ) -> ( A X. 2o ) ~<_ ~P ( ( A \ { x } ) |_| { x } ) ) |
50 |
27
|
a1i |
|- ( ( 1o ~< A /\ x e. A ) -> { x } e. _V ) |
51 |
|
incom |
|- ( ( A \ { x } ) i^i { x } ) = ( { x } i^i ( A \ { x } ) ) |
52 |
|
disjdif |
|- ( { x } i^i ( A \ { x } ) ) = (/) |
53 |
51 52
|
eqtri |
|- ( ( A \ { x } ) i^i { x } ) = (/) |
54 |
53
|
a1i |
|- ( ( 1o ~< A /\ x e. A ) -> ( ( A \ { x } ) i^i { x } ) = (/) ) |
55 |
|
endjudisj |
|- ( ( ( A \ { x } ) e. _V /\ { x } e. _V /\ ( ( A \ { x } ) i^i { x } ) = (/) ) -> ( ( A \ { x } ) |_| { x } ) ~~ ( ( A \ { x } ) u. { x } ) ) |
56 |
36 50 54 55
|
syl3anc |
|- ( ( 1o ~< A /\ x e. A ) -> ( ( A \ { x } ) |_| { x } ) ~~ ( ( A \ { x } ) u. { x } ) ) |
57 |
56 34
|
breqtrd |
|- ( ( 1o ~< A /\ x e. A ) -> ( ( A \ { x } ) |_| { x } ) ~~ A ) |
58 |
|
pwen |
|- ( ( ( A \ { x } ) |_| { x } ) ~~ A -> ~P ( ( A \ { x } ) |_| { x } ) ~~ ~P A ) |
59 |
57 58
|
syl |
|- ( ( 1o ~< A /\ x e. A ) -> ~P ( ( A \ { x } ) |_| { x } ) ~~ ~P A ) |
60 |
|
domentr |
|- ( ( ( A X. 2o ) ~<_ ~P ( ( A \ { x } ) |_| { x } ) /\ ~P ( ( A \ { x } ) |_| { x } ) ~~ ~P A ) -> ( A X. 2o ) ~<_ ~P A ) |
61 |
49 59 60
|
syl2anc |
|- ( ( 1o ~< A /\ x e. A ) -> ( A X. 2o ) ~<_ ~P A ) |
62 |
9 61
|
exlimddv |
|- ( 1o ~< A -> ( A X. 2o ) ~<_ ~P A ) |
63 |
|
domtr |
|- ( ( ( A |_| 2o ) ~<_ ( A X. 2o ) /\ ( A X. 2o ) ~<_ ~P A ) -> ( A |_| 2o ) ~<_ ~P A ) |
64 |
3 62 63
|
syl2anc |
|- ( 1o ~< A -> ( A |_| 2o ) ~<_ ~P A ) |