Metamath Proof Explorer

Theorem fin1a2lem12

Description: Lemma for fin1a2 . (Contributed by Stefan O'Rear, 8-Nov-2014) (Revised by Mario Carneiro, 17-May-2015)

Ref Expression
Assertion fin1a2lem12 
|- ( ( ( A C_ ~P B /\ [C.] Or A /\ -. U. A e. A ) /\ ( A C_ Fin /\ A =/= (/) ) ) -> -. B e. Fin3 )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( ( ( A C_ ~P B /\ [C.] Or A /\ -. U. A e. A ) /\ ( A C_ Fin /\ A =/= (/) ) ) /\ B e. Fin3 ) -> B e. Fin3 )
2 simpll1 
 |-  ( ( ( ( A C_ ~P B /\ [C.] Or A /\ -. U. A e. A ) /\ ( A C_ Fin /\ A =/= (/) ) ) /\ B e. Fin3 ) -> A C_ ~P B )
3 2 adantr 
 |-  ( ( ( ( ( A C_ ~P B /\ [C.] Or A /\ -. U. A e. A ) /\ ( A C_ Fin /\ A =/= (/) ) ) /\ B e. Fin3 ) /\ e e. _om ) -> A C_ ~P B )
4 ssrab2 
 |-  { f e. A | f ~<_ e } C_ A
5 4 unissi 
 |-  U. { f e. A | f ~<_ e } C_ U. A
6 sspwuni 
 |-  ( A C_ ~P B <-> U. A C_ B )
7 6 biimpi 
 |-  ( A C_ ~P B -> U. A C_ B )
8 5 7 sstrid 
 |-  ( A C_ ~P B -> U. { f e. A | f ~<_ e } C_ B )
9 3 8 syl 
 |-  ( ( ( ( ( A C_ ~P B /\ [C.] Or A /\ -. U. A e. A ) /\ ( A C_ Fin /\ A =/= (/) ) ) /\ B e. Fin3 ) /\ e e. _om ) -> U. { f e. A | f ~<_ e } C_ B )
10 elpw2g 
 |-  ( B e. Fin3 -> ( U. { f e. A | f ~<_ e } e. ~P B <-> U. { f e. A | f ~<_ e } C_ B ) )
11 10 ad2antlr 
 |-  ( ( ( ( ( A C_ ~P B /\ [C.] Or A /\ -. U. A e. A ) /\ ( A C_ Fin /\ A =/= (/) ) ) /\ B e. Fin3 ) /\ e e. _om ) -> ( U. { f e. A | f ~<_ e } e. ~P B <-> U. { f e. A | f ~<_ e } C_ B ) )
12 9 11 mpbird 
 |-  ( ( ( ( ( A C_ ~P B /\ [C.] Or A /\ -. U. A e. A ) /\ ( A C_ Fin /\ A =/= (/) ) ) /\ B e. Fin3 ) /\ e e. _om ) -> U. { f e. A | f ~<_ e } e. ~P B )
13 12 fmpttd 
 |-  ( ( ( ( A C_ ~P B /\ [C.] Or A /\ -. U. A e. A ) /\ ( A C_ Fin /\ A =/= (/) ) ) /\ B e. Fin3 ) -> ( e e. _om |-> U. { f e. A | f ~<_ e } ) : _om --> ~P B )
14 vex 
 |-  d e. _V
15 14 sucex 
 |-  suc d e. _V
16 sssucid 
 |-  d C_ suc d
17 ssdomg 
 |-  ( suc d e. _V -> ( d C_ suc d -> d ~<_ suc d ) )
18 15 16 17 mp2 
 |-  d ~<_ suc d
19 domtr 
 |-  ( ( f ~<_ d /\ d ~<_ suc d ) -> f ~<_ suc d )
20 18 19 mpan2 
 |-  ( f ~<_ d -> f ~<_ suc d )
