Metamath Proof Explorer

Theorem canthp1lem1

Description: Lemma for canthp1 . (Contributed by Mario Carneiro, 18-May-2015)

Ref Expression
Assertion canthp1lem1 
|- ( 1o ~< A -> ( A |_| 2o ) ~<_ ~P A )

Proof

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 vsnex 
 |-  { 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 eqtrid 
 |-  ( ( 1o ~< A /\ x e. A ) -> ( ( A \ { x } ) u. { x } ) = A )
35 12 difexd 
 |-  ( ( 1o ~< A /\ x e. A ) -> ( A \ { x } ) e. _V )
36 canth2g 
 |-  ( ( A \ { x } ) e. _V -> ( A \ { x } ) ~< ~P ( A \ { x } ) )
37 domunsn 
 |-  ( ( A \ { x } ) ~< ~P ( A \ { x } ) -> ( ( A \ { x } ) u. { x } ) ~<_ ~P ( A \ { x } ) )
38 35 36 37 3syl 
 |-  ( ( 1o ~< A /\ x e. A ) -> ( ( A \ { x } ) u. { x } ) ~<_ ~P ( A \ { x } ) )
39 34 38 eqbrtrrd 
 |-  ( ( 1o ~< A /\ x e. A ) -> A ~<_ ~P ( A \ { x } ) )
40 xpdom1g 
 |-  ( ( ~P { x } e. _V /\ A ~<_ ~P ( A \ { x } ) ) -> ( A X. ~P { x } ) ~<_ ( ~P ( A \ { x } ) X. ~P { x } ) )
41 28 39 40 sylancr 
 |-  ( ( 1o ~< A /\ x e. A ) -> ( A X. ~P { x } ) ~<_ ( ~P ( A \ { x } ) X. ~P { x } ) )
42 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 } ) )
43 26 41 42 syl2anc 
 |-  ( ( 1o ~< A /\ x e. A ) -> ( A X. 2o ) ~<_ ( ~P ( A \ { x } ) X. ~P { x } ) )
44 pwdjuen 
 |-  ( ( ( A \ { x } ) e. _V /\ { x } e. _V ) -> ~P ( ( A \ { x } ) |_| { x } ) ~~ ( ~P ( A \ { x } ) X. ~P { x } ) )
45 35 27 44 sylancl 
 |-  ( ( 1o ~< A /\ x e. A ) -> ~P ( ( A \ { x } ) |_| { x } ) ~~ ( ~P ( A \ { x } ) X. ~P { x } ) )
46 45 ensymd 
 |-  ( ( 1o ~< A /\ x e. A ) -> ( ~P ( A \ { x } ) X. ~P { x } ) ~~ ~P ( ( A \ { x } ) |_| { x } ) )
47 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 } ) )
48 43 46 47 syl2anc 
 |-  ( ( 1o ~< A /\ x e. A ) -> ( A X. 2o ) ~<_ ~P ( ( A \ { x } ) |_| { x } ) )
49 27 a1i 
 |-  ( ( 1o ~< A /\ x e. A ) -> { x } e. _V )
50 disjdifr 
 |-  ( ( A \ { x } ) i^i { x } ) = (/)
51 50 a1i 
 |-  ( ( 1o ~< A /\ x e. A ) -> ( ( A \ { x } ) i^i { x } ) = (/) )
52 endjudisj 
 |-  ( ( ( A \ { x } ) e. _V /\ { x } e. _V /\ ( ( A \ { x } ) i^i { x } ) = (/) ) -> ( ( A \ { x } ) |_| { x } ) ~~ ( ( A \ { x } ) u. { x } ) )
53 35 49 51 52 syl3anc 
 |-  ( ( 1o ~< A /\ x e. A ) -> ( ( A \ { x } ) |_| { x } ) ~~ ( ( A \ { x } ) u. { x } ) )
54 53 34 breqtrd 
 |-  ( ( 1o ~< A /\ x e. A ) -> ( ( A \ { x } ) |_| { x } ) ~~ A )
55 pwen 
 |-  ( ( ( A \ { x } ) |_| { x } ) ~~ A -> ~P ( ( A \ { x } ) |_| { x } ) ~~ ~P A )
56 54 55 syl 
 |-  ( ( 1o ~< A /\ x e. A ) -> ~P ( ( A \ { x } ) |_| { x } ) ~~ ~P A )
57 domentr 
 |-  ( ( ( A X. 2o ) ~<_ ~P ( ( A \ { x } ) |_| { x } ) /\ ~P ( ( A \ { x } ) |_| { x } ) ~~ ~P A ) -> ( A X. 2o ) ~<_ ~P A )
58 48 56 57 syl2anc 
 |-  ( ( 1o ~< A /\ x e. A ) -> ( A X. 2o ) ~<_ ~P A )
59 9 58 exlimddv 
 |-  ( 1o ~< A -> ( A X. 2o ) ~<_ ~P A )
60 domtr 
 |-  ( ( ( A |_| 2o ) ~<_ ( A X. 2o ) /\ ( A X. 2o ) ~<_ ~P A ) -> ( A |_| 2o ) ~<_ ~P A )
61 3 59 60 syl2anc 
 |-  ( 1o ~< A -> ( A |_| 2o ) ~<_ ~P A )