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∈Fin∧[⊂]OrA→⋃A∈A

Proof

Step Hyp Ref Expression
1 eqneqall ⊢a=∅→a≠∅→[⊂]Ora→⋃a∈a
2 tru ⊢⊤
3 2 a1i ⊢a=∅→⊤
4 1 3 2thd ⊢a=∅→a≠∅→[⊂]Ora→⋃a∈a↔⊤
5 neeq1 ⊢a=b→a≠∅↔b≠∅
6 soeq2 ⊢a=b→[⊂]Ora↔[⊂]Orb
7 unieq ⊢a=b→⋃a=⋃b
8 id ⊢a=b→a=b
9 7 8 eleq12d ⊢a=b→⋃a∈a↔⋃b∈b
10 6 9 imbi12d ⊢a=b→[⊂]Ora→⋃a∈a↔[⊂]Orb→⋃b∈b
11 5 10 imbi12d ⊢a=b→a≠∅→[⊂]Ora→⋃a∈a↔b≠∅→[⊂]Orb→⋃b∈b
12 neeq1 ⊢a=b∪c→a≠∅↔b∪c≠∅
13 soeq2 ⊢a=b∪c→[⊂]Ora↔[⊂]Orb∪c
14 unieq ⊢a=b∪c→⋃a=⋃b∪c
15 id ⊢a=b∪c→a=b∪c
16 14 15 eleq12d ⊢a=b∪c→⋃a∈a↔⋃b∪c∈b∪c
17 13 16 imbi12d ⊢a=b∪c→[⊂]Ora→⋃a∈a↔[⊂]Orb∪c→⋃b∪c∈b∪c
18 12 17 imbi12d ⊢a=b∪c→a≠∅→[⊂]Ora→⋃a∈a↔b∪c≠∅→[⊂]Orb∪c→⋃b∪c∈b∪c
19 neeq1 ⊢a=A→a≠∅↔A≠∅
20 soeq2 ⊢a=A→[⊂]Ora↔[⊂]OrA
21 unieq ⊢a=A→⋃a=⋃A
22 id ⊢a=A→a=A
23 21 22 eleq12d ⊢a=A→⋃a∈a↔⋃A∈A
24 20 23 imbi12d ⊢a=A→[⊂]Ora→⋃a∈a↔[⊂]OrA→⋃A∈A
25 19 24 imbi12d ⊢a=A→a≠∅→[⊂]Ora→⋃a∈a↔A≠∅→[⊂]OrA→⋃A∈A
26 unisnv ⊢⋃c=c
27 vsnid ⊢c∈c
28 26 27 eqeltri ⊢⋃c∈c
29 uneq1 ⊢b=∅→b∪c=∅∪c
30 uncom ⊢∅∪c=c∪∅
31 un0 ⊢c∪∅=c
32 30 31 eqtri ⊢∅∪c=c
33 29 32 eqtrdi ⊢b=∅→b∪c=c
34 33 unieqd ⊢b=∅→⋃b∪c=⋃c
35 34 33 eleq12d ⊢b=∅→⋃b∪c∈b∪c↔⋃c∈c
36 28 35 mpbiri ⊢b=∅→⋃b∪c∈b∪c
37 36 a1d ⊢b=∅→b≠∅→[⊂]Orb→⋃b∈b→⋃b∪c∈b∪c
38 37 adantl ⊢b∈Fin∧[⊂]Orb∪c∧b∪c≠∅∧b=∅→b≠∅→[⊂]Orb→⋃b∈b→⋃b∪c∈b∪c
39 simpr ⊢b∈Fin∧[⊂]Orb∪c∧b∪c≠∅∧b≠∅→b≠∅
40 ssun1 ⊢b⊆b∪c
41 simpl2 ⊢b∈Fin∧[⊂]Orb∪c∧b∪c≠∅∧b≠∅→[⊂]Orb∪c
42 soss ⊢b⊆b∪c→[⊂]Orb∪c→[⊂]Orb
43 40 41 42 mpsyl ⊢b∈Fin∧[⊂]Orb∪c∧b∪c≠∅∧b≠∅→[⊂]Orb
44 uniun ⊢⋃b∪c=⋃b∪⋃c
45 26 uneq2i ⊢⋃b∪⋃c=⋃b∪c
46 44 45 eqtri ⊢⋃b∪c=⋃b∪c
47 simprr ⊢b∈Fin∧[⊂]Orb∪c∧b∪c≠∅∧b≠∅∧⋃b∈b→⋃b∈b
48 simpl2 ⊢b∈Fin∧[⊂]Orb∪c∧b∪c≠∅∧b≠∅∧⋃b∈b→[⊂]Orb∪c
49 elun1 ⊢⋃b∈b→⋃b∈b∪c
50 49 ad2antll ⊢b∈Fin∧[⊂]Orb∪c∧b∪c≠∅∧b≠∅∧⋃b∈b→⋃b∈b∪c
51 ssun2 ⊢c⊆b∪c
52 51 27 sselii ⊢c∈b∪c
53 52 a1i ⊢b∈Fin∧[⊂]Orb∪c∧b∪c≠∅∧b≠∅∧⋃b∈b→c∈b∪c
54 sorpssi ⊢[⊂]Orb∪c∧⋃b∈b∪c∧c∈b∪c→⋃b⊆c∨c⊆⋃b
55 48 50 53 54 syl12anc ⊢b∈Fin∧[⊂]Orb∪c∧b∪c≠∅∧b≠∅∧⋃b∈b→⋃b⊆c∨c⊆⋃b
56 ssequn1 ⊢⋃b⊆c↔⋃b∪c=c
57 52 a1i ⊢⋃b∈b→c∈b∪c
58 eleq1 ⊢⋃b∪c=c→⋃b∪c∈b∪c↔c∈b∪c
59 57 58 imbitrrid ⊢⋃b∪c=c→⋃b∈b→⋃b∪c∈b∪c
60 56 59 sylbi ⊢⋃b⊆c→⋃b∈b→⋃b∪c∈b∪c
61 60 impcom ⊢⋃b∈b∧⋃b⊆c→⋃b∪c∈b∪c
62 uncom ⊢⋃b∪c=c∪⋃b
63 ssequn1 ⊢c⊆⋃b↔c∪⋃b=⋃b
64 eleq1 ⊢c∪⋃b=⋃b→c∪⋃b∈b∪c↔⋃b∈b∪c
65 49 64 imbitrrid ⊢c∪⋃b=⋃b→⋃b∈b→c∪⋃b∈b∪c
66 63 65 sylbi ⊢c⊆⋃b→⋃b∈b→c∪⋃b∈b∪c
67 66 impcom ⊢⋃b∈b∧c⊆⋃b→c∪⋃b∈b∪c
68 62 67 eqeltrid ⊢⋃b∈b∧c⊆⋃b→⋃b∪c∈b∪c
69 61 68 jaodan ⊢⋃b∈b∧⋃b⊆c∨c⊆⋃b→⋃b∪c∈b∪c
70 47 55 69 syl2anc ⊢b∈Fin∧[⊂]Orb∪c∧b∪c≠∅∧b≠∅∧⋃b∈b→⋃b∪c∈b∪c
71 46 70 eqeltrid ⊢b∈Fin∧[⊂]Orb∪c∧b∪c≠∅∧b≠∅∧⋃b∈b→⋃b∪c∈b∪c
72 71 expr ⊢b∈Fin∧[⊂]Orb∪c∧b∪c≠∅∧b≠∅→⋃b∈b→⋃b∪c∈b∪c
73 43 72 embantd ⊢b∈Fin∧[⊂]Orb∪c∧b∪c≠∅∧b≠∅→[⊂]Orb→⋃b∈b→⋃b∪c∈b∪c
74 39 73 embantd ⊢b∈Fin∧[⊂]Orb∪c∧b∪c≠∅∧b≠∅→b≠∅→[⊂]Orb→⋃b∈b→⋃b∪c∈b∪c
75 38 74 pm2.61dane ⊢b∈Fin∧[⊂]Orb∪c∧b∪c≠∅→b≠∅→[⊂]Orb→⋃b∈b→⋃b∪c∈b∪c
76 75 3exp ⊢b∈Fin→[⊂]Orb∪c→b∪c≠∅→b≠∅→[⊂]Orb→⋃b∈b→⋃b∪c∈b∪c
77 76 com24 ⊢b∈Fin→b≠∅→[⊂]Orb→⋃b∈b→b∪c≠∅→[⊂]Orb∪c→⋃b∪c∈b∪c
78 4 11 18 25 2 77 findcard2 ⊢A∈Fin→A≠∅→[⊂]OrA→⋃A∈A
79 78 3imp21 ⊢A≠∅∧A∈Fin∧[⊂]OrA→⋃A∈A