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