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

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 )