Metamath Proof Explorer

Theorem ackbij1lem15

Description: Lemma for ackbij1 . (Contributed by Stefan O'Rear, 18-Nov-2014)

Ref Expression
Hypothesis ackbij.f 
|- F = ( x e. ( ~P _om i^i Fin ) |-> ( card ` U_ y e. x ( { y } X. ~P y ) ) )
Assertion ackbij1lem15 
|- ( ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) /\ ( c e. _om /\ c e. A /\ -. c e. B ) ) -> -. ( F ` ( A i^i suc c ) ) = ( F ` ( B i^i suc c ) ) )

Proof

Step Hyp Ref Expression
1 ackbij.f 
 |-  F = ( x e. ( ~P _om i^i Fin ) |-> ( card ` U_ y e. x ( { y } X. ~P y ) ) )
2 simpr1 
 |-  ( ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) /\ ( c e. _om /\ c e. A /\ -. c e. B ) ) -> c e. _om )
3 ackbij1lem3 
 |-  ( c e. _om -> c e. ( ~P _om i^i Fin ) )
4 2 3 syl 
 |-  ( ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) /\ ( c e. _om /\ c e. A /\ -. c e. B ) ) -> c e. ( ~P _om i^i Fin ) )
5 simpr3 
 |-  ( ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) /\ ( c e. _om /\ c e. A /\ -. c e. B ) ) -> -. c e. B )
6 ackbij1lem1 
 |-  ( -. c e. B -> ( B i^i suc c ) = ( B i^i c ) )
7 5 6 syl 
 |-  ( ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) /\ ( c e. _om /\ c e. A /\ -. c e. B ) ) -> ( B i^i suc c ) = ( B i^i c ) )
8 inss2 
 |-  ( B i^i c ) C_ c
9 7 8 eqsstrdi 
 |-  ( ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) /\ ( c e. _om /\ c e. A /\ -. c e. B ) ) -> ( B i^i suc c ) C_ c )
10 1 ackbij1lem12 
 |-  ( ( c e. ( ~P _om i^i Fin ) /\ ( B i^i suc c ) C_ c ) -> ( F ` ( B i^i suc c ) ) C_ ( F ` c ) )
11 4 9 10 syl2anc 
 |-  ( ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) /\ ( c e. _om /\ c e. A /\ -. c e. B ) ) -> ( F ` ( B i^i suc c ) ) C_ ( F ` c ) )
12 1 ackbij1lem10 
 |-  F : ( ~P _om i^i Fin ) --> _om
13 12 ffvelrni 
 |-  ( c e. ( ~P _om i^i Fin ) -> ( F ` c ) e. _om )
14 nnon 
 |-  ( ( F ` c ) e. _om -> ( F ` c ) e. On )
15 onpsssuc 
 |-  ( ( F ` c ) e. On -> ( F ` c ) C. suc ( F ` c ) )
16 4 13 14 15 4syl 
 |-  ( ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) /\ ( c e. _om /\ c e. A /\ -. c e. B ) ) -> ( F ` c ) C. suc ( F ` c ) )
17 1 ackbij1lem14 
 |-  ( c e. _om -> ( F ` { c } ) = suc ( F ` c ) )
18 2 17 syl 
 |-  ( ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) /\ ( c e. _om /\ c e. A /\ -. c e. B ) ) -> ( F ` { c } ) = suc ( F ` c ) )
19 18 psseq2d 
 |-  ( ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) /\ ( c e. _om /\ c e. A /\ -. c e. B ) ) -> ( ( F ` c ) C. ( F ` { c } ) <-> ( F ` c ) C. suc ( F ` c ) ) )
20 16 19 mpbird 
 |-  ( ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) /\ ( c e. _om /\ c e. A /\ -. c e. B ) ) -> ( F ` c ) C. ( F ` { c } ) )
21 simpll 
 |-  ( ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) /\ ( c e. _om /\ c e. A /\ -. c e. B ) ) -> A e. ( ~P _om i^i Fin ) )
22 inss1 
 |-  ( A i^i suc c ) C_ A
23 1 ackbij1lem11 
 |-  ( ( A e. ( ~P _om i^i Fin ) /\ ( A i^i suc c ) C_ A ) -> ( A i^i suc c ) e. ( ~P _om i^i Fin ) )
24 21 22 23 sylancl 
 |-  ( ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) /\ ( c e. _om /\ c e. A /\ -. c e. B ) ) -> ( A i^i suc c ) e. ( ~P _om i^i Fin ) )
25 ssun1 
 |-  { c } C_ ( { c } u. ( A i^i c ) )
26 simpr2 
 |-  ( ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) /\ ( c e. _om /\ c e. A /\ -. c e. B ) ) -> c e. A )
27 ackbij1lem2 
 |-  ( c e. A -> ( A i^i suc c ) = ( { c } u. ( A i^i c ) ) )
28 26 27 syl 
 |-  ( ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) /\ ( c e. _om /\ c e. A /\ -. c e. B ) ) -> ( A i^i suc c ) = ( { c } u. ( A i^i c ) ) )
29 25 28 sseqtrrid 
 |-  ( ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) /\ ( c e. _om /\ c e. A /\ -. c e. B ) ) -> { c } C_ ( A i^i suc c ) )
30 1 ackbij1lem12 
 |-  ( ( ( A i^i suc c ) e. ( ~P _om i^i Fin ) /\ { c } C_ ( A i^i suc c ) ) -> ( F ` { c } ) C_ ( F ` ( A i^i suc c ) ) )
31 24 29 30 syl2anc 
 |-  ( ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) /\ ( c e. _om /\ c e. A /\ -. c e. B ) ) -> ( F ` { c } ) C_ ( F ` ( A i^i suc c ) ) )
32 20 31 psssstrd 
 |-  ( ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) /\ ( c e. _om /\ c e. A /\ -. c e. B ) ) -> ( F ` c ) C. ( F ` ( A i^i suc c ) ) )
33 11 32 sspsstrd 
 |-  ( ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) /\ ( c e. _om /\ c e. A /\ -. c e. B ) ) -> ( F ` ( B i^i suc c ) ) C. ( F ` ( A i^i suc c ) ) )
34 33 pssned 
 |-  ( ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) /\ ( c e. _om /\ c e. A /\ -. c e. B ) ) -> ( F ` ( B i^i suc c ) ) =/= ( F ` ( A i^i suc c ) ) )
35 34 necomd 
 |-  ( ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) /\ ( c e. _om /\ c e. A /\ -. c e. B ) ) -> ( F ` ( A i^i suc c ) ) =/= ( F ` ( B i^i suc c ) ) )
36 35 neneqd 
 |-  ( ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) /\ ( c e. _om /\ c e. A /\ -. c e. B ) ) -> -. ( F ` ( A i^i suc c ) ) = ( F ` ( B i^i suc c ) ) )