Theorem pwdjudom

Description: A property of dominance over a powerset, and a main lemma for gchac . Similar to Lemma 2.3 of KanamoriPincus p. 420. (Contributed by Mario Carneiro, 15-May-2015)

	Ref	Expression
Assertion	pwdjudom	|- ( ~P ( A |_| A ) ~<_ ( A |_| B ) -> ~P A ~<_ B )

Proof

Step	Hyp	Ref	Expression
1		canthwdom	|- -. ~P A ~<_* A
2		0ex	|- (/) e. _V
3		reldom	|- Rel ~<_
4	3	brrelex2i	|- ( ~P ( A |_| A ) ~<_ ( A |_| B ) -> ( A |_| B ) e. _V )
5		djuexb	|- ( ( A e. _V /\ B e. _V ) <-> ( A |_| B ) e. _V )
6	4 5	sylibr	|- ( ~P ( A |_| A ) ~<_ ( A |_| B ) -> ( A e. _V /\ B e. _V ) )
7	6	simpld	|- ( ~P ( A |_| A ) ~<_ ( A |_| B ) -> A e. _V )
8		xpsnen2g	|- ( ( (/) e. _V /\ A e. _V ) -> ( { (/) } X. A ) ~~ A )
9	2 7 8	sylancr	|- ( ~P ( A |_| A ) ~<_ ( A |_| B ) -> ( { (/) } X. A ) ~~ A )
10		endom	|- ( ( { (/) } X. A ) ~~ A -> ( { (/) } X. A ) ~<_ A )
11		domwdom	|- ( ( { (/) } X. A ) ~<_ A -> ( { (/) } X. A ) ~<_* A )
12		wdomtr	|- ( ( ~P A ~<_* ( { (/) } X. A ) /\ ( { (/) } X. A ) ~<_* A ) -> ~P A ~<_* A )
13	12	expcom	|- ( ( { (/) } X. A ) ~<_* A -> ( ~P A ~<_* ( { (/) } X. A ) -> ~P A ~<_* A ) )
14	9 10 11 13	4syl	|- ( ~P ( A |_| A ) ~<_ ( A |_| B ) -> ( ~P A ~<_* ( { (/) } X. A ) -> ~P A ~<_* A ) )
15	1 14	mtoi	|- ( ~P ( A |_| A ) ~<_ ( A |_| B ) -> -. ~P A ~<_* ( { (/) } X. A ) )
16		pwdjuen	|- ( ( A e. _V /\ A e. _V ) -> ~P ( A |_| A ) ~~ ( ~P A X. ~P A ) )
17	7 7 16	syl2anc	|- ( ~P ( A |_| A ) ~<_ ( A |_| B ) -> ~P ( A |_| A ) ~~ ( ~P A X. ~P A ) )
18		domen1	|- ( ~P ( A |_| A ) ~~ ( ~P A X. ~P A ) -> ( ~P ( A |_| A ) ~<_ ( A |_| B ) <-> ( ~P A X. ~P A ) ~<_ ( A |_| B ) ) )
19	17 18	syl	|- ( ~P ( A |_| A ) ~<_ ( A |_| B ) -> ( ~P ( A |_| A ) ~<_ ( A |_| B ) <-> ( ~P A X. ~P A ) ~<_ ( A |_| B ) ) )
20	19	ibi	|- ( ~P ( A |_| A ) ~<_ ( A |_| B ) -> ( ~P A X. ~P A ) ~<_ ( A |_| B ) )
21		df-dju	|- ( A |_| B ) = ( ( { (/) } X. A ) u. ( { 1o } X. B ) )
22	20 21	breqtrdi	|- ( ~P ( A |_| A ) ~<_ ( A |_| B ) -> ( ~P A X. ~P A ) ~<_ ( ( { (/) } X. A ) u. ( { 1o } X. B ) ) )
23		unxpwdom	|- ( ( ~P A X. ~P A ) ~<_ ( ( { (/) } X. A ) u. ( { 1o } X. B ) ) -> ( ~P A ~<_* ( { (/) } X. A ) \/ ~P A ~<_ ( { 1o } X. B ) ) )
24	22 23	syl	|- ( ~P ( A |_| A ) ~<_ ( A |_| B ) -> ( ~P A ~<_* ( { (/) } X. A ) \/ ~P A ~<_ ( { 1o } X. B ) ) )
25	24	ord	|- ( ~P ( A |_| A ) ~<_ ( A |_| B ) -> ( -. ~P A ~<_* ( { (/) } X. A ) -> ~P A ~<_ ( { 1o } X. B ) ) )
26	15 25	mpd	|- ( ~P ( A |_| A ) ~<_ ( A |_| B ) -> ~P A ~<_ ( { 1o } X. B ) )
27		1on	|- 1o e. On
28	6	simprd	|- ( ~P ( A |_| A ) ~<_ ( A |_| B ) -> B e. _V )
29		xpsnen2g	|- ( ( 1o e. On /\ B e. _V ) -> ( { 1o } X. B ) ~~ B )
30	27 28 29	sylancr	|- ( ~P ( A |_| A ) ~<_ ( A |_| B ) -> ( { 1o } X. B ) ~~ B )
31		domentr	|- ( ( ~P A ~<_ ( { 1o } X. B ) /\ ( { 1o } X. B ) ~~ B ) -> ~P A ~<_ B )
32	26 30 31	syl2anc	|- ( ~P ( A |_| A ) ~<_ ( A |_| B ) -> ~P A ~<_ B )