Step |
Hyp |
Ref |
Expression |
1 |
|
0ex |
|- (/) e. _V |
2 |
1
|
a1i |
|- ( -. A e. Fin -> (/) e. _V ) |
3 |
|
xpsneng |
|- ( ( A e. GCH /\ (/) e. _V ) -> ( A X. { (/) } ) ~~ A ) |
4 |
2 3
|
sylan2 |
|- ( ( A e. GCH /\ -. A e. Fin ) -> ( A X. { (/) } ) ~~ A ) |
5 |
4
|
ensymd |
|- ( ( A e. GCH /\ -. A e. Fin ) -> A ~~ ( A X. { (/) } ) ) |
6 |
|
df1o2 |
|- 1o = { (/) } |
7 |
|
id |
|- ( A = (/) -> A = (/) ) |
8 |
|
0fin |
|- (/) e. Fin |
9 |
7 8
|
eqeltrdi |
|- ( A = (/) -> A e. Fin ) |
10 |
9
|
necon3bi |
|- ( -. A e. Fin -> A =/= (/) ) |
11 |
10
|
adantl |
|- ( ( A e. GCH /\ -. A e. Fin ) -> A =/= (/) ) |
12 |
|
0sdomg |
|- ( A e. GCH -> ( (/) ~< A <-> A =/= (/) ) ) |
13 |
12
|
adantr |
|- ( ( A e. GCH /\ -. A e. Fin ) -> ( (/) ~< A <-> A =/= (/) ) ) |
14 |
11 13
|
mpbird |
|- ( ( A e. GCH /\ -. A e. Fin ) -> (/) ~< A ) |
15 |
|
0sdom1dom |
|- ( (/) ~< A <-> 1o ~<_ A ) |
16 |
14 15
|
sylib |
|- ( ( A e. GCH /\ -. A e. Fin ) -> 1o ~<_ A ) |
17 |
6 16
|
eqbrtrrid |
|- ( ( A e. GCH /\ -. A e. Fin ) -> { (/) } ~<_ A ) |
18 |
|
xpdom2g |
|- ( ( A e. GCH /\ { (/) } ~<_ A ) -> ( A X. { (/) } ) ~<_ ( A X. A ) ) |
19 |
17 18
|
syldan |
|- ( ( A e. GCH /\ -. A e. Fin ) -> ( A X. { (/) } ) ~<_ ( A X. A ) ) |
20 |
|
endomtr |
|- ( ( A ~~ ( A X. { (/) } ) /\ ( A X. { (/) } ) ~<_ ( A X. A ) ) -> A ~<_ ( A X. A ) ) |
21 |
5 19 20
|
syl2anc |
|- ( ( A e. GCH /\ -. A e. Fin ) -> A ~<_ ( A X. A ) ) |
22 |
|
canth2g |
|- ( A e. GCH -> A ~< ~P A ) |
23 |
22
|
adantr |
|- ( ( A e. GCH /\ -. A e. Fin ) -> A ~< ~P A ) |
24 |
|
sdomdom |
|- ( A ~< ~P A -> A ~<_ ~P A ) |
25 |
23 24
|
syl |
|- ( ( A e. GCH /\ -. A e. Fin ) -> A ~<_ ~P A ) |
26 |
|
xpdom1g |
|- ( ( A e. GCH /\ A ~<_ ~P A ) -> ( A X. A ) ~<_ ( ~P A X. A ) ) |
27 |
25 26
|
syldan |
|- ( ( A e. GCH /\ -. A e. Fin ) -> ( A X. A ) ~<_ ( ~P A X. A ) ) |
28 |
|
pwexg |
|- ( A e. GCH -> ~P A e. _V ) |
29 |
28
|
adantr |
|- ( ( A e. GCH /\ -. A e. Fin ) -> ~P A e. _V ) |
30 |
|
xpdom2g |
|- ( ( ~P A e. _V /\ A ~<_ ~P A ) -> ( ~P A X. A ) ~<_ ( ~P A X. ~P A ) ) |
31 |
29 25 30
|
syl2anc |
|- ( ( A e. GCH /\ -. A e. Fin ) -> ( ~P A X. A ) ~<_ ( ~P A X. ~P A ) ) |
32 |
|
domtr |
|- ( ( ( A X. A ) ~<_ ( ~P A X. A ) /\ ( ~P A X. A ) ~<_ ( ~P A X. ~P A ) ) -> ( A X. A ) ~<_ ( ~P A X. ~P A ) ) |
33 |
27 31 32
|
syl2anc |
|- ( ( A e. GCH /\ -. A e. Fin ) -> ( A X. A ) ~<_ ( ~P A X. ~P A ) ) |
34 |
|
simpl |
|- ( ( A e. GCH /\ -. A e. Fin ) -> A e. GCH ) |
35 |
|
pwdjuen |
|- ( ( A e. GCH /\ A e. GCH ) -> ~P ( A |_| A ) ~~ ( ~P A X. ~P A ) ) |
36 |
34 35
|
syldan |
|- ( ( A e. GCH /\ -. A e. Fin ) -> ~P ( A |_| A ) ~~ ( ~P A X. ~P A ) ) |
37 |
36
|
ensymd |
|- ( ( A e. GCH /\ -. A e. Fin ) -> ( ~P A X. ~P A ) ~~ ~P ( A |_| A ) ) |
38 |
|
gchdjuidm |
|- ( ( A e. GCH /\ -. A e. Fin ) -> ( A |_| A ) ~~ A ) |
39 |
|
pwen |
|- ( ( A |_| A ) ~~ A -> ~P ( A |_| A ) ~~ ~P A ) |
40 |
38 39
|
syl |
|- ( ( A e. GCH /\ -. A e. Fin ) -> ~P ( A |_| A ) ~~ ~P A ) |
41 |
|
entr |
|- ( ( ( ~P A X. ~P A ) ~~ ~P ( A |_| A ) /\ ~P ( A |_| A ) ~~ ~P A ) -> ( ~P A X. ~P A ) ~~ ~P A ) |
42 |
37 40 41
|
syl2anc |
|- ( ( A e. GCH /\ -. A e. Fin ) -> ( ~P A X. ~P A ) ~~ ~P A ) |
43 |
|
domentr |
|- ( ( ( A X. A ) ~<_ ( ~P A X. ~P A ) /\ ( ~P A X. ~P A ) ~~ ~P A ) -> ( A X. A ) ~<_ ~P A ) |
44 |
33 42 43
|
syl2anc |
|- ( ( A e. GCH /\ -. A e. Fin ) -> ( A X. A ) ~<_ ~P A ) |
45 |
|
gchinf |
|- ( ( A e. GCH /\ -. A e. Fin ) -> _om ~<_ A ) |
46 |
|
pwxpndom |
|- ( _om ~<_ A -> -. ~P A ~<_ ( A X. A ) ) |
47 |
45 46
|
syl |
|- ( ( A e. GCH /\ -. A e. Fin ) -> -. ~P A ~<_ ( A X. A ) ) |
48 |
|
ensym |
|- ( ( A X. A ) ~~ ~P A -> ~P A ~~ ( A X. A ) ) |
49 |
|
endom |
|- ( ~P A ~~ ( A X. A ) -> ~P A ~<_ ( A X. A ) ) |
50 |
48 49
|
syl |
|- ( ( A X. A ) ~~ ~P A -> ~P A ~<_ ( A X. A ) ) |
51 |
47 50
|
nsyl |
|- ( ( A e. GCH /\ -. A e. Fin ) -> -. ( A X. A ) ~~ ~P A ) |
52 |
|
brsdom |
|- ( ( A X. A ) ~< ~P A <-> ( ( A X. A ) ~<_ ~P A /\ -. ( A X. A ) ~~ ~P A ) ) |
53 |
44 51 52
|
sylanbrc |
|- ( ( A e. GCH /\ -. A e. Fin ) -> ( A X. A ) ~< ~P A ) |
54 |
21 53
|
jca |
|- ( ( A e. GCH /\ -. A e. Fin ) -> ( A ~<_ ( A X. A ) /\ ( A X. A ) ~< ~P A ) ) |
55 |
|
gchen1 |
|- ( ( ( A e. GCH /\ -. A e. Fin ) /\ ( A ~<_ ( A X. A ) /\ ( A X. A ) ~< ~P A ) ) -> A ~~ ( A X. A ) ) |
56 |
54 55
|
mpdan |
|- ( ( A e. GCH /\ -. A e. Fin ) -> A ~~ ( A X. A ) ) |
57 |
56
|
ensymd |
|- ( ( A e. GCH /\ -. A e. Fin ) -> ( A X. A ) ~~ A ) |