21 20 a1i 
 |-  ( f e. A -> ( f ~<_ d -> f ~<_ suc d ) )
22 21 ss2rabi 
 |-  { f e. A | f ~<_ d } C_ { f e. A | f ~<_ suc d }
23 uniss 
 |-  ( { f e. A | f ~<_ d } C_ { f e. A | f ~<_ suc d } -> U. { f e. A | f ~<_ d } C_ U. { f e. A | f ~<_ suc d } )
24 22 23 mp1i 
 |-  ( ( ( ( ( A C_ ~P B /\ [C.] Or A /\ -. U. A e. A ) /\ ( A C_ Fin /\ A =/= (/) ) ) /\ B e. Fin3 ) /\ d e. _om ) -> U. { f e. A | f ~<_ d } C_ U. { f e. A | f ~<_ suc d } )
25 id 
 |-  ( d e. _om -> d e. _om )
26 pwexg 
 |-  ( B e. Fin3 -> ~P B e. _V )
27 26 adantl 
 |-  ( ( ( ( A C_ ~P B /\ [C.] Or A /\ -. U. A e. A ) /\ ( A C_ Fin /\ A =/= (/) ) ) /\ B e. Fin3 ) -> ~P B e. _V )
28 27 2 ssexd 
 |-  ( ( ( ( A C_ ~P B /\ [C.] Or A /\ -. U. A e. A ) /\ ( A C_ Fin /\ A =/= (/) ) ) /\ B e. Fin3 ) -> A e. _V )
29 rabexg 
 |-  ( A e. _V -> { f e. A | f ~<_ d } e. _V )
30 uniexg 
 |-  ( { f e. A | f ~<_ d } e. _V -> U. { f e. A | f ~<_ d } e. _V )
31 28 29 30 3syl 
 |-  ( ( ( ( A C_ ~P B /\ [C.] Or A /\ -. U. A e. A ) /\ ( A C_ Fin /\ A =/= (/) ) ) /\ B e. Fin3 ) -> U. { f e. A | f ~<_ d } e. _V )
32 breq2 
 |-  ( e = d -> ( f ~<_ e <-> f ~<_ d ) )
33 32 rabbidv 
 |-  ( e = d -> { f e. A | f ~<_ e } = { f e. A | f ~<_ d } )
34 33 unieqd 
 |-  ( e = d -> U. { f e. A | f ~<_ e } = U. { f e. A | f ~<_ d } )
35 eqid 
 |-  ( e e. _om |-> U. { f e. A | f ~<_ e } ) = ( e e. _om |-> U. { f e. A | f ~<_ e } )
36 34 35 fvmptg 
 |-  ( ( d e. _om /\ U. { f e. A | f ~<_ d } e. _V ) -> ( ( e e. _om |-> U. { f e. A | f ~<_ e } ) ` d ) = U. { f e. A | f ~<_ d } )
37 25 31 36 syl2anr 
 |-  ( ( ( ( ( A C_ ~P B /\ [C.] Or A /\ -. U. A e. A ) /\ ( A C_ Fin /\ A =/= (/) ) ) /\ B e. Fin3 ) /\ d e. _om ) -> ( ( e e. _om |-> U. { f e. A | f ~<_ e } ) ` d ) = U. { f e. A | f ~<_ d } )
38 peano2 
 |-  ( d e. _om -> suc d e. _om )
39 rabexg 
 |-  ( A e. _V -> { f e. A | f ~<_ suc d } e. _V )
40 uniexg 
 |-  ( { f e. A | f ~<_ suc d } e. _V -> U. { f e. A | f ~<_ suc d } e. _V )
41 28 39 40 3syl 
 |-  ( ( ( ( A C_ ~P B /\ [C.] Or A /\ -. U. A e. A ) /\ ( A C_ Fin /\ A =/= (/) ) ) /\ B e. Fin3 ) -> U. { f e. A | f ~<_ suc d } e. _V )
