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

Metamath Proof Explorer

Theorem ackbij1lem12

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 ackbij1lem12 
|- ( ( B e. ( ~P _om i^i Fin ) /\ A C_ B ) -> ( F ` A ) C_ ( F ` B ) )

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 1 ackbij1lem10 
 |-  F : ( ~P _om i^i Fin ) --> _om
3 1 ackbij1lem11 
 |-  ( ( B e. ( ~P _om i^i Fin ) /\ A C_ B ) -> A e. ( ~P _om i^i Fin ) )
4 ffvelcdm 
 |-  ( ( F : ( ~P _om i^i Fin ) --> _om /\ A e. ( ~P _om i^i Fin ) ) -> ( F ` A ) e. _om )
5 2 3 4 sylancr 
 |-  ( ( B e. ( ~P _om i^i Fin ) /\ A C_ B ) -> ( F ` A ) e. _om )
6 difssd 
 |-  ( ( B e. ( ~P _om i^i Fin ) /\ A C_ B ) -> ( B \ A ) C_ B )
7 1 ackbij1lem11 
 |-  ( ( B e. ( ~P _om i^i Fin ) /\ ( B \ A ) C_ B ) -> ( B \ A ) e. ( ~P _om i^i Fin ) )
8 6 7 syldan 
 |-  ( ( B e. ( ~P _om i^i Fin ) /\ A C_ B ) -> ( B \ A ) e. ( ~P _om i^i Fin ) )
9 ffvelcdm 
 |-  ( ( F : ( ~P _om i^i Fin ) --> _om /\ ( B \ A ) e. ( ~P _om i^i Fin ) ) -> ( F ` ( B \ A ) ) e. _om )
10 2 8 9 sylancr 
 |-  ( ( B e. ( ~P _om i^i Fin ) /\ A C_ B ) -> ( F ` ( B \ A ) ) e. _om )
11 nnaword1 
 |-  ( ( ( F ` A ) e. _om /\ ( F ` ( B \ A ) ) e. _om ) -> ( F ` A ) C_ ( ( F ` A ) +o ( F ` ( B \ A ) ) ) )
12 5 10 11 syl2anc 
 |-  ( ( B e. ( ~P _om i^i Fin ) /\ A C_ B ) -> ( F ` A ) C_ ( ( F ` A ) +o ( F ` ( B \ A ) ) ) )
13 disjdif 
 |-  ( A i^i ( B \ A ) ) = (/)
14 13 a1i 
 |-  ( ( B e. ( ~P _om i^i Fin ) /\ A C_ B ) -> ( A i^i ( B \ A ) ) = (/) )
15 1 ackbij1lem9 
 |-  ( ( A e. ( ~P _om i^i Fin ) /\ ( B \ A ) e. ( ~P _om i^i Fin ) /\ ( A i^i ( B \ A ) ) = (/) ) -> ( F ` ( A u. ( B \ A ) ) ) = ( ( F ` A ) +o ( F ` ( B \ A ) ) ) )
16 3 8 14 15 syl3anc 
 |-  ( ( B e. ( ~P _om i^i Fin ) /\ A C_ B ) -> ( F ` ( A u. ( B \ A ) ) ) = ( ( F ` A ) +o ( F ` ( B \ A ) ) ) )
17 undif 
 |-  ( A C_ B <-> ( A u. ( B \ A ) ) = B )
18 17 biimpi 
 |-  ( A C_ B -> ( A u. ( B \ A ) ) = B )
19 18 adantl 
 |-  ( ( B e. ( ~P _om i^i Fin ) /\ A C_ B ) -> ( A u. ( B \ A ) ) = B )
20 19 fveq2d 
 |-  ( ( B e. ( ~P _om i^i Fin ) /\ A C_ B ) -> ( F ` ( A u. ( B \ A ) ) ) = ( F ` B ) )
21 16 20 eqtr3d 
 |-  ( ( B e. ( ~P _om i^i Fin ) /\ A C_ B ) -> ( ( F ` A ) +o ( F ` ( B \ A ) ) ) = ( F ` B ) )
22 12 21 sseqtrd 
 |-  ( ( B e. ( ~P _om i^i Fin ) /\ A C_ B ) -> ( F ` A ) C_ ( F ` B ) )