Metamath Proof Explorer

Theorem finsschain

Description: A finite subset of the union of a superset chain is a subset of some element of the chain. A useful preliminary result for alexsub and others. (Contributed by Jeff Hankins, 25-Jan-2010) (Proof shortened by Mario Carneiro, 11-Feb-2015) (Revised by Mario Carneiro, 18-May-2015)

Ref Expression
Assertion finsschain 
|- ( ( ( A =/= (/) /\ [C.] Or A ) /\ ( B e. Fin /\ B C_ U. A ) ) -> E. z e. A B C_ z )

Proof

Step Hyp Ref Expression
1 sseq1 
 |-  ( a = (/) -> ( a C_ U. A <-> (/) C_ U. A ) )
2 sseq1 
 |-  ( a = (/) -> ( a C_ z <-> (/) C_ z ) )
3 2 rexbidv 
 |-  ( a = (/) -> ( E. z e. A a C_ z <-> E. z e. A (/) C_ z ) )
4 1 3 imbi12d 
 |-  ( a = (/) -> ( ( a C_ U. A -> E. z e. A a C_ z ) <-> ( (/) C_ U. A -> E. z e. A (/) C_ z ) ) )
5 4 imbi2d 
 |-  ( a = (/) -> ( ( ( A =/= (/) /\ [C.] Or A ) -> ( a C_ U. A -> E. z e. A a C_ z ) ) <-> ( ( A =/= (/) /\ [C.] Or A ) -> ( (/) C_ U. A -> E. z e. A (/) C_ z ) ) ) )
6 sseq1 
 |-  ( a = b -> ( a C_ U. A <-> b C_ U. A ) )
7 sseq1 
 |-  ( a = b -> ( a C_ z <-> b C_ z ) )
8 7 rexbidv 
 |-  ( a = b -> ( E. z e. A a C_ z <-> E. z e. A b C_ z ) )
9 6 8 imbi12d 
 |-  ( a = b -> ( ( a C_ U. A -> E. z e. A a C_ z ) <-> ( b C_ U. A -> E. z e. A b C_ z ) ) )
10 9 imbi2d 
 |-  ( a = b -> ( ( ( A =/= (/) /\ [C.] Or A ) -> ( a C_ U. A -> E. z e. A a C_ z ) ) <-> ( ( A =/= (/) /\ [C.] Or A ) -> ( b C_ U. A -> E. z e. A b C_ z ) ) ) )
11 sseq1 
 |-  ( a = ( b u. { c } ) -> ( a C_ U. A <-> ( b u. { c } ) C_ U. A ) )
12 sseq1 
 |-  ( a = ( b u. { c } ) -> ( a C_ z <-> ( b u. { c } ) C_ z ) )
13 12 rexbidv 
 |-  ( a = ( b u. { c } ) -> ( E. z e. A a C_ z <-> E. z e. A ( b u. { c } ) C_ z ) )
14 11 13 imbi12d 
 |-  ( a = ( b u. { c } ) -> ( ( a C_ U. A -> E. z e. A a C_ z ) <-> ( ( b u. { c } ) C_ U. A -> E. z e. A ( b u. { c } ) C_ z ) ) )
15 14 imbi2d 
 |-  ( a = ( b u. { c } ) -> ( ( ( A =/= (/) /\ [C.] Or A ) -> ( a C_ U. A -> E. z e. A a C_ z ) ) <-> ( ( A =/= (/) /\ [C.] Or A ) -> ( ( b u. { c } ) C_ U. A -> E. z e. A ( b u. { c } ) C_ z ) ) ) )
16 sseq1 
 |-  ( a = B -> ( a C_ U. A <-> B C_ U. A ) )
17 sseq1 
 |-  ( a = B -> ( a C_ z <-> B C_ z ) )
18 17 rexbidv 
 |-  ( a = B -> ( E. z e. A a C_ z <-> E. z e. A B C_ z ) )
19 16 18 imbi12d 
 |-  ( a = B -> ( ( a C_ U. A -> E. z e. A a C_ z ) <-> ( B C_ U. A -> E. z e. A B C_ z ) ) )
20 19 imbi2d 
 |-  ( a = B -> ( ( ( A =/= (/) /\ [C.] Or A ) -> ( a C_ U. A -> E. z e. A a C_ z ) ) <-> ( ( A =/= (/) /\ [C.] Or A ) -> ( B C_ U. A -> E. z e. A B C_ z ) ) ) )
21 0ss 
 |-  (/) C_ z
22 21 rgenw 
 |-  A. z e. A (/) C_ z
23 r19.2z 
 |-  ( ( A =/= (/) /\ A. z e. A (/) C_ z ) -> E. z e. A (/) C_ z )
24 22 23 mpan2 
 |-  ( A =/= (/) -> E. z e. A (/) C_ z )
25 24 adantr 
 |-  ( ( A =/= (/) /\ [C.] Or A ) -> E. z e. A (/) C_ z )
26 25 a1d 
 |-  ( ( A =/= (/) /\ [C.] Or A ) -> ( (/) C_ U. A -> E. z e. A (/) C_ z ) )
27 id 
 |-  ( ( b u. { c } ) C_ U. A -> ( b u. { c } ) C_ U. A )
28 27 unssad 
 |-  ( ( b u. { c } ) C_ U. A -> b C_ U. A )
29 28 imim1i 
 |-  ( ( b C_ U. A -> E. z e. A b C_ z ) -> ( ( b u. { c } ) C_ U. A -> E. z e. A b C_ z ) )
30 sseq2 
 |-  ( z = w -> ( b C_ z <-> b C_ w ) )
31 30 cbvrexvw 
 |-  ( E. z e. A b C_ z <-> E. w e. A b C_ w )
32 simpr 
 |-  ( ( ( A =/= (/) /\ [C.] Or A ) /\ ( b u. { c } ) C_ U. A ) -> ( b u. { c } ) C_ U. A )
33 32 unssbd 
 |-  ( ( ( A =/= (/) /\ [C.] Or A ) /\ ( b u. { c } ) C_ U. A ) -> { c } C_ U. A )
34 vex 
 |-  c e. _V
35 34 snss 
 |-  ( c e. U. A <-> { c } C_ U. A )
36 33 35 sylibr 
 |-  ( ( ( A =/= (/) /\ [C.] Or A ) /\ ( b u. { c } ) C_ U. A ) -> c e. U. A )
37 eluni2 
 |-  ( c e. U. A <-> E. u e. A c e. u )
38 36 37 sylib 
 |-  ( ( ( A =/= (/) /\ [C.] Or A ) /\ ( b u. { c } ) C_ U. A ) -> E. u e. A c e. u )
39 reeanv 
 |-  ( E. u e. A E. w e. A ( c e. u /\ b C_ w ) <-> ( E. u e. A c e. u /\ E. w e. A b C_ w ) )
40 simpllr 
 |-  ( ( ( ( A =/= (/) /\ [C.] Or A ) /\ ( b u. { c } ) C_ U. A ) /\ ( ( u e. A /\ w e. A ) /\ ( c e. u /\ b C_ w ) ) ) -> [C.] Or A )
41 simprlr 
 |-  ( ( ( ( A =/= (/) /\ [C.] Or A ) /\ ( b u. { c } ) C_ U. A ) /\ ( ( u e. A /\ w e. A ) /\ ( c e. u /\ b C_ w ) ) ) -> w e. A )
42 simprll 
 |-  ( ( ( ( A =/= (/) /\ [C.] Or A ) /\ ( b u. { c } ) C_ U. A ) /\ ( ( u e. A /\ w e. A ) /\ ( c e. u /\ b C_ w ) ) ) -> u e. A )
43 sorpssun 
 |-  ( ( [C.] Or A /\ ( w e. A /\ u e. A ) ) -> ( w u. u ) e. A )
44 40 41 42 43 syl12anc 
 |-  ( ( ( ( A =/= (/) /\ [C.] Or A ) /\ ( b u. { c } ) C_ U. A ) /\ ( ( u e. A /\ w e. A ) /\ ( c e. u /\ b C_ w ) ) ) -> ( w u. u ) e. A )
45 simprrr 
 |-  ( ( ( ( A =/= (/) /\ [C.] Or A ) /\ ( b u. { c } ) C_ U. A ) /\ ( ( u e. A /\ w e. A ) /\ ( c e. u /\ b C_ w ) ) ) -> b C_ w )
46 simprrl 
 |-  ( ( ( ( A =/= (/) /\ [C.] Or A ) /\ ( b u. { c } ) C_ U. A ) /\ ( ( u e. A /\ w e. A ) /\ ( c e. u /\ b C_ w ) ) ) -> c e. u )
47 46 snssd 
 |-  ( ( ( ( A =/= (/) /\ [C.] Or A ) /\ ( b u. { c } ) C_ U. A ) /\ ( ( u e. A /\ w e. A ) /\ ( c e. u /\ b C_ w ) ) ) -> { c } C_ u )
48 unss12 
 |-  ( ( b C_ w /\ { c } C_ u ) -> ( b u. { c } ) C_ ( w u. u ) )
49 45 47 48 syl2anc 
 |-  ( ( ( ( A =/= (/) /\ [C.] Or A ) /\ ( b u. { c } ) C_ U. A ) /\ ( ( u e. A /\ w e. A ) /\ ( c e. u /\ b C_ w ) ) ) -> ( b u. { c } ) C_ ( w u. u ) )
50 sseq2 
 |-  ( z = ( w u. u ) -> ( ( b u. { c } ) C_ z <-> ( b u. { c } ) C_ ( w u. u ) ) )
51 50 rspcev 
 |-  ( ( ( w u. u ) e. A /\ ( b u. { c } ) C_ ( w u. u ) ) -> E. z e. A ( b u. { c } ) C_ z )
52 44 49 51 syl2anc 
 |-  ( ( ( ( A =/= (/) /\ [C.] Or A ) /\ ( b u. { c } ) C_ U. A ) /\ ( ( u e. A /\ w e. A ) /\ ( c e. u /\ b C_ w ) ) ) -> E. z e. A ( b u. { c } ) C_ z )
53 52 expr 
 |-  ( ( ( ( A =/= (/) /\ [C.] Or A ) /\ ( b u. { c } ) C_ U. A ) /\ ( u e. A /\ w e. A ) ) -> ( ( c e. u /\ b C_ w ) -> E. z e. A ( b u. { c } ) C_ z ) )
54 53 rexlimdvva 
 |-  ( ( ( A =/= (/) /\ [C.] Or A ) /\ ( b u. { c } ) C_ U. A ) -> ( E. u e. A E. w e. A ( c e. u /\ b C_ w ) -> E. z e. A ( b u. { c } ) C_ z ) )
55 39 54 syl5bir 
 |-  ( ( ( A =/= (/) /\ [C.] Or A ) /\ ( b u. { c } ) C_ U. A ) -> ( ( E. u e. A c e. u /\ E. w e. A b C_ w ) -> E. z e. A ( b u. { c } ) C_ z ) )
56 38 55 mpand 
 |-  ( ( ( A =/= (/) /\ [C.] Or A ) /\ ( b u. { c } ) C_ U. A ) -> ( E. w e. A b C_ w -> E. z e. A ( b u. { c } ) C_ z ) )
57 31 56 syl5bi 
 |-  ( ( ( A =/= (/) /\ [C.] Or A ) /\ ( b u. { c } ) C_ U. A ) -> ( E. z e. A b C_ z -> E. z e. A ( b u. { c } ) C_ z ) )
58 57 ex 
 |-  ( ( A =/= (/) /\ [C.] Or A ) -> ( ( b u. { c } ) C_ U. A -> ( E. z e. A b C_ z -> E. z e. A ( b u. { c } ) C_ z ) ) )
59 58 a2d 
 |-  ( ( A =/= (/) /\ [C.] Or A ) -> ( ( ( b u. { c } ) C_ U. A -> E. z e. A b C_ z ) -> ( ( b u. { c } ) C_ U. A -> E. z e. A ( b u. { c } ) C_ z ) ) )
60 29 59 syl5 
 |-  ( ( A =/= (/) /\ [C.] Or A ) -> ( ( b C_ U. A -> E. z e. A b C_ z ) -> ( ( b u. { c } ) C_ U. A -> E. z e. A ( b u. { c } ) C_ z ) ) )
61 60 a2i 
 |-  ( ( ( A =/= (/) /\ [C.] Or A ) -> ( b C_ U. A -> E. z e. A b C_ z ) ) -> ( ( A =/= (/) /\ [C.] Or A ) -> ( ( b u. { c } ) C_ U. A -> E. z e. A ( b u. { c } ) C_ z ) ) )
62 61 a1i 
 |-  ( b e. Fin -> ( ( ( A =/= (/) /\ [C.] Or A ) -> ( b C_ U. A -> E. z e. A b C_ z ) ) -> ( ( A =/= (/) /\ [C.] Or A ) -> ( ( b u. { c } ) C_ U. A -> E. z e. A ( b u. { c } ) C_ z ) ) ) )
63 5 10 15 20 26 62 findcard2 
 |-  ( B e. Fin -> ( ( A =/= (/) /\ [C.] Or A ) -> ( B C_ U. A -> E. z e. A B C_ z ) ) )
64 63 com12 
 |-  ( ( A =/= (/) /\ [C.] Or A ) -> ( B e. Fin -> ( B C_ U. A -> E. z e. A B C_ z ) ) )
65 64 imp32 
 |-  ( ( ( A =/= (/) /\ [C.] Or A ) /\ ( B e. Fin /\ B C_ U. A ) ) -> E. z e. A B C_ z )