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 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 )