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 vex ⊢ c ∈ V
27 26 unisn ⊢ ⋃ c = c
28 vsnid ⊢ c ∈ c
29 27 28 eqeltri ⊢ ⋃ c ∈ c
30 uneq1 ⊢ b = ∅ → b ∪ c = ∅ ∪ c
31 uncom ⊢ ∅ ∪ c = c ∪ ∅
32 un0 ⊢ c ∪ ∅ = c
33 31 32 eqtri ⊢ ∅ ∪ c = c
34 30 33 eqtrdi ⊢ b = ∅ → b ∪ c = c
35 34 unieqd ⊢ b = ∅ → ⋃ b ∪ c = ⋃ c
36 35 34 eleq12d ⊢ b = ∅ → ⋃ b ∪ c ∈ b ∪ c ↔ ⋃ c ∈ c
37 29 36 mpbiri ⊢ b = ∅ → ⋃ b ∪ c ∈ b ∪ c
38 37 a1d ⊢ b = ∅ → b ≠ ∅ → [⊂] Or b → ⋃ b ∈ b → ⋃ b ∪ c ∈ b ∪ c
39 38 adantl ⊢ b ∈ Fin ∧ [⊂] Or b ∪ c ∧ b ∪ c ≠ ∅ ∧ b = ∅ → b ≠ ∅ → [⊂] Or b → ⋃ b ∈ b → ⋃ b ∪ c ∈ b ∪ c
40 simpr ⊢ b ∈ Fin ∧ [⊂] Or b ∪ c ∧ b ∪ c ≠ ∅ ∧ b ≠ ∅ → b ≠ ∅
41 ssun1 ⊢ b ⊆ b ∪ c
42 simpl2 ⊢ b ∈ Fin ∧ [⊂] Or b ∪ c ∧ b ∪ c ≠ ∅ ∧ b ≠ ∅ → [⊂] Or b ∪ c
43 soss ⊢ b ⊆ b ∪ c → [⊂] Or b ∪ c → [⊂] Or b
44 41 42 43 mpsyl ⊢ b ∈ Fin ∧ [⊂] Or b ∪ c ∧ b ∪ c ≠ ∅ ∧ b ≠ ∅ → [⊂] Or b
45 uniun ⊢ ⋃ b ∪ c = ⋃ b ∪ ⋃ c
46 27 uneq2i ⊢ ⋃ b ∪ ⋃ c = ⋃ b ∪ c
47 45 46 eqtri ⊢ ⋃ b ∪ c = ⋃ b ∪ c
48 simprr ⊢ b ∈ Fin ∧ [⊂] Or b ∪ c ∧ b ∪ c ≠ ∅ ∧ b ≠ ∅ ∧ ⋃ b ∈ b → ⋃ b ∈ b
49 simpl2 ⊢ b ∈ Fin ∧ [⊂] Or b ∪ c ∧ b ∪ c ≠ ∅ ∧ b ≠ ∅ ∧ ⋃ b ∈ b → [⊂] Or b ∪ c
50 elun1 ⊢ ⋃ b ∈ b → ⋃ b ∈ b ∪ c
51 50 ad2antll ⊢ b ∈ Fin ∧ [⊂] Or b ∪ c ∧ b ∪ c ≠ ∅ ∧ b ≠ ∅ ∧ ⋃ b ∈ b → ⋃ b ∈ b ∪ c
52 ssun2 ⊢ c ⊆ b ∪ c
53 52 28 sselii ⊢ c ∈ b ∪ c
54 53 a1i ⊢ b ∈ Fin ∧ [⊂] Or b ∪ c ∧ b ∪ c ≠ ∅ ∧ b ≠ ∅ ∧ ⋃ b ∈ b → c ∈ b ∪ c
55 sorpssi ⊢ [⊂] Or b ∪ c ∧ ⋃ b ∈ b ∪ c ∧ c ∈ b ∪ c → ⋃ b ⊆ c ∨ c ⊆ ⋃ b
56 49 51 54 55 syl12anc ⊢ b ∈ Fin ∧ [⊂] Or b ∪ c ∧ b ∪ c ≠ ∅ ∧ b ≠ ∅ ∧ ⋃ b ∈ b → ⋃ b ⊆ c ∨ c ⊆ ⋃ b
57 ssequn1 ⊢ ⋃ b ⊆ c ↔ ⋃ b ∪ c = c
58 53 a1i ⊢ ⋃ b ∈ b → c ∈ b ∪ c
59 eleq1 ⊢ ⋃ b ∪ c = c → ⋃ b ∪ c ∈ b ∪ c ↔ c ∈ b ∪ c
60 58 59 syl5ibr ⊢ ⋃ b ∪ c = c → ⋃ b ∈ b → ⋃ b ∪ c ∈ b ∪ c
61 57 60 sylbi ⊢ ⋃ b ⊆ c → ⋃ b ∈ b → ⋃ b ∪ c ∈ b ∪ c
62 61 impcom ⊢ ⋃ b ∈ b ∧ ⋃ b ⊆ c → ⋃ b ∪ c ∈ b ∪ c
63 uncom ⊢ ⋃ b ∪ c = c ∪ ⋃ b
64 ssequn1 ⊢ c ⊆ ⋃ b ↔ c ∪ ⋃ b = ⋃ b
65 eleq1 ⊢ c ∪ ⋃ b = ⋃ b → c ∪ ⋃ b ∈ b ∪ c ↔ ⋃ b ∈ b ∪ c
66 50 65 syl5ibr ⊢ c ∪ ⋃ b = ⋃ b → ⋃ b ∈ b → c ∪ ⋃ b ∈ b ∪ c
67 64 66 sylbi ⊢ c ⊆ ⋃ b → ⋃ b ∈ b → c ∪ ⋃ b ∈ b ∪ c
68 67 impcom ⊢ ⋃ b ∈ b ∧ c ⊆ ⋃ b → c ∪ ⋃ b ∈ b ∪ c
69 63 68 eqeltrid ⊢ ⋃ b ∈ b ∧ c ⊆ ⋃ b → ⋃ b ∪ c ∈ b ∪ c
70 62 69 jaodan ⊢ ⋃ b ∈ b ∧ ⋃ b ⊆ c ∨ c ⊆ ⋃ b → ⋃ b ∪ c ∈ b ∪ c
71 48 56 70 syl2anc ⊢ b ∈ Fin ∧ [⊂] Or b ∪ c ∧ b ∪ c ≠ ∅ ∧ b ≠ ∅ ∧ ⋃ b ∈ b → ⋃ b ∪ c ∈ b ∪ c
72 47 71 eqeltrid ⊢ b ∈ Fin ∧ [⊂] Or b ∪ c ∧ b ∪ c ≠ ∅ ∧ b ≠ ∅ ∧ ⋃ b ∈ b → ⋃ b ∪ c ∈ b ∪ c
73 72 expr ⊢ b ∈ Fin ∧ [⊂] Or b ∪ c ∧ b ∪ c ≠ ∅ ∧ b ≠ ∅ → ⋃ b ∈ b → ⋃ b ∪ c ∈ b ∪ c
74 44 73 embantd ⊢ b ∈ Fin ∧ [⊂] Or b ∪ c ∧ b ∪ c ≠ ∅ ∧ b ≠ ∅ → [⊂] Or b → ⋃ b ∈ b → ⋃ b ∪ c ∈ b ∪ c
75 40 74 embantd ⊢ b ∈ Fin ∧ [⊂] Or b ∪ c ∧ b ∪ c ≠ ∅ ∧ b ≠ ∅ → b ≠ ∅ → [⊂] Or b → ⋃ b ∈ b → ⋃ b ∪ c ∈ b ∪ c
76 39 75 pm2.61dane ⊢ b ∈ Fin ∧ [⊂] Or b ∪ c ∧ b ∪ c ≠ ∅ → b ≠ ∅ → [⊂] Or b → ⋃ b ∈ b → ⋃ b ∪ c ∈ b ∪ c
77 76 3exp ⊢ b ∈ Fin → [⊂] Or b ∪ c → b ∪ c ≠ ∅ → b ≠ ∅ → [⊂] Or b → ⋃ b ∈ b → ⋃ b ∪ c ∈ b ∪ c
78 77 com24 ⊢ b ∈ Fin → b ≠ ∅ → [⊂] Or b → ⋃ b ∈ b → b ∪ c ≠ ∅ → [⊂] Or b ∪ c → ⋃ b ∪ c ∈ b ∪ c
79 4 11 18 25 2 78 findcard2 ⊢ A ∈ Fin → A ≠ ∅ → [⊂] Or A → ⋃ A ∈ A
80 79 3imp21 ⊢ A ≠ ∅ ∧ A ∈ Fin ∧ [⊂] Or A → ⋃ A ∈ A