Metamath Proof Explorer

Theorem iuninc

Description: The union of an increasing collection of sets is its last element. (Contributed by Thierry Arnoux, 22-Jan-2017)

Ref Expression
Hypotheses iuninc.1 ⊢ ( 𝜑 → 𝐹 Fn ℕ )
iuninc.2 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
Assertion iuninc ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ∪ 𝑛 ∈ ( 1 ... 𝑖 ) ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑖 ) )

Proof

Step Hyp Ref Expression
1 iuninc.1 ⊢ ( 𝜑 → 𝐹 Fn ℕ )
2 iuninc.2 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
3 oveq2 ⊢ ( 𝑗 = 1 → ( 1 ... 𝑗 ) = ( 1 ... 1 ) )
4 3 iuneq1d ⊢ ( 𝑗 = 1 → ∪ 𝑛 ∈ ( 1 ... 𝑗 ) ( 𝐹 ‘ 𝑛 ) = ∪ 𝑛 ∈ ( 1 ... 1 ) ( 𝐹 ‘ 𝑛 ) )
5 fveq2 ⊢ ( 𝑗 = 1 → ( 𝐹 ‘ 𝑗 ) = ( 𝐹 ‘ 1 ) )
6 4 5 eqeq12d ⊢ ( 𝑗 = 1 → ( ∪ 𝑛 ∈ ( 1 ... 𝑗 ) ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑗 ) ↔ ∪ 𝑛 ∈ ( 1 ... 1 ) ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 1 ) ) )
7 6 imbi2d ⊢ ( 𝑗 = 1 → ( ( 𝜑 → ∪ 𝑛 ∈ ( 1 ... 𝑗 ) ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑗 ) ) ↔ ( 𝜑 → ∪ 𝑛 ∈ ( 1 ... 1 ) ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 1 ) ) ) )
8 oveq2 ⊢ ( 𝑗 = 𝑘 → ( 1 ... 𝑗 ) = ( 1 ... 𝑘 ) )
9 8 iuneq1d ⊢ ( 𝑗 = 𝑘 → ∪ 𝑛 ∈ ( 1 ... 𝑗 ) ( 𝐹 ‘ 𝑛 ) = ∪ 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹 ‘ 𝑛 ) )
10 fveq2 ⊢ ( 𝑗 = 𝑘 → ( 𝐹 ‘ 𝑗 ) = ( 𝐹 ‘ 𝑘 ) )
11 9 10 eqeq12d ⊢ ( 𝑗 = 𝑘 → ( ∪ 𝑛 ∈ ( 1 ... 𝑗 ) ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑗 ) ↔ ∪ 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑘 ) ) )
12 11 imbi2d ⊢ ( 𝑗 = 𝑘 → ( ( 𝜑 → ∪ 𝑛 ∈ ( 1 ... 𝑗 ) ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑗 ) ) ↔ ( 𝜑 → ∪ 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑘 ) ) ) )
13 oveq2 ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( 1 ... 𝑗 ) = ( 1 ... ( 𝑘 + 1 ) ) )
14 13 iuneq1d ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ∪ 𝑛 ∈ ( 1 ... 𝑗 ) ( 𝐹 ‘ 𝑛 ) = ∪ 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹 ‘ 𝑛 ) )
15 fveq2 ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( 𝐹 ‘ 𝑗 ) = ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
16 14 15 eqeq12d ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ∪ 𝑛 ∈ ( 1 ... 𝑗 ) ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑗 ) ↔ ∪ 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) )
17 16 imbi2d ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( 𝜑 → ∪ 𝑛 ∈ ( 1 ... 𝑗 ) ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑗 ) ) ↔ ( 𝜑 → ∪ 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) )
18 oveq2 ⊢ ( 𝑗 = 𝑖 → ( 1 ... 𝑗 ) = ( 1 ... 𝑖 ) )
19 18 iuneq1d ⊢ ( 𝑗 = 𝑖 → ∪ 𝑛 ∈ ( 1 ... 𝑗 ) ( 𝐹 ‘ 𝑛 ) = ∪ 𝑛 ∈ ( 1 ... 𝑖 ) ( 𝐹 ‘ 𝑛 ) )
20 fveq2 ⊢ ( 𝑗 = 𝑖 → ( 𝐹 ‘ 𝑗 ) = ( 𝐹 ‘ 𝑖 ) )
21 19 20 eqeq12d ⊢ ( 𝑗 = 𝑖 → ( ∪ 𝑛 ∈ ( 1 ... 𝑗 ) ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑗 ) ↔ ∪ 𝑛 ∈ ( 1 ... 𝑖 ) ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑖 ) ) )
22 21 imbi2d ⊢ ( 𝑗 = 𝑖 → ( ( 𝜑 → ∪ 𝑛 ∈ ( 1 ... 𝑗 ) ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑗 ) ) ↔ ( 𝜑 → ∪ 𝑛 ∈ ( 1 ... 𝑖 ) ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑖 ) ) ) )
23 1z ⊢ 1 ∈ ℤ
24 fzsn ⊢ ( 1 ∈ ℤ → ( 1 ... 1 ) = { 1 } )
25 iuneq1 ⊢ ( ( 1 ... 1 ) = { 1 } → ∪ 𝑛 ∈ ( 1 ... 1 ) ( 𝐹 ‘ 𝑛 ) = ∪ 𝑛 ∈ { 1 } ( 𝐹 ‘ 𝑛 ) )
26 23 24 25 mp2b ⊢ ∪ 𝑛 ∈ ( 1 ... 1 ) ( 𝐹 ‘ 𝑛 ) = ∪ 𝑛 ∈ { 1 } ( 𝐹 ‘ 𝑛 )
27 1ex ⊢ 1 ∈ V
28 fveq2 ⊢ ( 𝑛 = 1 → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 1 ) )
29 27 28 iunxsn ⊢ ∪ 𝑛 ∈ { 1 } ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 1 )
30 26 29 eqtri ⊢ ∪ 𝑛 ∈ ( 1 ... 1 ) ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 1 )
31 30 a1i ⊢ ( 𝜑 → ∪ 𝑛 ∈ ( 1 ... 1 ) ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 1 ) )
32 simpll ⊢ ( ( ( 𝑘 ∈ ℕ ∧ 𝜑 ) ∧ ∪ 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑘 ) ) → 𝑘 ∈ ℕ )
33 elnnuz ⊢ ( 𝑘 ∈ ℕ ↔ 𝑘 ∈ ( ℤ≥ ‘ 1 ) )
34 fzsuc ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 1 ) → ( 1 ... ( 𝑘 + 1 ) ) = ( ( 1 ... 𝑘 ) ∪ { ( 𝑘 + 1 ) } ) )
35 33 34 sylbi ⊢ ( 𝑘 ∈ ℕ → ( 1 ... ( 𝑘 + 1 ) ) = ( ( 1 ... 𝑘 ) ∪ { ( 𝑘 + 1 ) } ) )
36 35 iuneq1d ⊢ ( 𝑘 ∈ ℕ → ∪ 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹 ‘ 𝑛 ) = ∪ 𝑛 ∈ ( ( 1 ... 𝑘 ) ∪ { ( 𝑘 + 1 ) } ) ( 𝐹 ‘ 𝑛 ) )
37 iunxun ⊢ ∪ 𝑛 ∈ ( ( 1 ... 𝑘 ) ∪ { ( 𝑘 + 1 ) } ) ( 𝐹 ‘ 𝑛 ) = ( ∪ 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹 ‘ 𝑛 ) ∪ ∪ 𝑛 ∈ { ( 𝑘 + 1 ) } ( 𝐹 ‘ 𝑛 ) )
38 ovex ⊢ ( 𝑘 + 1 ) ∈ V
39 fveq2 ⊢ ( 𝑛 = ( 𝑘 + 1 ) → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
40 38 39 iunxsn ⊢ ∪ 𝑛 ∈ { ( 𝑘 + 1 ) } ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ ( 𝑘 + 1 ) )
41 40 uneq2i ⊢ ( ∪ 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹 ‘ 𝑛 ) ∪ ∪ 𝑛 ∈ { ( 𝑘 + 1 ) } ( 𝐹 ‘ 𝑛 ) ) = ( ∪ 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹 ‘ 𝑛 ) ∪ ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
42 37 41 eqtri ⊢ ∪ 𝑛 ∈ ( ( 1 ... 𝑘 ) ∪ { ( 𝑘 + 1 ) } ) ( 𝐹 ‘ 𝑛 ) = ( ∪ 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹 ‘ 𝑛 ) ∪ ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
43 36 42 eqtrdi ⊢ ( 𝑘 ∈ ℕ → ∪ 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹 ‘ 𝑛 ) = ( ∪ 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹 ‘ 𝑛 ) ∪ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) )
44 32 43 syl ⊢ ( ( ( 𝑘 ∈ ℕ ∧ 𝜑 ) ∧ ∪ 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑘 ) ) → ∪ 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹 ‘ 𝑛 ) = ( ∪ 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹 ‘ 𝑛 ) ∪ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) )
45 simpr ⊢ ( ( ( 𝑘 ∈ ℕ ∧ 𝜑 ) ∧ ∪ 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑘 ) ) → ∪ 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑘 ) )
46 45 uneq1d ⊢ ( ( ( 𝑘 ∈ ℕ ∧ 𝜑 ) ∧ ∪ 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑘 ) ) → ( ∪ 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹 ‘ 𝑛 ) ∪ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) = ( ( 𝐹 ‘ 𝑘 ) ∪ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) )
47 simplr ⊢ ( ( ( 𝑘 ∈ ℕ ∧ 𝜑 ) ∧ ∪ 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑘 ) ) → 𝜑 )
48 2 sbt ⊢ [ 𝑘 / 𝑛 ] ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
49 sbim ⊢ ( [ 𝑘 / 𝑛 ] ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ↔ ( [ 𝑘 / 𝑛 ] ( 𝜑 ∧ 𝑛 ∈ ℕ ) → [ 𝑘 / 𝑛 ] ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
50 sban ⊢ ( [ 𝑘 / 𝑛 ] ( 𝜑 ∧ 𝑛 ∈ ℕ ) ↔ ( [ 𝑘 / 𝑛 ] 𝜑 ∧ [ 𝑘 / 𝑛 ] 𝑛 ∈ ℕ ) )
51 sbv ⊢ ( [ 𝑘 / 𝑛 ] 𝜑 ↔ 𝜑 )
52 clelsb1 ⊢ ( [ 𝑘 / 𝑛 ] 𝑛 ∈ ℕ ↔ 𝑘 ∈ ℕ )
53 51 52 anbi12i ⊢ ( ( [ 𝑘 / 𝑛 ] 𝜑 ∧ [ 𝑘 / 𝑛 ] 𝑛 ∈ ℕ ) ↔ ( 𝜑 ∧ 𝑘 ∈ ℕ ) )
54 50 53 bitr2i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ↔ [ 𝑘 / 𝑛 ] ( 𝜑 ∧ 𝑛 ∈ ℕ ) )
55 sbsbc ⊢ ( [ 𝑘 / 𝑛 ] ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ↔ [ 𝑘 / 𝑛 ] ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
56 sbcssg ⊢ ( 𝑘 ∈ V → ( [ 𝑘 / 𝑛 ] ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ↔ ⦋ 𝑘 / 𝑛 ⦌ ( 𝐹 ‘ 𝑛 ) ⊆ ⦋ 𝑘 / 𝑛 ⦌ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
57 56 elv ⊢ ( [ 𝑘 / 𝑛 ] ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ↔ ⦋ 𝑘 / 𝑛 ⦌ ( 𝐹 ‘ 𝑛 ) ⊆ ⦋ 𝑘 / 𝑛 ⦌ ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
58 csbfv ⊢ ⦋ 𝑘 / 𝑛 ⦌ ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑘 )
59 csbfv2g ⊢ ( 𝑘 ∈ V → ⦋ 𝑘 / 𝑛 ⦌ ( 𝐹 ‘ ( 𝑛 + 1 ) ) = ( 𝐹 ‘ ⦋ 𝑘 / 𝑛 ⦌ ( 𝑛 + 1 ) ) )
60 59 elv ⊢ ⦋ 𝑘 / 𝑛 ⦌ ( 𝐹 ‘ ( 𝑛 + 1 ) ) = ( 𝐹 ‘ ⦋ 𝑘 / 𝑛 ⦌ ( 𝑛 + 1 ) )
61 csbov1g ⊢ ( 𝑘 ∈ V → ⦋ 𝑘 / 𝑛 ⦌ ( 𝑛 + 1 ) = ( ⦋ 𝑘 / 𝑛 ⦌ 𝑛 + 1 ) )
62 61 elv ⊢ ⦋ 𝑘 / 𝑛 ⦌ ( 𝑛 + 1 ) = ( ⦋ 𝑘 / 𝑛 ⦌ 𝑛 + 1 )
63 62 fveq2i ⊢ ( 𝐹 ‘ ⦋ 𝑘 / 𝑛 ⦌ ( 𝑛 + 1 ) ) = ( 𝐹 ‘ ( ⦋ 𝑘 / 𝑛 ⦌ 𝑛 + 1 ) )
64 vex ⊢ 𝑘 ∈ V
65 64 csbvargi ⊢ ⦋ 𝑘 / 𝑛 ⦌ 𝑛 = 𝑘
66 65 oveq1i ⊢ ( ⦋ 𝑘 / 𝑛 ⦌ 𝑛 + 1 ) = ( 𝑘 + 1 )
67 66 fveq2i ⊢ ( 𝐹 ‘ ( ⦋ 𝑘 / 𝑛 ⦌ 𝑛 + 1 ) ) = ( 𝐹 ‘ ( 𝑘 + 1 ) )
68 60 63 67 3eqtri ⊢ ⦋ 𝑘 / 𝑛 ⦌ ( 𝐹 ‘ ( 𝑛 + 1 ) ) = ( 𝐹 ‘ ( 𝑘 + 1 ) )
69 58 68 sseq12i ⊢ ( ⦋ 𝑘 / 𝑛 ⦌ ( 𝐹 ‘ 𝑛 ) ⊆ ⦋ 𝑘 / 𝑛 ⦌ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ↔ ( 𝐹 ‘ 𝑘 ) ⊆ ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
70 55 57 69 3bitrri ⊢ ( ( 𝐹 ‘ 𝑘 ) ⊆ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ↔ [ 𝑘 / 𝑛 ] ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
71 54 70 imbi12i ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) ⊆ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ↔ ( [ 𝑘 / 𝑛 ] ( 𝜑 ∧ 𝑛 ∈ ℕ ) → [ 𝑘 / 𝑛 ] ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
72 49 71 bitr4i ⊢ ( [ 𝑘 / 𝑛 ] ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ↔ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) ⊆ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) )
73 48 72 mpbi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) ⊆ ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
74 ssequn1 ⊢ ( ( 𝐹 ‘ 𝑘 ) ⊆ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ↔ ( ( 𝐹 ‘ 𝑘 ) ∪ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) = ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
75 73 74 sylib ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑘 ) ∪ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) = ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
76 47 32 75 syl2anc ⊢ ( ( ( 𝑘 ∈ ℕ ∧ 𝜑 ) ∧ ∪ 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑘 ) ) → ( ( 𝐹 ‘ 𝑘 ) ∪ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) = ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
77 44 46 76 3eqtrd ⊢ ( ( ( 𝑘 ∈ ℕ ∧ 𝜑 ) ∧ ∪ 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑘 ) ) → ∪ 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
78 77 exp31 ⊢ ( 𝑘 ∈ ℕ → ( 𝜑 → ( ∪ 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑘 ) → ∪ 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) )
79 78 a2d ⊢ ( 𝑘 ∈ ℕ → ( ( 𝜑 → ∪ 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑘 ) ) → ( 𝜑 → ∪ 𝑛 ∈ ( 1 ... ( 𝑘 + 1 ) ) ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) )
80 7 12 17 22 31 79 nnind ⊢ ( 𝑖 ∈ ℕ → ( 𝜑 → ∪ 𝑛 ∈ ( 1 ... 𝑖 ) ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑖 ) ) )
81 80 impcom ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ∪ 𝑛 ∈ ( 1 ... 𝑖 ) ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑖 ) )