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 unisnv
 |-  U. { c } = c
27 vsnid
 |-  c e. { c }
28 26 27 eqeltri
 |-  U. { c } e. { c }
29 uneq1
 |-  ( b = (/) -> ( b u. { c } ) = ( (/) u. { c } ) )
30 uncom
 |-  ( (/) u. { c } ) = ( { c } u. (/) )
31 un0
 |-  ( { c } u. (/) ) = { c }
32 30 31 eqtri
 |-  ( (/) u. { c } ) = { c }
33 29 32 eqtrdi
 |-  ( b = (/) -> ( b u. { c } ) = { c } )
34 33 unieqd
 |-  ( b = (/) -> U. ( b u. { c } ) = U. { c } )
35 34 33 eleq12d
 |-  ( b = (/) -> ( U. ( b u. { c } ) e. ( b u. { c } ) <-> U. { c } e. { c } ) )
36 28 35 mpbiri
 |-  ( b = (/) -> U. ( b u. { c } ) e. ( b u. { c } ) )
37 36 a1d
 |-  ( b = (/) -> ( ( b =/= (/) -> ( [C.] Or b -> U. b e. b ) ) -> U. ( b u. { c } ) e. ( b u. { c } ) ) )
38 37 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 } ) ) )
39 simpr
 |-  ( ( ( b e. Fin /\ [C.] Or ( b u. { c } ) /\ ( b u. { c } ) =/= (/) ) /\ b =/= (/) ) -> b =/= (/) )
40 ssun1
 |-  b C_ ( b u. { c } )
41 simpl2
 |-  ( ( ( b e. Fin /\ [C.] Or ( b u. { c } ) /\ ( b u. { c } ) =/= (/) ) /\ b =/= (/) ) -> [C.] Or ( b u. { c } ) )
42 soss
 |-  ( b C_ ( b u. { c } ) -> ( [C.] Or ( b u. { c } ) -> [C.] Or b ) )
43 40 41 42 mpsyl
 |-  ( ( ( b e. Fin /\ [C.] Or ( b u. { c } ) /\ ( b u. { c } ) =/= (/) ) /\ b =/= (/) ) -> [C.] Or b )
44 uniun
 |-  U. ( b u. { c } ) = ( U. b u. U. { c } )
45 26 uneq2i
 |-  ( U. b u. U. { c } ) = ( U. b u. c )
46 44 45 eqtri
 |-  U. ( b u. { c } ) = ( U. b u. c )
47 simprr
 |-  ( ( ( b e. Fin /\ [C.] Or ( b u. { c } ) /\ ( b u. { c } ) =/= (/) ) /\ ( b =/= (/) /\ U. b e. b ) ) -> U. b e. b )
48 simpl2
 |-  ( ( ( b e. Fin /\ [C.] Or ( b u. { c } ) /\ ( b u. { c } ) =/= (/) ) /\ ( b =/= (/) /\ U. b e. b ) ) -> [C.] Or ( b u. { c } ) )
49 elun1
 |-  ( U. b e. b -> U. b e. ( b u. { c } ) )
50 49 ad2antll
 |-  ( ( ( b e. Fin /\ [C.] Or ( b u. { c } ) /\ ( b u. { c } ) =/= (/) ) /\ ( b =/= (/) /\ U. b e. b ) ) -> U. b e. ( b u. { c } ) )
51 ssun2
 |-  { c } C_ ( b u. { c } )
52 51 27 sselii
 |-  c e. ( b u. { c } )
53 52 a1i
 |-  ( ( ( b e. Fin /\ [C.] Or ( b u. { c } ) /\ ( b u. { c } ) =/= (/) ) /\ ( b =/= (/) /\ U. b e. b ) ) -> c e. ( b u. { c } ) )
54 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 ) )
55 48 50 53 54 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 ) )
56 ssequn1
 |-  ( U. b C_ c <-> ( U. b u. c ) = c )
57 52 a1i
 |-  ( U. b e. b -> c e. ( b u. { c } ) )
58 eleq1
 |-  ( ( U. b u. c ) = c -> ( ( U. b u. c ) e. ( b u. { c } ) <-> c e. ( b u. { c } ) ) )
59 57 58 imbitrrid
 |-  ( ( U. b u. c ) = c -> ( U. b e. b -> ( U. b u. c ) e. ( b u. { c } ) ) )
60 56 59 sylbi
 |-  ( U. b C_ c -> ( U. b e. b -> ( U. b u. c ) e. ( b u. { c } ) ) )
61 60 impcom
 |-  ( ( U. b e. b /\ U. b C_ c ) -> ( U. b u. c ) e. ( b u. { c } ) )
62 uncom
 |-  ( U. b u. c ) = ( c u. U. b )
63 ssequn1
 |-  ( c C_ U. b <-> ( c u. U. b ) = U. b )
64 eleq1
 |-  ( ( c u. U. b ) = U. b -> ( ( c u. U. b ) e. ( b u. { c } ) <-> U. b e. ( b u. { c } ) ) )
65 49 64 imbitrrid
 |-  ( ( c u. U. b ) = U. b -> ( U. b e. b -> ( c u. U. b ) e. ( b u. { c } ) ) )
66 63 65 sylbi
 |-  ( c C_ U. b -> ( U. b e. b -> ( c u. U. b ) e. ( b u. { c } ) ) )
67 66 impcom
 |-  ( ( U. b e. b /\ c C_ U. b ) -> ( c u. U. b ) e. ( b u. { c } ) )
68 62 67 eqeltrid
 |-  ( ( U. b e. b /\ c C_ U. b ) -> ( U. b u. c ) e. ( b u. { c } ) )
69 61 68 jaodan
 |-  ( ( U. b e. b /\ ( U. b C_ c \/ c C_ U. b ) ) -> ( U. b u. c ) e. ( b u. { c } ) )
70 47 55 69 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 } ) )
71 46 70 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 } ) )
72 71 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 } ) ) )
73 43 72 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 } ) ) )
74 39 73 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 } ) ) )
75 38 74 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 } ) ) )
76 75 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 } ) ) ) ) )
77 76 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 } ) ) ) ) )
78 4 11 18 25 2 77 findcard2
 |-  ( A e. Fin -> ( A =/= (/) -> ( [C.] Or A -> U. A e. A ) ) )
79 78 3imp21
 |-  ( ( A =/= (/) /\ A e. Fin /\ [C.] Or A ) -> U. A e. A )