42 breq2 
 |-  ( e = suc d -> ( f ~<_ e <-> f ~<_ suc d ) )
43 42 rabbidv 
 |-  ( e = suc d -> { f e. A | f ~<_ e } = { f e. A | f ~<_ suc d } )
44 43 unieqd 
 |-  ( e = suc d -> U. { f e. A | f ~<_ e } = U. { f e. A | f ~<_ suc d } )
45 44 35 fvmptg 
 |-  ( ( suc d e. _om /\ U. { f e. A | f ~<_ suc d } e. _V ) -> ( ( e e. _om |-> U. { f e. A | f ~<_ e } ) ` suc d ) = U. { f e. A | f ~<_ suc d } )
46 38 41 45 syl2anr 
 |-  ( ( ( ( ( A C_ ~P B /\ [C.] Or A /\ -. U. A e. A ) /\ ( A C_ Fin /\ A =/= (/) ) ) /\ B e. Fin3 ) /\ d e. _om ) -> ( ( e e. _om |-> U. { f e. A | f ~<_ e } ) ` suc d ) = U. { f e. A | f ~<_ suc d } )
47 24 37 46 3sstr4d 
 |-  ( ( ( ( ( A C_ ~P B /\ [C.] Or A /\ -. U. A e. A ) /\ ( A C_ Fin /\ A =/= (/) ) ) /\ B e. Fin3 ) /\ d e. _om ) -> ( ( e e. _om |-> U. { f e. A | f ~<_ e } ) ` d ) C_ ( ( e e. _om |-> U. { f e. A | f ~<_ e } ) ` suc d ) )
48 47 ralrimiva 
 |-  ( ( ( ( A C_ ~P B /\ [C.] Or A /\ -. U. A e. A ) /\ ( A C_ Fin /\ A =/= (/) ) ) /\ B e. Fin3 ) -> A. d e. _om ( ( e e. _om |-> U. { f e. A | f ~<_ e } ) ` d ) C_ ( ( e e. _om |-> U. { f e. A | f ~<_ e } ) ` suc d ) )
49 fin34i 
 |-  ( ( B e. Fin3 /\ ( e e. _om |-> U. { f e. A | f ~<_ e } ) : _om --> ~P B /\ A. d e. _om ( ( e e. _om |-> U. { f e. A | f ~<_ e } ) ` d ) C_ ( ( e e. _om |-> U. { f e. A | f ~<_ e } ) ` suc d ) ) -> U. ran ( e e. _om |-> U. { f e. A | f ~<_ e } ) e. ran ( e e. _om |-> U. { f e. A | f ~<_ e } ) )
50 1 13 48 49 syl3anc 
 |-  ( ( ( ( A C_ ~P B /\ [C.] Or A /\ -. U. A e. A ) /\ ( A C_ Fin /\ A =/= (/) ) ) /\ B e. Fin3 ) -> U. ran ( e e. _om |-> U. { f e. A | f ~<_ e } ) e. ran ( e e. _om |-> U. { f e. A | f ~<_ e } ) )
51 fin1a2lem11 
 |-  ( ( [C.] Or A /\ A C_ Fin ) -> ran ( e e. _om |-> U. { f e. A | f ~<_ e } ) = ( A u. { (/) } ) )
52 51 adantrr 
 |-  ( ( [C.] Or A /\ ( A C_ Fin /\ A =/= (/) ) ) -> ran ( e e. _om |-> U. { f e. A | f ~<_ e } ) = ( A u. { (/) } ) )
53 52 3ad2antl2 
 |-  ( ( ( A C_ ~P B /\ [C.] Or A /\ -. U. A e. A ) /\ ( A C_ Fin /\ A =/= (/) ) ) -> ran ( e e. _om |-> U. { f e. A | f ~<_ e } ) = ( A u. { (/) } ) )
