This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )