Metamath Proof Explorer

Theorem fin1a2lem10

Description: Lemma for fin1a2 . A nonempty finite union of members of a chain is a member of the chain. (Contributed by Stefan O'Rear, 8-Nov-2014)

Ref Expression
Assertion fin1a2lem10 
|- ( ( A =/= (/) /\ A e. Fin /\ [C.] Or A ) -> U. A e. A )

Proof

Step Hyp Ref Expression
1 eqneqall 
 |-  ( a = (/) -> ( a =/= (/) -> ( [C.] Or a -> U. a e. a ) ) )
2 tru 
 |-  T.
3 2 a1i 
 |-  ( a = (/) -> T. )
4 1 3 2thd 
 |-  ( a = (/) -> ( ( a =/= (/) -> ( [C.] Or a -> U. a e. a ) ) <-> T. ) )
5 neeq1 
 |-  ( a = b -> ( a =/= (/) <-> b =/= (/) ) )
6 soeq2 
 |-  ( a = b -> ( [C.] Or a <-> [C.] Or b ) )
7 unieq 
 |-  ( a = b -> U. a = U. b )
8 id 
 |-  ( a = b -> a = b )
9 7 8 eleq12d 
 |-  ( a = b -> ( U. a e. a <-> U. b e. b ) )
10 6 9 imbi12d 
 |-  ( a = b -> ( ( [C.] Or a -> U. a e. a ) <-> ( [C.] Or b -> U. b e. b ) ) )
11 5 10 imbi12d 
 |-  ( a = b -> ( ( a =/= (/) -> ( [C.] Or a -> U. a e. a ) ) <-> ( b =/= (/) -> ( [C.] Or b -> U. b e. b ) ) ) )
12 neeq1 
 |-  ( a = ( b u. { c } ) -> ( a =/= (/) <-> ( b u. { c } ) =/= (/) ) )
13 soeq2 
 |-  ( a = ( b u. { c } ) -> ( [C.] Or a <-> [C.] Or ( b u. { c } ) ) )
14 unieq 
 |-  ( a = ( b u. { c } ) -> U. a = U. ( b u. { c } ) )
15 id 
 |-  ( a = ( b u. { c } ) -> a = ( b u. { c } ) )
16 14 15 eleq12d 
 |-  ( a = ( b u. { c } ) -> ( U. a e. a <-> U. ( b u. { c } ) e. ( b u. { c } ) ) )
17 13 16 imbi12d 
 |-  ( a = ( b u. { c } ) -> ( ( [C.] Or a -> U. a e. a ) <-> ( [C.] Or ( b u. { c } ) -> U. ( b u. { c } ) e. ( b u. { c } ) ) ) )
18 12 17 imbi12d 
 |-  ( a = ( b u. { c } ) -> ( ( a =/= (/) -> ( [C.] Or a -> U. a e. a ) ) <-> ( ( b u. { c } ) =/= (/) -> ( [C.] Or ( b u. { c } ) -> U. ( b u. { c } ) e. ( b u. { c } ) ) ) ) )
19 neeq1 
 |-  ( a = A -> ( a =/= (/) <-> A =/= (/) ) )
20 soeq2 
 |-  ( a = A -> ( [C.] Or a <-> [C.] Or A ) )
21 unieq 
 |-  ( a = A -> U. a = U. A )
22 id 
 |-  ( a = A -> a = A )
23 21 22 eleq12d 
 |-  ( a = A -> ( U. a e. a <-> U. A e. A ) )
24 20 23 imbi12d 
 |-  ( a = A -> ( ( [C.] Or a -> U. a e. a ) <-> ( [C.] Or A -> U. A e. A ) ) )
25 19 24 imbi12d 
 |-  ( a = A -> ( ( a =/= (/) -> ( [C.] Or a -> U. a e. a ) ) <-> ( A =/= (/) -> ( [C.] Or A -> U. A e. A ) ) ) )
26 vex 
 |-  c e. _V
27 26 unisn 
 |-  U. { c } = c
28 vsnid 
 |-  c e. { c }
29 27 28 eqeltri 
 |-  U. { c } e. { c }
30 uneq1 
 |-  ( b = (/) -> ( b u. { c } ) = ( (/) u. { c } ) )
31 uncom 
 |-  ( (/) u. { c } ) = ( { c } u. (/) )
32 un0 
 |-  ( { c } u. (/) ) = { c }
33 31 32 eqtri 
 |-  ( (/) u. { c } ) = { c }
34 30 33 eqtrdi 
 |-  ( b = (/) -> ( b u. { c } ) = { c } )
35 34 unieqd 
 |-  ( b = (/) -> U. ( b u. { c } ) = U. { c } )
36 35 34 eleq12d 
 |-  ( b = (/) -> ( U. ( b u. { c } ) e. ( b u. { c } ) <-> U. { c } e. { c } ) )
37 29 36 mpbiri 
 |-  ( b = (/) -> U. ( b u. { c } ) e. ( b u. { c } ) )
38 37 a1d 
 |-  ( b = (/) -> ( ( b =/= (/) -> ( [C.] Or b -> U. b e. b ) ) -> U. ( b u. { c } ) e. ( b u. { c } ) ) )
39 38 adantl 
 |-  ( ( ( b e. Fin /\ [C.] Or ( b u. { c } ) /\ ( b u. { c } ) =/= (/) ) /\ b = (/) ) -> ( ( b =/= (/) -> ( [C.] Or b -> U. b e. b ) ) -> U. ( b u. { c } ) e. ( b u. { c } ) ) )
40 simpr 
 |-  ( ( ( b e. Fin /\ [C.] Or ( b u. { c } ) /\ ( b u. { c } ) =/= (/) ) /\ b =/= (/) ) -> b =/= (/) )
41 ssun1 
 |-  b C_ ( b u. { c } )
42 simpl2 
 |-  ( ( ( b e. Fin /\ [C.] Or ( b u. { c } ) /\ ( b u. { c } ) =/= (/) ) /\ b =/= (/) ) -> [C.] Or ( b u. { c } ) )
43 soss 
 |-  ( b C_ ( b u. { c } ) -> ( [C.] Or ( b u. { c } ) -> [C.] Or b ) )
44 41 42 43 mpsyl 
 |-  ( ( ( b e. Fin /\ [C.] Or ( b u. { c } ) /\ ( b u. { c } ) =/= (/) ) /\ b =/= (/) ) -> [C.] Or b )
45 uniun 
 |-  U. ( b u. { c } ) = ( U. b u. U. { c } )
46 27 uneq2i 
 |-  ( U. b u. U. { c } ) = ( U. b u. c )
47 45 46 eqtri 
 |-  U. ( b u. { c } ) = ( U. b u. c )
48 simprr 
 |-  ( ( ( b e. Fin /\ [C.] Or ( b u. { c } ) /\ ( b u. { c } ) =/= (/) ) /\ ( b =/= (/) /\ U. b e. b ) ) -> U. b e. b )
49 simpl2 
 |-  ( ( ( b e. Fin /\ [C.] Or ( b u. { c } ) /\ ( b u. { c } ) =/= (/) ) /\ ( b =/= (/) /\ U. b e. b ) ) -> [C.] Or ( b u. { c } ) )
50 elun1 
 |-  ( U. b e. b -> U. b e. ( b u. { c } ) )
51 50 ad2antll 
 |-  ( ( ( b e. Fin /\ [C.] Or ( b u. { c } ) /\ ( b u. { c } ) =/= (/) ) /\ ( b =/= (/) /\ U. b e. b ) ) -> U. b e. ( b u. { c } ) )
52 ssun2 
 |-  { c } C_ ( b u. { c } )
53 52 28 sselii 
 |-  c e. ( b u. { c } )
54 53 a1i 
 |-  ( ( ( b e. Fin /\ [C.] Or ( b u. { c } ) /\ ( b u. { c } ) =/= (/) ) /\ ( b =/= (/) /\ U. b e. b ) ) -> c e. ( b u. { c } ) )
55 sorpssi 
 |-  ( ( [C.] Or ( b u. { c } ) /\ ( U. b e. ( b u. { c } ) /\ c e. ( b u. { c } ) ) ) -> ( U. b C_ c \/ c C_ U. b ) )
56 49 51 54 55 syl12anc 
 |-  ( ( ( b e. Fin /\ [C.] Or ( b u. { c } ) /\ ( b u. { c } ) =/= (/) ) /\ ( b =/= (/) /\ U. b e. b ) ) -> ( U. b C_ c \/ c C_ U. b ) )
57 ssequn1 
 |-  ( U. b C_ c <-> ( U. b u. c ) = c )
58 53 a1i 
 |-  ( U. b e. b -> c e. ( b u. { c } ) )
59 eleq1 
 |-  ( ( U. b u. c ) = c -> ( ( U. b u. c ) e. ( b u. { c } ) <-> c e. ( b u. { c } ) ) )
60 58 59 syl5ibr 
 |-  ( ( U. b u. c ) = c -> ( U. b e. b -> ( U. b u. c ) e. ( b u. { c } ) ) )
61 57 60 sylbi 
 |-  ( U. b C_ c -> ( U. b e. b -> ( U. b u. c ) e. ( b u. { c } ) ) )
62 61 impcom 
 |-  ( ( U. b e. b /\ U. b C_ c ) -> ( U. b u. c ) e. ( b u. { c } ) )
63 uncom 
 |-  ( U. b u. c ) = ( c u. U. b )
64 ssequn1 
 |-  ( c C_ U. b <-> ( c u. U. b ) = U. b )
65 eleq1 
 |-  ( ( c u. U. b ) = U. b -> ( ( c u. U. b ) e. ( b u. { c } ) <-> U. b e. ( b u. { c } ) ) )
66 50 65 syl5ibr 
 |-  ( ( c u. U. b ) = U. b -> ( U. b e. b -> ( c u. U. b ) e. ( b u. { c } ) ) )
67 64 66 sylbi 
 |-  ( c C_ U. b -> ( U. b e. b -> ( c u. U. b ) e. ( b u. { c } ) ) )
68 67 impcom 
 |-  ( ( U. b e. b /\ c C_ U. b ) -> ( c u. U. b ) e. ( b u. { c } ) )
69 63 68 eqeltrid 
 |-  ( ( U. b e. b /\ c C_ U. b ) -> ( U. b u. c ) e. ( b u. { c } ) )
70 62 69 jaodan 
 |-  ( ( U. b e. b /\ ( U. b C_ c \/ c C_ U. b ) ) -> ( U. b u. c ) e. ( b u. { c } ) )
71 48 56 70 syl2anc 
 |-  ( ( ( b e. Fin /\ [C.] Or ( b u. { c } ) /\ ( b u. { c } ) =/= (/) ) /\ ( b =/= (/) /\ U. b e. b ) ) -> ( U. b u. c ) e. ( b u. { c } ) )
72 47 71 eqeltrid 
 |-  ( ( ( b e. Fin /\ [C.] Or ( b u. { c } ) /\ ( b u. { c } ) =/= (/) ) /\ ( b =/= (/) /\ U. b e. b ) ) -> U. ( b u. { c } ) e. ( b u. { c } ) )
73 72 expr 
 |-  ( ( ( b e. Fin /\ [C.] Or ( b u. { c } ) /\ ( b u. { c } ) =/= (/) ) /\ b =/= (/) ) -> ( U. b e. b -> U. ( b u. { c } ) e. ( b u. { c } ) ) )
74 44 73 embantd 
 |-  ( ( ( b e. Fin /\ [C.] Or ( b u. { c } ) /\ ( b u. { c } ) =/= (/) ) /\ b =/= (/) ) -> ( ( [C.] Or b -> U. b e. b ) -> U. ( b u. { c } ) e. ( b u. { c } ) ) )
75 40 74 embantd 
 |-  ( ( ( b e. Fin /\ [C.] Or ( b u. { c } ) /\ ( b u. { c } ) =/= (/) ) /\ b =/= (/) ) -> ( ( b =/= (/) -> ( [C.] Or b -> U. b e. b ) ) -> U. ( b u. { c } ) e. ( b u. { c } ) ) )
76 39 75 pm2.61dane 
 |-  ( ( b e. Fin /\ [C.] Or ( b u. { c } ) /\ ( b u. { c } ) =/= (/) ) -> ( ( b =/= (/) -> ( [C.] Or b -> U. b e. b ) ) -> U. ( b u. { c } ) e. ( b u. { c } ) ) )
77 76 3exp 
 |-  ( b e. Fin -> ( [C.] Or ( b u. { c } ) -> ( ( b u. { c } ) =/= (/) -> ( ( b =/= (/) -> ( [C.] Or b -> U. b e. b ) ) -> U. ( b u. { c } ) e. ( b u. { c } ) ) ) ) )
78 77 com24 
 |-  ( b e. Fin -> ( ( b =/= (/) -> ( [C.] Or b -> U. b e. b ) ) -> ( ( b u. { c } ) =/= (/) -> ( [C.] Or ( b u. { c } ) -> U. ( b u. { c } ) e. ( b u. { c } ) ) ) ) )
79 4 11 18 25 2 78 findcard2 
 |-  ( A e. Fin -> ( A =/= (/) -> ( [C.] Or A -> U. A e. A ) ) )
80 79 3imp21 
 |-  ( ( A =/= (/) /\ A e. Fin /\ [C.] Or A ) -> U. A e. A )