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≠∅∧[⊂]OrA∧B∈Fin∧B⊆⋃A→∃z∈AB⊆z

Proof

Step Hyp Ref Expression
1 sseq1 ⊢a=∅→a⊆⋃A↔∅⊆⋃A
2 sseq1 ⊢a=∅→a⊆z↔∅⊆z
3 2 rexbidv ⊢a=∅→∃z∈Aa⊆z↔∃z∈A∅⊆z
4 1 3 imbi12d ⊢a=∅→a⊆⋃A→∃z∈Aa⊆z↔∅⊆⋃A→∃z∈A∅⊆z
5 4 imbi2d ⊢a=∅→A≠∅∧[⊂]OrA→a⊆⋃A→∃z∈Aa⊆z↔A≠∅∧[⊂]OrA→∅⊆⋃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∈Aa⊆z↔∃z∈Ab⊆z
9 6 8 imbi12d ⊢a=b→a⊆⋃A→∃z∈Aa⊆z↔b⊆⋃A→∃z∈Ab⊆z
10 9 imbi2d ⊢a=b→A≠∅∧[⊂]OrA→a⊆⋃A→∃z∈Aa⊆z↔A≠∅∧[⊂]OrA→b⊆⋃A→∃z∈Ab⊆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∈Aa⊆z↔∃z∈Ab∪c⊆z
14 11 13 imbi12d ⊢a=b∪c→a⊆⋃A→∃z∈Aa⊆z↔b∪c⊆⋃A→∃z∈Ab∪c⊆z
15 14 imbi2d ⊢a=b∪c→A≠∅∧[⊂]OrA→a⊆⋃A→∃z∈Aa⊆z↔A≠∅∧[⊂]OrA→b∪c⊆⋃A→∃z∈Ab∪c⊆z
16 sseq1 ⊢a=B→a⊆⋃A↔B⊆⋃A
17 sseq1 ⊢a=B→a⊆z↔B⊆z
18 17 rexbidv ⊢a=B→∃z∈Aa⊆z↔∃z∈AB⊆z
19 16 18 imbi12d ⊢a=B→a⊆⋃A→∃z∈Aa⊆z↔B⊆⋃A→∃z∈AB⊆z
20 19 imbi2d ⊢a=B→A≠∅∧[⊂]OrA→a⊆⋃A→∃z∈Aa⊆z↔A≠∅∧[⊂]OrA→B⊆⋃A→∃z∈AB⊆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≠∅∧[⊂]OrA→∃z∈A∅⊆z
26 25 a1d ⊢A≠∅∧[⊂]OrA→∅⊆⋃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∈Ab⊆z→b∪c⊆⋃A→∃z∈Ab⊆z
30 sseq2 ⊢z=w→b⊆z↔b⊆w
31 30 cbvrexvw ⊢∃z∈Ab⊆z↔∃w∈Ab⊆w
32 simpr ⊢A≠∅∧[⊂]OrA∧b∪c⊆⋃A→b∪c⊆⋃A
33 32 unssbd ⊢A≠∅∧[⊂]OrA∧b∪c⊆⋃A→c⊆⋃A
34 vex ⊢c∈V
35 34 snss ⊢c∈⋃A↔c⊆⋃A
36 33 35 sylibr ⊢A≠∅∧[⊂]OrA∧b∪c⊆⋃A→c∈⋃A
37 eluni2 ⊢c∈⋃A↔∃u∈Ac∈u
38 36 37 sylib ⊢A≠∅∧[⊂]OrA∧b∪c⊆⋃A→∃u∈Ac∈u
39 reeanv ⊢∃u∈A∃w∈Ac∈u∧b⊆w↔∃u∈Ac∈u∧∃w∈Ab⊆w
40 simpllr ⊢A≠∅∧[⊂]OrA∧b∪c⊆⋃A∧u∈A∧w∈A∧c∈u∧b⊆w→[⊂]OrA
41 simprlr ⊢A≠∅∧[⊂]OrA∧b∪c⊆⋃A∧u∈A∧w∈A∧c∈u∧b⊆w→w∈A
42 simprll ⊢A≠∅∧[⊂]OrA∧b∪c⊆⋃A∧u∈A∧w∈A∧c∈u∧b⊆w→u∈A
43 sorpssun ⊢[⊂]OrA∧w∈A∧u∈A→w∪u∈A
44 40 41 42 43 syl12anc ⊢A≠∅∧[⊂]OrA∧b∪c⊆⋃A∧u∈A∧w∈A∧c∈u∧b⊆w→w∪u∈A
45 simprrr ⊢A≠∅∧[⊂]OrA∧b∪c⊆⋃A∧u∈A∧w∈A∧c∈u∧b⊆w→b⊆w
46 simprrl ⊢A≠∅∧[⊂]OrA∧b∪c⊆⋃A∧u∈A∧w∈A∧c∈u∧b⊆w→c∈u
47 46 snssd ⊢A≠∅∧[⊂]OrA∧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≠∅∧[⊂]OrA∧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∈Ab∪c⊆z
52 44 49 51 syl2anc ⊢A≠∅∧[⊂]OrA∧b∪c⊆⋃A∧u∈A∧w∈A∧c∈u∧b⊆w→∃z∈Ab∪c⊆z
53 52 expr ⊢A≠∅∧[⊂]OrA∧b∪c⊆⋃A∧u∈A∧w∈A→c∈u∧b⊆w→∃z∈Ab∪c⊆z
54 53 rexlimdvva ⊢A≠∅∧[⊂]OrA∧b∪c⊆⋃A→∃u∈A∃w∈Ac∈u∧b⊆w→∃z∈Ab∪c⊆z
55 39 54 biimtrrid ⊢A≠∅∧[⊂]OrA∧b∪c⊆⋃A→∃u∈Ac∈u∧∃w∈Ab⊆w→∃z∈Ab∪c⊆z
56 38 55 mpand ⊢A≠∅∧[⊂]OrA∧b∪c⊆⋃A→∃w∈Ab⊆w→∃z∈Ab∪c⊆z
57 31 56 biimtrid ⊢A≠∅∧[⊂]OrA∧b∪c⊆⋃A→∃z∈Ab⊆z→∃z∈Ab∪c⊆z
58 57 ex ⊢A≠∅∧[⊂]OrA→b∪c⊆⋃A→∃z∈Ab⊆z→∃z∈Ab∪c⊆z
59 58 a2d ⊢A≠∅∧[⊂]OrA→b∪c⊆⋃A→∃z∈Ab⊆z→b∪c⊆⋃A→∃z∈Ab∪c⊆z
60 29 59 syl5 ⊢A≠∅∧[⊂]OrA→b⊆⋃A→∃z∈Ab⊆z→b∪c⊆⋃A→∃z∈Ab∪c⊆z
61 60 a2i ⊢A≠∅∧[⊂]OrA→b⊆⋃A→∃z∈Ab⊆z→A≠∅∧[⊂]OrA→b∪c⊆⋃A→∃z∈Ab∪c⊆z
62 61 a1i ⊢b∈Fin→A≠∅∧[⊂]OrA→b⊆⋃A→∃z∈Ab⊆z→A≠∅∧[⊂]OrA→b∪c⊆⋃A→∃z∈Ab∪c⊆z
63 5 10 15 20 26 62 findcard2 ⊢B∈Fin→A≠∅∧[⊂]OrA→B⊆⋃A→∃z∈AB⊆z
64 63 com12 ⊢A≠∅∧[⊂]OrA→B∈Fin→B⊆⋃A→∃z∈AB⊆z
65 64 imp32 ⊢A≠∅∧[⊂]OrA∧B∈Fin∧B⊆⋃A→∃z∈AB⊆z