54 53 adantr 
 |-  ( ( ( ( A C_ ~P B /\ [C.] Or A /\ -. U. A e. A ) /\ ( A C_ Fin /\ A =/= (/) ) ) /\ B e. Fin3 ) -> ran ( e e. _om |-> U. { f e. A | f ~<_ e } ) = ( A u. { (/) } ) )
55 simpll3 
 |-  ( ( ( ( A C_ ~P B /\ [C.] Or A /\ -. U. A e. A ) /\ ( A C_ Fin /\ A =/= (/) ) ) /\ B e. Fin3 ) -> -. U. A e. A )
56 simplrr 
 |-  ( ( ( ( A C_ ~P B /\ [C.] Or A /\ -. U. A e. A ) /\ ( A C_ Fin /\ A =/= (/) ) ) /\ B e. Fin3 ) -> A =/= (/) )
57 sspwuni 
 |-  ( A C_ ~P (/) <-> U. A C_ (/) )
58 ss0b 
 |-  ( U. A C_ (/) <-> U. A = (/) )
59 57 58 bitri 
 |-  ( A C_ ~P (/) <-> U. A = (/) )
60 pw0 
 |-  ~P (/) = { (/) }
61 60 sseq2i 
 |-  ( A C_ ~P (/) <-> A C_ { (/) } )
62 sssn 
 |-  ( A C_ { (/) } <-> ( A = (/) \/ A = { (/) } ) )
63 61 62 bitri 
 |-  ( A C_ ~P (/) <-> ( A = (/) \/ A = { (/) } ) )
64 df-ne 
 |-  ( A =/= (/) <-> -. A = (/) )
65 0ex 
 |-  (/) e. _V
66 65 unisn 
 |-  U. { (/) } = (/)
67 65 snid 
 |-  (/) e. { (/) }
68 66 67 eqeltri 
 |-  U. { (/) } e. { (/) }
69 unieq 
 |-  ( A = { (/) } -> U. A = U. { (/) } )
70 id 
 |-  ( A = { (/) } -> A = { (/) } )
71 69 70 eleq12d 
 |-  ( A = { (/) } -> ( U. A e. A <-> U. { (/) } e. { (/) } ) )
72 68 71 mpbiri 
 |-  ( A = { (/) } -> U. A e. A )
73 72 orim2i 
 |-  ( ( A = (/) \/ A = { (/) } ) -> ( A = (/) \/ U. A e. A ) )
74 73 ord 
 |-  ( ( A = (/) \/ A = { (/) } ) -> ( -. A = (/) -> U. A e. A ) )
75 64 74 syl5bi 
 |-  ( ( A = (/) \/ A = { (/) } ) -> ( A =/= (/) -> U. A e. A ) )
76 63 75 sylbi 
 |-  ( A C_ ~P (/) -> ( A =/= (/) -> U. A e. A ) )
77 59 76 sylbir 
 |-  ( U. A = (/) -> ( A =/= (/) -> U. A e. A ) )
78 77 com12 
 |-  ( A =/= (/) -> ( U. A = (/) -> U. A e. A ) )
79 78 con3d 
 |-  ( A =/= (/) -> ( -. U. A e. A -> -. U. A = (/) ) )
80 56 55 79 sylc 
 |-  ( ( ( ( A C_ ~P B /\ [C.] Or A /\ -. U. A e. A ) /\ ( A C_ Fin /\ A =/= (/) ) ) /\ B e. Fin3 ) -> -. U. A = (/) )
81 ioran 
 |-  ( -. ( U. A e. A \/ U. A = (/) ) <-> ( -. U. A e. A /\ -. U. A = (/) ) )
82 55 80 81 sylanbrc 
 |-  ( ( ( ( A C_ ~P B /\ [C.] Or A /\ -. U. A e. A ) /\ ( A C_ Fin /\ A =/= (/) ) ) /\ B e. Fin3 ) -> -. ( U. A e. A \/ U. A = (/) ) )
83 uniun 
 |-  U. ( A u. { (/) } ) = ( U. A u. U. { (/) } )
