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

Proof

Step Hyp Ref Expression
1 eqneqall ⊢ a = ∅ → a ≠ ∅ → [⊂] Or a → ⋃ a ∈ a
2 tru ⊢ ⊤
3 2 a1i ⊢ a = ∅ → ⊤
4 1 3 2thd ⊢ a = ∅ → a ≠ ∅ → [⊂] Or a → ⋃ a ∈ a ↔ ⊤
5 neeq1 ⊢ a = b → a ≠ ∅ ↔ b ≠ ∅
6 soeq2 ⊢ a = b → [⊂] Or a ↔ [⊂] Or b
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 → [⊂] Or a → ⋃ a ∈ a ↔ [⊂] Or b → ⋃ b ∈ b
11 5 10 imbi12d ⊢ a = b → a ≠ ∅ → [⊂] Or a → ⋃ a ∈ a ↔ b ≠ ∅ → [⊂] Or b → ⋃ b ∈ b
12 neeq1 ⊢ a = b ∪ c → a ≠ ∅ ↔ b ∪ c ≠ ∅
13 soeq2 ⊢ a = b ∪ c → [⊂] Or a ↔ [⊂] Or b ∪ 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 → [⊂] Or a → ⋃ a ∈ a ↔ [⊂] Or b ∪ c → ⋃ b ∪ c ∈ b ∪ c
18 12 17 imbi12d ⊢ a = b ∪ c → a ≠ ∅ → [⊂] Or a → ⋃ a ∈ a ↔ b ∪ c ≠ ∅ → [⊂] Or b ∪ c → ⋃ b ∪ c ∈ b ∪ c
19 neeq1 ⊢ a = A → a ≠ ∅ ↔ A ≠ ∅
20 soeq2 ⊢ a = A → [⊂] Or a ↔ [⊂] Or A
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 → [⊂] Or a → ⋃ a ∈ a ↔ [⊂] Or A → ⋃ A ∈ A
25 19 24 imbi12d ⊢ a = A → a ≠ ∅ → [⊂] Or a → ⋃ a ∈ a ↔ A ≠ ∅ → [⊂] Or A → ⋃ 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 ≠ ∅ → [⊂] Or b → ⋃ b ∈ b → ⋃ b ∪ c ∈ b ∪ c
38 37 adantl ⊢ b ∈ Fin ∧ [⊂] Or b ∪ c ∧ b ∪ c ≠ ∅ ∧ b = ∅ → b ≠ ∅ → [⊂] Or b → ⋃ b ∈ b → ⋃ b ∪ c ∈ b ∪ c
39 simpr ⊢ b ∈ Fin ∧ [⊂] Or b ∪ c ∧ b ∪ c ≠ ∅ ∧ b ≠ ∅ → b ≠ ∅
40 ssun1 ⊢ b ⊆ b ∪ c
41 simpl2 ⊢ b ∈ Fin ∧ [⊂] Or b ∪ c ∧ b ∪ c ≠ ∅ ∧ b ≠ ∅ → [⊂] Or b ∪ c
42 soss ⊢ b ⊆ b ∪ c → [⊂] Or b ∪ c → [⊂] Or b
43 40 41 42 mpsyl ⊢ b ∈ Fin ∧ [⊂] Or b ∪ c ∧ b ∪ c ≠ ∅ ∧ b ≠ ∅ → [⊂] Or b
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 ∧ [⊂] Or b ∪ c ∧ b ∪ c ≠ ∅ ∧ b ≠ ∅ ∧ ⋃ b ∈ b → ⋃ b ∈ b
48 simpl2 ⊢ b ∈ Fin ∧ [⊂] Or b ∪ c ∧ b ∪ c ≠ ∅ ∧ b ≠ ∅ ∧ ⋃ b ∈ b → [⊂] Or b ∪ c
49 elun1 ⊢ ⋃ b ∈ b → ⋃ b ∈ b ∪ c
50 49 ad2antll ⊢ b ∈ Fin ∧ [⊂] Or b ∪ 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 ∧ [⊂] Or b ∪ c ∧ b ∪ c ≠ ∅ ∧ b ≠ ∅ ∧ ⋃ b ∈ b → c ∈ b ∪ c
54 sorpssi ⊢ [⊂] Or b ∪ c ∧ ⋃ b ∈ b ∪ c ∧ c ∈ b ∪ c → ⋃ b ⊆ c ∨ c ⊆ ⋃ b
55 48 50 53 54 syl12anc ⊢ b ∈ Fin ∧ [⊂] Or b ∪ 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 ∧ [⊂] Or b ∪ c ∧ b ∪ c ≠ ∅ ∧ b ≠ ∅ ∧ ⋃ b ∈ b → ⋃ b ∪ c ∈ b ∪ c
71 46 70 eqeltrid ⊢ b ∈ Fin ∧ [⊂] Or b ∪ c ∧ b ∪ c ≠ ∅ ∧ b ≠ ∅ ∧ ⋃ b ∈ b → ⋃ b ∪ c ∈ b ∪ c
72 71 expr ⊢ b ∈ Fin ∧ [⊂] Or b ∪ c ∧ b ∪ c ≠ ∅ ∧ b ≠ ∅ → ⋃ b ∈ b → ⋃ b ∪ c ∈ b ∪ c
73 43 72 embantd ⊢ b ∈ Fin ∧ [⊂] Or b ∪ c ∧ b ∪ c ≠ ∅ ∧ b ≠ ∅ → [⊂] Or b → ⋃ b ∈ b → ⋃ b ∪ c ∈ b ∪ c
74 39 73 embantd ⊢ b ∈ Fin ∧ [⊂] Or b ∪ c ∧ b ∪ c ≠ ∅ ∧ b ≠ ∅ → b ≠ ∅ → [⊂] Or b → ⋃ b ∈ b → ⋃ b ∪ c ∈ b ∪ c
75 38 74 pm2.61dane ⊢ b ∈ Fin ∧ [⊂] Or b ∪ c ∧ b ∪ c ≠ ∅ → b ≠ ∅ → [⊂] Or b → ⋃ b ∈ b → ⋃ b ∪ c ∈ b ∪ c
76 75 3exp ⊢ b ∈ Fin → [⊂] Or b ∪ c → b ∪ c ≠ ∅ → b ≠ ∅ → [⊂] Or b → ⋃ b ∈ b → ⋃ b ∪ c ∈ b ∪ c
77 76 com24 ⊢ b ∈ Fin → b ≠ ∅ → [⊂] Or b → ⋃ b ∈ b → b ∪ c ≠ ∅ → [⊂] Or b ∪ c → ⋃ b ∪ c ∈ b ∪ c
78 4 11 18 25 2 77 findcard2 ⊢ A ∈ Fin → A ≠ ∅ → [⊂] Or A → ⋃ A ∈ A
79 78 3imp21 ⊢ A ≠ ∅ ∧ A ∈ Fin ∧ [⊂] Or A → ⋃ A ∈ A