Metamath Proof Explorer

Theorem finsschain

Description: A finite subset of the union of a superset chain is a subset of some element of the chain. A useful preliminary result for alexsub and others. (Contributed by Jeff Hankins, 25-Jan-2010) (Proof shortened by Mario Carneiro, 11-Feb-2015) (Revised by Mario Carneiro, 18-May-2015)

Ref Expression
Assertion finsschain ⊢ A ≠ ∅ ∧ [⊂] Or A ∧ B ∈ Fin ∧ B ⊆ ⋃ A → ∃ z ∈ A B ⊆ z

Proof

Step Hyp Ref Expression
1 sseq1 ⊢ a = ∅ → a ⊆ ⋃ A ↔ ∅ ⊆ ⋃ A
2 sseq1 ⊢ a = ∅ → a ⊆ z ↔ ∅ ⊆ z
3 2 rexbidv ⊢ a = ∅ → ∃ z ∈ A a ⊆ z ↔ ∃ z ∈ A ∅ ⊆ z
4 1 3 imbi12d ⊢ a = ∅ → a ⊆ ⋃ A → ∃ z ∈ A a ⊆ z ↔ ∅ ⊆ ⋃ A → ∃ z ∈ A ∅ ⊆ z
5 4 imbi2d ⊢ a = ∅ → A ≠ ∅ ∧ [⊂] Or A → a ⊆ ⋃ A → ∃ z ∈ A a ⊆ z ↔ A ≠ ∅ ∧ [⊂] Or A → ∅ ⊆ ⋃ A → ∃ z ∈ A ∅ ⊆ z
6 sseq1 ⊢ a = b → a ⊆ ⋃ A ↔ b ⊆ ⋃ A
7 sseq1 ⊢ a = b → a ⊆ z ↔ b ⊆ z
8 7 rexbidv ⊢ a = b → ∃ z ∈ A a ⊆ z ↔ ∃ z ∈ A b ⊆ z
9 6 8 imbi12d ⊢ a = b → a ⊆ ⋃ A → ∃ z ∈ A a ⊆ z ↔ b ⊆ ⋃ A → ∃ z ∈ A b ⊆ z
10 9 imbi2d ⊢ a = b → A ≠ ∅ ∧ [⊂] Or A → a ⊆ ⋃ A → ∃ z ∈ A a ⊆ z ↔ A ≠ ∅ ∧ [⊂] Or A → b ⊆ ⋃ A → ∃ z ∈ A b ⊆ z
11 sseq1 ⊢ a = b ∪ c → a ⊆ ⋃ A ↔ b ∪ c ⊆ ⋃ A
12 sseq1 ⊢ a = b ∪ c → a ⊆ z ↔ b ∪ c ⊆ z
13 12 rexbidv ⊢ a = b ∪ c → ∃ z ∈ A a ⊆ z ↔ ∃ z ∈ A b ∪ c ⊆ z
14 11 13 imbi12d ⊢ a = b ∪ c → a ⊆ ⋃ A → ∃ z ∈ A a ⊆ z ↔ b ∪ c ⊆ ⋃ A → ∃ z ∈ A b ∪ c ⊆ z
15 14 imbi2d ⊢ a = b ∪ c → A ≠ ∅ ∧ [⊂] Or A → a ⊆ ⋃ A → ∃ z ∈ A a ⊆ z ↔ A ≠ ∅ ∧ [⊂] Or A → b ∪ c ⊆ ⋃ A → ∃ z ∈ A b ∪ c ⊆ z
16 sseq1 ⊢ a = B → a ⊆ ⋃ A ↔ B ⊆ ⋃ A
17 sseq1 ⊢ a = B → a ⊆ z ↔ B ⊆ z
18 17 rexbidv ⊢ a = B → ∃ z ∈ A a ⊆ z ↔ ∃ z ∈ A B ⊆ z
19 16 18 imbi12d ⊢ a = B → a ⊆ ⋃ A → ∃ z ∈ A a ⊆ z ↔ B ⊆ ⋃ A → ∃ z ∈ A B ⊆ z
20 19 imbi2d ⊢ a = B → A ≠ ∅ ∧ [⊂] Or A → a ⊆ ⋃ A → ∃ z ∈ A a ⊆ z ↔ A ≠ ∅ ∧ [⊂] Or A → B ⊆ ⋃ A → ∃ z ∈ A B ⊆ z
21 0ss ⊢ ∅ ⊆ z
22 21 rgenw ⊢ ∀ z ∈ A ∅ ⊆ z
23 r19.2z ⊢ A ≠ ∅ ∧ ∀ z ∈ A ∅ ⊆ z → ∃ z ∈ A ∅ ⊆ z
24 22 23 mpan2 ⊢ A ≠ ∅ → ∃ z ∈ A ∅ ⊆ z
25 24 adantr ⊢ A ≠ ∅ ∧ [⊂] Or A → ∃ z ∈ A ∅ ⊆ z
26 25 a1d ⊢ A ≠ ∅ ∧ [⊂] Or A → ∅ ⊆ ⋃ A → ∃ z ∈ A ∅ ⊆ z
27 id ⊢ b ∪ c ⊆ ⋃ A → b ∪ c ⊆ ⋃ A
28 27 unssad ⊢ b ∪ c ⊆ ⋃ A → b ⊆ ⋃ A
29 28 imim1i ⊢ b ⊆ ⋃ A → ∃ z ∈ A b ⊆ z → b ∪ c ⊆ ⋃ A → ∃ z ∈ A b ⊆ z
30 sseq2 ⊢ z = w → b ⊆ z ↔ b ⊆ w
31 30 cbvrexvw ⊢ ∃ z ∈ A b ⊆ z ↔ ∃ w ∈ A b ⊆ w
32 simpr ⊢ A ≠ ∅ ∧ [⊂] Or A ∧ b ∪ c ⊆ ⋃ A → b ∪ c ⊆ ⋃ A
33 32 unssbd ⊢ A ≠ ∅ ∧ [⊂] Or A ∧ b ∪ c ⊆ ⋃ A → c ⊆ ⋃ A
34 vex ⊢ c ∈ V
35 34 snss ⊢ c ∈ ⋃ A ↔ c ⊆ ⋃ A
36 33 35 sylibr ⊢ A ≠ ∅ ∧ [⊂] Or A ∧ b ∪ c ⊆ ⋃ A → c ∈ ⋃ A
37 eluni2 ⊢ c ∈ ⋃ A ↔ ∃ u ∈ A c ∈ u
38 36 37 sylib ⊢ A ≠ ∅ ∧ [⊂] Or A ∧ b ∪ c ⊆ ⋃ A → ∃ u ∈ A c ∈ u
39 reeanv ⊢ ∃ u ∈ A ∃ w ∈ A c ∈ u ∧ b ⊆ w ↔ ∃ u ∈ A c ∈ u ∧ ∃ w ∈ A b ⊆ w
40 simpllr ⊢ A ≠ ∅ ∧ [⊂] Or A ∧ b ∪ c ⊆ ⋃ A ∧ u ∈ A ∧ w ∈ A ∧ c ∈ u ∧ b ⊆ w → [⊂] Or A
41 simprlr ⊢ A ≠ ∅ ∧ [⊂] Or A ∧ b ∪ c ⊆ ⋃ A ∧ u ∈ A ∧ w ∈ A ∧ c ∈ u ∧ b ⊆ w → w ∈ A
42 simprll ⊢ A ≠ ∅ ∧ [⊂] Or A ∧ b ∪ c ⊆ ⋃ A ∧ u ∈ A ∧ w ∈ A ∧ c ∈ u ∧ b ⊆ w → u ∈ A
43 sorpssun ⊢ [⊂] Or A ∧ w ∈ A ∧ u ∈ A → w ∪ u ∈ A
44 40 41 42 43 syl12anc ⊢ A ≠ ∅ ∧ [⊂] Or A ∧ b ∪ c ⊆ ⋃ A ∧ u ∈ A ∧ w ∈ A ∧ c ∈ u ∧ b ⊆ w → w ∪ u ∈ A
45 simprrr ⊢ A ≠ ∅ ∧ [⊂] Or A ∧ b ∪ c ⊆ ⋃ A ∧ u ∈ A ∧ w ∈ A ∧ c ∈ u ∧ b ⊆ w → b ⊆ w
46 simprrl ⊢ A ≠ ∅ ∧ [⊂] Or A ∧ b ∪ c ⊆ ⋃ A ∧ u ∈ A ∧ w ∈ A ∧ c ∈ u ∧ b ⊆ w → c ∈ u
47 46 snssd ⊢ A ≠ ∅ ∧ [⊂] Or A ∧ b ∪ c ⊆ ⋃ A ∧ u ∈ A ∧ w ∈ A ∧ c ∈ u ∧ b ⊆ w → c ⊆ u
48 unss12 ⊢ b ⊆ w ∧ c ⊆ u → b ∪ c ⊆ w ∪ u
49 45 47 48 syl2anc ⊢ A ≠ ∅ ∧ [⊂] Or A ∧ b ∪ c ⊆ ⋃ A ∧ u ∈ A ∧ w ∈ A ∧ c ∈ u ∧ b ⊆ w → b ∪ c ⊆ w ∪ u
50 sseq2 ⊢ z = w ∪ u → b ∪ c ⊆ z ↔ b ∪ c ⊆ w ∪ u
51 50 rspcev ⊢ w ∪ u ∈ A ∧ b ∪ c ⊆ w ∪ u → ∃ z ∈ A b ∪ c ⊆ z
52 44 49 51 syl2anc ⊢ A ≠ ∅ ∧ [⊂] Or A ∧ b ∪ c ⊆ ⋃ A ∧ u ∈ A ∧ w ∈ A ∧ c ∈ u ∧ b ⊆ w → ∃ z ∈ A b ∪ c ⊆ z
53 52 expr ⊢ A ≠ ∅ ∧ [⊂] Or A ∧ b ∪ c ⊆ ⋃ A ∧ u ∈ A ∧ w ∈ A → c ∈ u ∧ b ⊆ w → ∃ z ∈ A b ∪ c ⊆ z
54 53 rexlimdvva ⊢ A ≠ ∅ ∧ [⊂] Or A ∧ b ∪ c ⊆ ⋃ A → ∃ u ∈ A ∃ w ∈ A c ∈ u ∧ b ⊆ w → ∃ z ∈ A b ∪ c ⊆ z
55 39 54 syl5bir ⊢ A ≠ ∅ ∧ [⊂] Or A ∧ b ∪ c ⊆ ⋃ A → ∃ u ∈ A c ∈ u ∧ ∃ w ∈ A b ⊆ w → ∃ z ∈ A b ∪ c ⊆ z
56 38 55 mpand ⊢ A ≠ ∅ ∧ [⊂] Or A ∧ b ∪ c ⊆ ⋃ A → ∃ w ∈ A b ⊆ w → ∃ z ∈ A b ∪ c ⊆ z
57 31 56 syl5bi ⊢ A ≠ ∅ ∧ [⊂] Or A ∧ b ∪ c ⊆ ⋃ A → ∃ z ∈ A b ⊆ z → ∃ z ∈ A b ∪ c ⊆ z
58 57 ex ⊢ A ≠ ∅ ∧ [⊂] Or A → b ∪ c ⊆ ⋃ A → ∃ z ∈ A b ⊆ z → ∃ z ∈ A b ∪ c ⊆ z
59 58 a2d ⊢ A ≠ ∅ ∧ [⊂] Or A → b ∪ c ⊆ ⋃ A → ∃ z ∈ A b ⊆ z → b ∪ c ⊆ ⋃ A → ∃ z ∈ A b ∪ c ⊆ z
60 29 59 syl5 ⊢ A ≠ ∅ ∧ [⊂] Or A → b ⊆ ⋃ A → ∃ z ∈ A b ⊆ z → b ∪ c ⊆ ⋃ A → ∃ z ∈ A b ∪ c ⊆ z
61 60 a2i ⊢ A ≠ ∅ ∧ [⊂] Or A → b ⊆ ⋃ A → ∃ z ∈ A b ⊆ z → A ≠ ∅ ∧ [⊂] Or A → b ∪ c ⊆ ⋃ A → ∃ z ∈ A b ∪ c ⊆ z
62 61 a1i ⊢ b ∈ Fin → A ≠ ∅ ∧ [⊂] Or A → b ⊆ ⋃ A → ∃ z ∈ A b ⊆ z → A ≠ ∅ ∧ [⊂] Or A → b ∪ c ⊆ ⋃ A → ∃ z ∈ A b ∪ c ⊆ z
63 5 10 15 20 26 62 findcard2 ⊢ B ∈ Fin → A ≠ ∅ ∧ [⊂] Or A → B ⊆ ⋃ A → ∃ z ∈ A B ⊆ z
64 63 com12 ⊢ A ≠ ∅ ∧ [⊂] Or A → B ∈ Fin → B ⊆ ⋃ A → ∃ z ∈ A B ⊆ z
65 64 imp32 ⊢ A ≠ ∅ ∧ [⊂] Or A ∧ B ∈ Fin ∧ B ⊆ ⋃ A → ∃ z ∈ A B ⊆ z