84 66 uneq2i 
 |-  ( U. A u. U. { (/) } ) = ( U. A u. (/) )
85 un0 
 |-  ( U. A u. (/) ) = U. A
86 83 84 85 3eqtri 
 |-  U. ( A u. { (/) } ) = U. A
87 86 eleq1i 
 |-  ( U. ( A u. { (/) } ) e. ( A u. { (/) } ) <-> U. A e. ( A u. { (/) } ) )
88 elun 
 |-  ( U. A e. ( A u. { (/) } ) <-> ( U. A e. A \/ U. A e. { (/) } ) )
89 65 elsn2 
 |-  ( U. A e. { (/) } <-> U. A = (/) )
90 89 orbi2i 
 |-  ( ( U. A e. A \/ U. A e. { (/) } ) <-> ( U. A e. A \/ U. A = (/) ) )
91 87 88 90 3bitri 
 |-  ( U. ( A u. { (/) } ) e. ( A u. { (/) } ) <-> ( U. A e. A \/ U. A = (/) ) )
92 82 91 sylnibr 
 |-  ( ( ( ( A C_ ~P B /\ [C.] Or A /\ -. U. A e. A ) /\ ( A C_ Fin /\ A =/= (/) ) ) /\ B e. Fin3 ) -> -. U. ( A u. { (/) } ) e. ( A u. { (/) } ) )
93 unieq 
 |-  ( ran ( e e. _om |-> U. { f e. A | f ~<_ e } ) = ( A u. { (/) } ) -> U. ran ( e e. _om |-> U. { f e. A | f ~<_ e } ) = U. ( A u. { (/) } ) )
94 id 
 |-  ( ran ( e e. _om |-> U. { f e. A | f ~<_ e } ) = ( A u. { (/) } ) -> ran ( e e. _om |-> U. { f e. A | f ~<_ e } ) = ( A u. { (/) } ) )
95 93 94 eleq12d 
 |-  ( ran ( e e. _om |-> U. { f e. A | f ~<_ e } ) = ( A u. { (/) } ) -> ( U. ran ( e e. _om |-> U. { f e. A | f ~<_ e } ) e. ran ( e e. _om |-> U. { f e. A | f ~<_ e } ) <-> U. ( A u. { (/) } ) e. ( A u. { (/) } ) ) )
96 95 notbid 
 |-  ( ran ( e e. _om |-> U. { f e. A | f ~<_ e } ) = ( A u. { (/) } ) -> ( -. U. ran ( e e. _om |-> U. { f e. A | f ~<_ e } ) e. ran ( e e. _om |-> U. { f e. A | f ~<_ e } ) <-> -. U. ( A u. { (/) } ) e. ( A u. { (/) } ) ) )
97 92 96 syl5ibrcom 
 |-  ( ( ( ( A C_ ~P B /\ [C.] Or A /\ -. U. A e. A ) /\ ( A C_ Fin /\ A =/= (/) ) ) /\ B e. Fin3 ) -> ( ran ( e e. _om |-> U. { f e. A | f ~<_ e } ) = ( A u. { (/) } ) -> -. U. ran ( e e. _om |-> U. { f e. A | f ~<_ e } ) e. ran ( e e. _om |-> U. { f e. A | f ~<_ e } ) ) )
98 54 97 mpd 
 |-  ( ( ( ( A C_ ~P B /\ [C.] Or A /\ -. U. A e. A ) /\ ( A C_ Fin /\ A =/= (/) ) ) /\ B e. Fin3 ) -> -. U. ran ( e e. _om |-> U. { f e. A | f ~<_ e } ) e. ran ( e e. _om |-> U. { f e. A | f ~<_ e } ) )
99 50 98 pm2.65da 
 |-  ( ( ( A C_ ~P B /\ [C.] Or A /\ -. U. A e. A ) /\ ( A C_ Fin /\ A =/= (/) ) ) -> -. B e. Fin3 )