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 ( ( ( 𝐴 ≠ ∅ ∧ [⊊] Or 𝐴 ) ∧ ( 𝐵 ∈ Fin ∧ 𝐵 ⊆ ∪ 𝐴 ) ) → ∃ 𝑧 ∈ 𝐴 𝐵 ⊆ 𝑧 )

Proof

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