This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iunincfi

Description: Given a sequence of increasing sets, the union of a finite subsequence, is its last element. (Contributed by Glauco Siliprandi, 8-Apr-2021)

Ref Expression
Hypotheses iunincfi.1 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
iunincfi.2 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
Assertion iunincfi ( 𝜑 → ∪ 𝑛 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 iunincfi.1 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
2 iunincfi.2 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
3 eliun ⊢ ( 𝑥 ∈ ∪ 𝑛 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑛 ) ↔ ∃ 𝑛 ∈ ( 𝑀 ... 𝑁 ) 𝑥 ∈ ( 𝐹 ‘ 𝑛 ) )
4 3 biimpi ⊢ ( 𝑥 ∈ ∪ 𝑛 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑛 ) → ∃ 𝑛 ∈ ( 𝑀 ... 𝑁 ) 𝑥 ∈ ( 𝐹 ‘ 𝑛 ) )
5 4 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝑛 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑛 ) ) → ∃ 𝑛 ∈ ( 𝑀 ... 𝑁 ) 𝑥 ∈ ( 𝐹 ‘ 𝑛 ) )
6 elfzuz3 ⊢ ( 𝑛 ∈ ( 𝑀 ... 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑛 ) )
7 6 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑛 ) )
8 simpll ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 𝑛 ..^ 𝑁 ) ) → 𝜑 )
9 elfzuz ⊢ ( 𝑛 ∈ ( 𝑀 ... 𝑁 ) → 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) )
10 fzoss1 ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑛 ..^ 𝑁 ) ⊆ ( 𝑀 ..^ 𝑁 ) )
11 9 10 syl ⊢ ( 𝑛 ∈ ( 𝑀 ... 𝑁 ) → ( 𝑛 ..^ 𝑁 ) ⊆ ( 𝑀 ..^ 𝑁 ) )
12 11 adantr ⊢ ( ( 𝑛 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑚 ∈ ( 𝑛 ..^ 𝑁 ) ) → ( 𝑛 ..^ 𝑁 ) ⊆ ( 𝑀 ..^ 𝑁 ) )
13 simpr ⊢ ( ( 𝑛 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑚 ∈ ( 𝑛 ..^ 𝑁 ) ) → 𝑚 ∈ ( 𝑛 ..^ 𝑁 ) )
14 12 13 sseldd ⊢ ( ( 𝑛 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑚 ∈ ( 𝑛 ..^ 𝑁 ) ) → 𝑚 ∈ ( 𝑀 ..^ 𝑁 ) )
15 14 adantll ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 𝑛 ..^ 𝑁 ) ) → 𝑚 ∈ ( 𝑀 ..^ 𝑁 ) )
16 eleq1w ⊢ ( 𝑛 = 𝑚 → ( 𝑛 ∈ ( 𝑀 ..^ 𝑁 ) ↔ 𝑚 ∈ ( 𝑀 ..^ 𝑁 ) ) )
17 16 anbi2d ⊢ ( 𝑛 = 𝑚 → ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ..^ 𝑁 ) ) ↔ ( 𝜑 ∧ 𝑚 ∈ ( 𝑀 ..^ 𝑁 ) ) ) )
18 fveq2 ⊢ ( 𝑛 = 𝑚 → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑚 ) )
19 fvoveq1 ⊢ ( 𝑛 = 𝑚 → ( 𝐹 ‘ ( 𝑛 + 1 ) ) = ( 𝐹 ‘ ( 𝑚 + 1 ) ) )
20 18 19 sseq12d ⊢ ( 𝑛 = 𝑚 → ( ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ↔ ( 𝐹 ‘ 𝑚 ) ⊆ ( 𝐹 ‘ ( 𝑚 + 1 ) ) ) )
21 17 20 imbi12d ⊢ ( 𝑛 = 𝑚 → ( ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ↔ ( ( 𝜑 ∧ 𝑚 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝐹 ‘ 𝑚 ) ⊆ ( 𝐹 ‘ ( 𝑚 + 1 ) ) ) ) )
22 21 2 chvarvv ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝐹 ‘ 𝑚 ) ⊆ ( 𝐹 ‘ ( 𝑚 + 1 ) ) )
23 8 15 22 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 𝑛 ..^ 𝑁 ) ) → ( 𝐹 ‘ 𝑚 ) ⊆ ( 𝐹 ‘ ( 𝑚 + 1 ) ) )
24 7 23 ssinc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ 𝑁 ) )
25 24 3adant3 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑥 ∈ ( 𝐹 ‘ 𝑛 ) ) → ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ 𝑁 ) )
26 simp3 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑥 ∈ ( 𝐹 ‘ 𝑛 ) ) → 𝑥 ∈ ( 𝐹 ‘ 𝑛 ) )
27 25 26 sseldd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑥 ∈ ( 𝐹 ‘ 𝑛 ) ) → 𝑥 ∈ ( 𝐹 ‘ 𝑁 ) )
28 27 3exp ⊢ ( 𝜑 → ( 𝑛 ∈ ( 𝑀 ... 𝑁 ) → ( 𝑥 ∈ ( 𝐹 ‘ 𝑛 ) → 𝑥 ∈ ( 𝐹 ‘ 𝑁 ) ) ) )
29 28 rexlimdv ⊢ ( 𝜑 → ( ∃ 𝑛 ∈ ( 𝑀 ... 𝑁 ) 𝑥 ∈ ( 𝐹 ‘ 𝑛 ) → 𝑥 ∈ ( 𝐹 ‘ 𝑁 ) ) )
30 29 imp ⊢ ( ( 𝜑 ∧ ∃ 𝑛 ∈ ( 𝑀 ... 𝑁 ) 𝑥 ∈ ( 𝐹 ‘ 𝑛 ) ) → 𝑥 ∈ ( 𝐹 ‘ 𝑁 ) )
31 5 30 syldan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝑛 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑛 ) ) → 𝑥 ∈ ( 𝐹 ‘ 𝑁 ) )
32 31 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ∪ 𝑛 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑛 ) 𝑥 ∈ ( 𝐹 ‘ 𝑁 ) )
33 dfss3 ⊢ ( ∪ 𝑛 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ 𝑁 ) ↔ ∀ 𝑥 ∈ ∪ 𝑛 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑛 ) 𝑥 ∈ ( 𝐹 ‘ 𝑁 ) )
34 32 33 sylibr ⊢ ( 𝜑 → ∪ 𝑛 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ 𝑁 ) )
35 eluzfz2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ( 𝑀 ... 𝑁 ) )
36 1 35 syl ⊢ ( 𝜑 → 𝑁 ∈ ( 𝑀 ... 𝑁 ) )
37 fveq2 ⊢ ( 𝑛 = 𝑁 → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑁 ) )
38 37 ssiun2s ⊢ ( 𝑁 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐹 ‘ 𝑁 ) ⊆ ∪ 𝑛 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑛 ) )
39 36 38 syl ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑁 ) ⊆ ∪ 𝑛 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑛 ) )
40 34 39 eqssd ⊢ ( 𝜑 → ∪ 𝑛 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑁 ) )