# Metamath Proof Explorer

## Theorem fseq1p1m1

Description: Add/remove an item to/from the end of a finite sequence. (Contributed by Paul Chapman, 17-Nov-2012) (Revised by Mario Carneiro, 7-Mar-2014)

Ref Expression
Hypothesis fseq1p1m1.1 ${⊢}{H}=\left\{⟨{N}+1,{B}⟩\right\}$
Assertion fseq1p1m1 ${⊢}{N}\in {ℕ}_{0}\to \left(\left({F}:\left(1\dots {N}\right)⟶{A}\wedge {B}\in {A}\wedge {G}={F}\cup {H}\right)↔\left({G}:\left(1\dots {N}+1\right)⟶{A}\wedge {G}\left({N}+1\right)={B}\wedge {F}={{G}↾}_{\left(1\dots {N}\right)}\right)\right)$

### Proof

Step Hyp Ref Expression
1 fseq1p1m1.1 ${⊢}{H}=\left\{⟨{N}+1,{B}⟩\right\}$
2 simpr1 ${⊢}\left({N}\in {ℕ}_{0}\wedge \left({F}:\left(1\dots {N}\right)⟶{A}\wedge {B}\in {A}\wedge {G}={F}\cup {H}\right)\right)\to {F}:\left(1\dots {N}\right)⟶{A}$
3 nn0p1nn ${⊢}{N}\in {ℕ}_{0}\to {N}+1\in ℕ$
4 3 adantr ${⊢}\left({N}\in {ℕ}_{0}\wedge \left({F}:\left(1\dots {N}\right)⟶{A}\wedge {B}\in {A}\wedge {G}={F}\cup {H}\right)\right)\to {N}+1\in ℕ$
5 simpr2 ${⊢}\left({N}\in {ℕ}_{0}\wedge \left({F}:\left(1\dots {N}\right)⟶{A}\wedge {B}\in {A}\wedge {G}={F}\cup {H}\right)\right)\to {B}\in {A}$
6 fsng ${⊢}\left({N}+1\in ℕ\wedge {B}\in {A}\right)\to \left({H}:\left\{{N}+1\right\}⟶\left\{{B}\right\}↔{H}=\left\{⟨{N}+1,{B}⟩\right\}\right)$
7 1 6 mpbiri ${⊢}\left({N}+1\in ℕ\wedge {B}\in {A}\right)\to {H}:\left\{{N}+1\right\}⟶\left\{{B}\right\}$
8 4 5 7 syl2anc ${⊢}\left({N}\in {ℕ}_{0}\wedge \left({F}:\left(1\dots {N}\right)⟶{A}\wedge {B}\in {A}\wedge {G}={F}\cup {H}\right)\right)\to {H}:\left\{{N}+1\right\}⟶\left\{{B}\right\}$
9 5 snssd ${⊢}\left({N}\in {ℕ}_{0}\wedge \left({F}:\left(1\dots {N}\right)⟶{A}\wedge {B}\in {A}\wedge {G}={F}\cup {H}\right)\right)\to \left\{{B}\right\}\subseteq {A}$
10 8 9 fssd ${⊢}\left({N}\in {ℕ}_{0}\wedge \left({F}:\left(1\dots {N}\right)⟶{A}\wedge {B}\in {A}\wedge {G}={F}\cup {H}\right)\right)\to {H}:\left\{{N}+1\right\}⟶{A}$
11 fzp1disj ${⊢}\left(1\dots {N}\right)\cap \left\{{N}+1\right\}=\varnothing$
12 11 a1i ${⊢}\left({N}\in {ℕ}_{0}\wedge \left({F}:\left(1\dots {N}\right)⟶{A}\wedge {B}\in {A}\wedge {G}={F}\cup {H}\right)\right)\to \left(1\dots {N}\right)\cap \left\{{N}+1\right\}=\varnothing$
13 2 10 12 fun2d ${⊢}\left({N}\in {ℕ}_{0}\wedge \left({F}:\left(1\dots {N}\right)⟶{A}\wedge {B}\in {A}\wedge {G}={F}\cup {H}\right)\right)\to \left({F}\cup {H}\right):\left(1\dots {N}\right)\cup \left\{{N}+1\right\}⟶{A}$
14 1z ${⊢}1\in ℤ$
15 simpl ${⊢}\left({N}\in {ℕ}_{0}\wedge \left({F}:\left(1\dots {N}\right)⟶{A}\wedge {B}\in {A}\wedge {G}={F}\cup {H}\right)\right)\to {N}\in {ℕ}_{0}$
16 nn0uz ${⊢}{ℕ}_{0}={ℤ}_{\ge 0}$
17 1m1e0 ${⊢}1-1=0$
18 17 fveq2i ${⊢}{ℤ}_{\ge \left(1-1\right)}={ℤ}_{\ge 0}$
19 16 18 eqtr4i ${⊢}{ℕ}_{0}={ℤ}_{\ge \left(1-1\right)}$
20 15 19 eleqtrdi ${⊢}\left({N}\in {ℕ}_{0}\wedge \left({F}:\left(1\dots {N}\right)⟶{A}\wedge {B}\in {A}\wedge {G}={F}\cup {H}\right)\right)\to {N}\in {ℤ}_{\ge \left(1-1\right)}$
21 fzsuc2 ${⊢}\left(1\in ℤ\wedge {N}\in {ℤ}_{\ge \left(1-1\right)}\right)\to \left(1\dots {N}+1\right)=\left(1\dots {N}\right)\cup \left\{{N}+1\right\}$
22 14 20 21 sylancr ${⊢}\left({N}\in {ℕ}_{0}\wedge \left({F}:\left(1\dots {N}\right)⟶{A}\wedge {B}\in {A}\wedge {G}={F}\cup {H}\right)\right)\to \left(1\dots {N}+1\right)=\left(1\dots {N}\right)\cup \left\{{N}+1\right\}$
23 22 eqcomd ${⊢}\left({N}\in {ℕ}_{0}\wedge \left({F}:\left(1\dots {N}\right)⟶{A}\wedge {B}\in {A}\wedge {G}={F}\cup {H}\right)\right)\to \left(1\dots {N}\right)\cup \left\{{N}+1\right\}=\left(1\dots {N}+1\right)$
24 23 feq2d ${⊢}\left({N}\in {ℕ}_{0}\wedge \left({F}:\left(1\dots {N}\right)⟶{A}\wedge {B}\in {A}\wedge {G}={F}\cup {H}\right)\right)\to \left(\left({F}\cup {H}\right):\left(1\dots {N}\right)\cup \left\{{N}+1\right\}⟶{A}↔\left({F}\cup {H}\right):\left(1\dots {N}+1\right)⟶{A}\right)$
25 13 24 mpbid ${⊢}\left({N}\in {ℕ}_{0}\wedge \left({F}:\left(1\dots {N}\right)⟶{A}\wedge {B}\in {A}\wedge {G}={F}\cup {H}\right)\right)\to \left({F}\cup {H}\right):\left(1\dots {N}+1\right)⟶{A}$
26 simpr3 ${⊢}\left({N}\in {ℕ}_{0}\wedge \left({F}:\left(1\dots {N}\right)⟶{A}\wedge {B}\in {A}\wedge {G}={F}\cup {H}\right)\right)\to {G}={F}\cup {H}$
27 26 feq1d ${⊢}\left({N}\in {ℕ}_{0}\wedge \left({F}:\left(1\dots {N}\right)⟶{A}\wedge {B}\in {A}\wedge {G}={F}\cup {H}\right)\right)\to \left({G}:\left(1\dots {N}+1\right)⟶{A}↔\left({F}\cup {H}\right):\left(1\dots {N}+1\right)⟶{A}\right)$
28 25 27 mpbird ${⊢}\left({N}\in {ℕ}_{0}\wedge \left({F}:\left(1\dots {N}\right)⟶{A}\wedge {B}\in {A}\wedge {G}={F}\cup {H}\right)\right)\to {G}:\left(1\dots {N}+1\right)⟶{A}$
29 ovex ${⊢}{N}+1\in \mathrm{V}$
30 29 snid ${⊢}{N}+1\in \left\{{N}+1\right\}$
31 fvres ${⊢}{N}+1\in \left\{{N}+1\right\}\to \left({{G}↾}_{\left\{{N}+1\right\}}\right)\left({N}+1\right)={G}\left({N}+1\right)$
32 30 31 ax-mp ${⊢}\left({{G}↾}_{\left\{{N}+1\right\}}\right)\left({N}+1\right)={G}\left({N}+1\right)$
33 26 reseq1d ${⊢}\left({N}\in {ℕ}_{0}\wedge \left({F}:\left(1\dots {N}\right)⟶{A}\wedge {B}\in {A}\wedge {G}={F}\cup {H}\right)\right)\to {{G}↾}_{\left\{{N}+1\right\}}={\left({F}\cup {H}\right)↾}_{\left\{{N}+1\right\}}$
34 ffn ${⊢}{F}:\left(1\dots {N}\right)⟶{A}\to {F}Fn\left(1\dots {N}\right)$
35 fnresdisj ${⊢}{F}Fn\left(1\dots {N}\right)\to \left(\left(1\dots {N}\right)\cap \left\{{N}+1\right\}=\varnothing ↔{{F}↾}_{\left\{{N}+1\right\}}=\varnothing \right)$
36 2 34 35 3syl ${⊢}\left({N}\in {ℕ}_{0}\wedge \left({F}:\left(1\dots {N}\right)⟶{A}\wedge {B}\in {A}\wedge {G}={F}\cup {H}\right)\right)\to \left(\left(1\dots {N}\right)\cap \left\{{N}+1\right\}=\varnothing ↔{{F}↾}_{\left\{{N}+1\right\}}=\varnothing \right)$
37 12 36 mpbid ${⊢}\left({N}\in {ℕ}_{0}\wedge \left({F}:\left(1\dots {N}\right)⟶{A}\wedge {B}\in {A}\wedge {G}={F}\cup {H}\right)\right)\to {{F}↾}_{\left\{{N}+1\right\}}=\varnothing$
38 37 uneq1d ${⊢}\left({N}\in {ℕ}_{0}\wedge \left({F}:\left(1\dots {N}\right)⟶{A}\wedge {B}\in {A}\wedge {G}={F}\cup {H}\right)\right)\to \left({{F}↾}_{\left\{{N}+1\right\}}\right)\cup \left({{H}↾}_{\left\{{N}+1\right\}}\right)=\varnothing \cup \left({{H}↾}_{\left\{{N}+1\right\}}\right)$
39 resundir ${⊢}{\left({F}\cup {H}\right)↾}_{\left\{{N}+1\right\}}=\left({{F}↾}_{\left\{{N}+1\right\}}\right)\cup \left({{H}↾}_{\left\{{N}+1\right\}}\right)$
40 uncom ${⊢}\varnothing \cup \left({{H}↾}_{\left\{{N}+1\right\}}\right)=\left({{H}↾}_{\left\{{N}+1\right\}}\right)\cup \varnothing$
41 un0 ${⊢}\left({{H}↾}_{\left\{{N}+1\right\}}\right)\cup \varnothing ={{H}↾}_{\left\{{N}+1\right\}}$
42 40 41 eqtr2i ${⊢}{{H}↾}_{\left\{{N}+1\right\}}=\varnothing \cup \left({{H}↾}_{\left\{{N}+1\right\}}\right)$
43 38 39 42 3eqtr4g ${⊢}\left({N}\in {ℕ}_{0}\wedge \left({F}:\left(1\dots {N}\right)⟶{A}\wedge {B}\in {A}\wedge {G}={F}\cup {H}\right)\right)\to {\left({F}\cup {H}\right)↾}_{\left\{{N}+1\right\}}={{H}↾}_{\left\{{N}+1\right\}}$
44 ffn ${⊢}{H}:\left\{{N}+1\right\}⟶{A}\to {H}Fn\left\{{N}+1\right\}$
45 fnresdm ${⊢}{H}Fn\left\{{N}+1\right\}\to {{H}↾}_{\left\{{N}+1\right\}}={H}$
46 10 44 45 3syl ${⊢}\left({N}\in {ℕ}_{0}\wedge \left({F}:\left(1\dots {N}\right)⟶{A}\wedge {B}\in {A}\wedge {G}={F}\cup {H}\right)\right)\to {{H}↾}_{\left\{{N}+1\right\}}={H}$
47 33 43 46 3eqtrd ${⊢}\left({N}\in {ℕ}_{0}\wedge \left({F}:\left(1\dots {N}\right)⟶{A}\wedge {B}\in {A}\wedge {G}={F}\cup {H}\right)\right)\to {{G}↾}_{\left\{{N}+1\right\}}={H}$
48 47 fveq1d ${⊢}\left({N}\in {ℕ}_{0}\wedge \left({F}:\left(1\dots {N}\right)⟶{A}\wedge {B}\in {A}\wedge {G}={F}\cup {H}\right)\right)\to \left({{G}↾}_{\left\{{N}+1\right\}}\right)\left({N}+1\right)={H}\left({N}+1\right)$
49 1 fveq1i ${⊢}{H}\left({N}+1\right)=\left\{⟨{N}+1,{B}⟩\right\}\left({N}+1\right)$
50 fvsng ${⊢}\left({N}+1\in ℕ\wedge {B}\in {A}\right)\to \left\{⟨{N}+1,{B}⟩\right\}\left({N}+1\right)={B}$
51 49 50 syl5eq ${⊢}\left({N}+1\in ℕ\wedge {B}\in {A}\right)\to {H}\left({N}+1\right)={B}$
52 4 5 51 syl2anc ${⊢}\left({N}\in {ℕ}_{0}\wedge \left({F}:\left(1\dots {N}\right)⟶{A}\wedge {B}\in {A}\wedge {G}={F}\cup {H}\right)\right)\to {H}\left({N}+1\right)={B}$
53 48 52 eqtrd ${⊢}\left({N}\in {ℕ}_{0}\wedge \left({F}:\left(1\dots {N}\right)⟶{A}\wedge {B}\in {A}\wedge {G}={F}\cup {H}\right)\right)\to \left({{G}↾}_{\left\{{N}+1\right\}}\right)\left({N}+1\right)={B}$
54 32 53 syl5eqr ${⊢}\left({N}\in {ℕ}_{0}\wedge \left({F}:\left(1\dots {N}\right)⟶{A}\wedge {B}\in {A}\wedge {G}={F}\cup {H}\right)\right)\to {G}\left({N}+1\right)={B}$
55 26 reseq1d ${⊢}\left({N}\in {ℕ}_{0}\wedge \left({F}:\left(1\dots {N}\right)⟶{A}\wedge {B}\in {A}\wedge {G}={F}\cup {H}\right)\right)\to {{G}↾}_{\left(1\dots {N}\right)}={\left({F}\cup {H}\right)↾}_{\left(1\dots {N}\right)}$
56 incom ${⊢}\left\{{N}+1\right\}\cap \left(1\dots {N}\right)=\left(1\dots {N}\right)\cap \left\{{N}+1\right\}$
57 56 12 syl5eq ${⊢}\left({N}\in {ℕ}_{0}\wedge \left({F}:\left(1\dots {N}\right)⟶{A}\wedge {B}\in {A}\wedge {G}={F}\cup {H}\right)\right)\to \left\{{N}+1\right\}\cap \left(1\dots {N}\right)=\varnothing$
58 ffn ${⊢}{H}:\left\{{N}+1\right\}⟶\left\{{B}\right\}\to {H}Fn\left\{{N}+1\right\}$
59 fnresdisj ${⊢}{H}Fn\left\{{N}+1\right\}\to \left(\left\{{N}+1\right\}\cap \left(1\dots {N}\right)=\varnothing ↔{{H}↾}_{\left(1\dots {N}\right)}=\varnothing \right)$
60 8 58 59 3syl ${⊢}\left({N}\in {ℕ}_{0}\wedge \left({F}:\left(1\dots {N}\right)⟶{A}\wedge {B}\in {A}\wedge {G}={F}\cup {H}\right)\right)\to \left(\left\{{N}+1\right\}\cap \left(1\dots {N}\right)=\varnothing ↔{{H}↾}_{\left(1\dots {N}\right)}=\varnothing \right)$
61 57 60 mpbid ${⊢}\left({N}\in {ℕ}_{0}\wedge \left({F}:\left(1\dots {N}\right)⟶{A}\wedge {B}\in {A}\wedge {G}={F}\cup {H}\right)\right)\to {{H}↾}_{\left(1\dots {N}\right)}=\varnothing$
62 61 uneq2d ${⊢}\left({N}\in {ℕ}_{0}\wedge \left({F}:\left(1\dots {N}\right)⟶{A}\wedge {B}\in {A}\wedge {G}={F}\cup {H}\right)\right)\to \left({{F}↾}_{\left(1\dots {N}\right)}\right)\cup \left({{H}↾}_{\left(1\dots {N}\right)}\right)=\left({{F}↾}_{\left(1\dots {N}\right)}\right)\cup \varnothing$
63 resundir ${⊢}{\left({F}\cup {H}\right)↾}_{\left(1\dots {N}\right)}=\left({{F}↾}_{\left(1\dots {N}\right)}\right)\cup \left({{H}↾}_{\left(1\dots {N}\right)}\right)$
64 un0 ${⊢}\left({{F}↾}_{\left(1\dots {N}\right)}\right)\cup \varnothing ={{F}↾}_{\left(1\dots {N}\right)}$
65 64 eqcomi ${⊢}{{F}↾}_{\left(1\dots {N}\right)}=\left({{F}↾}_{\left(1\dots {N}\right)}\right)\cup \varnothing$
66 62 63 65 3eqtr4g ${⊢}\left({N}\in {ℕ}_{0}\wedge \left({F}:\left(1\dots {N}\right)⟶{A}\wedge {B}\in {A}\wedge {G}={F}\cup {H}\right)\right)\to {\left({F}\cup {H}\right)↾}_{\left(1\dots {N}\right)}={{F}↾}_{\left(1\dots {N}\right)}$
67 fnresdm ${⊢}{F}Fn\left(1\dots {N}\right)\to {{F}↾}_{\left(1\dots {N}\right)}={F}$
68 2 34 67 3syl ${⊢}\left({N}\in {ℕ}_{0}\wedge \left({F}:\left(1\dots {N}\right)⟶{A}\wedge {B}\in {A}\wedge {G}={F}\cup {H}\right)\right)\to {{F}↾}_{\left(1\dots {N}\right)}={F}$
69 55 66 68 3eqtrrd ${⊢}\left({N}\in {ℕ}_{0}\wedge \left({F}:\left(1\dots {N}\right)⟶{A}\wedge {B}\in {A}\wedge {G}={F}\cup {H}\right)\right)\to {F}={{G}↾}_{\left(1\dots {N}\right)}$
70 28 54 69 3jca ${⊢}\left({N}\in {ℕ}_{0}\wedge \left({F}:\left(1\dots {N}\right)⟶{A}\wedge {B}\in {A}\wedge {G}={F}\cup {H}\right)\right)\to \left({G}:\left(1\dots {N}+1\right)⟶{A}\wedge {G}\left({N}+1\right)={B}\wedge {F}={{G}↾}_{\left(1\dots {N}\right)}\right)$
71 simpr1 ${⊢}\left({N}\in {ℕ}_{0}\wedge \left({G}:\left(1\dots {N}+1\right)⟶{A}\wedge {G}\left({N}+1\right)={B}\wedge {F}={{G}↾}_{\left(1\dots {N}\right)}\right)\right)\to {G}:\left(1\dots {N}+1\right)⟶{A}$
72 fzssp1 ${⊢}\left(1\dots {N}\right)\subseteq \left(1\dots {N}+1\right)$
73 fssres ${⊢}\left({G}:\left(1\dots {N}+1\right)⟶{A}\wedge \left(1\dots {N}\right)\subseteq \left(1\dots {N}+1\right)\right)\to \left({{G}↾}_{\left(1\dots {N}\right)}\right):\left(1\dots {N}\right)⟶{A}$
74 71 72 73 sylancl ${⊢}\left({N}\in {ℕ}_{0}\wedge \left({G}:\left(1\dots {N}+1\right)⟶{A}\wedge {G}\left({N}+1\right)={B}\wedge {F}={{G}↾}_{\left(1\dots {N}\right)}\right)\right)\to \left({{G}↾}_{\left(1\dots {N}\right)}\right):\left(1\dots {N}\right)⟶{A}$
75 simpr3 ${⊢}\left({N}\in {ℕ}_{0}\wedge \left({G}:\left(1\dots {N}+1\right)⟶{A}\wedge {G}\left({N}+1\right)={B}\wedge {F}={{G}↾}_{\left(1\dots {N}\right)}\right)\right)\to {F}={{G}↾}_{\left(1\dots {N}\right)}$
76 75 feq1d ${⊢}\left({N}\in {ℕ}_{0}\wedge \left({G}:\left(1\dots {N}+1\right)⟶{A}\wedge {G}\left({N}+1\right)={B}\wedge {F}={{G}↾}_{\left(1\dots {N}\right)}\right)\right)\to \left({F}:\left(1\dots {N}\right)⟶{A}↔\left({{G}↾}_{\left(1\dots {N}\right)}\right):\left(1\dots {N}\right)⟶{A}\right)$
77 74 76 mpbird ${⊢}\left({N}\in {ℕ}_{0}\wedge \left({G}:\left(1\dots {N}+1\right)⟶{A}\wedge {G}\left({N}+1\right)={B}\wedge {F}={{G}↾}_{\left(1\dots {N}\right)}\right)\right)\to {F}:\left(1\dots {N}\right)⟶{A}$
78 simpr2 ${⊢}\left({N}\in {ℕ}_{0}\wedge \left({G}:\left(1\dots {N}+1\right)⟶{A}\wedge {G}\left({N}+1\right)={B}\wedge {F}={{G}↾}_{\left(1\dots {N}\right)}\right)\right)\to {G}\left({N}+1\right)={B}$
79 3 adantr ${⊢}\left({N}\in {ℕ}_{0}\wedge \left({G}:\left(1\dots {N}+1\right)⟶{A}\wedge {G}\left({N}+1\right)={B}\wedge {F}={{G}↾}_{\left(1\dots {N}\right)}\right)\right)\to {N}+1\in ℕ$
80 nnuz ${⊢}ℕ={ℤ}_{\ge 1}$
81 79 80 eleqtrdi ${⊢}\left({N}\in {ℕ}_{0}\wedge \left({G}:\left(1\dots {N}+1\right)⟶{A}\wedge {G}\left({N}+1\right)={B}\wedge {F}={{G}↾}_{\left(1\dots {N}\right)}\right)\right)\to {N}+1\in {ℤ}_{\ge 1}$
82 eluzfz2 ${⊢}{N}+1\in {ℤ}_{\ge 1}\to {N}+1\in \left(1\dots {N}+1\right)$
83 81 82 syl ${⊢}\left({N}\in {ℕ}_{0}\wedge \left({G}:\left(1\dots {N}+1\right)⟶{A}\wedge {G}\left({N}+1\right)={B}\wedge {F}={{G}↾}_{\left(1\dots {N}\right)}\right)\right)\to {N}+1\in \left(1\dots {N}+1\right)$
84 71 83 ffvelrnd ${⊢}\left({N}\in {ℕ}_{0}\wedge \left({G}:\left(1\dots {N}+1\right)⟶{A}\wedge {G}\left({N}+1\right)={B}\wedge {F}={{G}↾}_{\left(1\dots {N}\right)}\right)\right)\to {G}\left({N}+1\right)\in {A}$
85 78 84 eqeltrrd ${⊢}\left({N}\in {ℕ}_{0}\wedge \left({G}:\left(1\dots {N}+1\right)⟶{A}\wedge {G}\left({N}+1\right)={B}\wedge {F}={{G}↾}_{\left(1\dots {N}\right)}\right)\right)\to {B}\in {A}$
86 ffn ${⊢}{G}:\left(1\dots {N}+1\right)⟶{A}\to {G}Fn\left(1\dots {N}+1\right)$
87 71 86 syl ${⊢}\left({N}\in {ℕ}_{0}\wedge \left({G}:\left(1\dots {N}+1\right)⟶{A}\wedge {G}\left({N}+1\right)={B}\wedge {F}={{G}↾}_{\left(1\dots {N}\right)}\right)\right)\to {G}Fn\left(1\dots {N}+1\right)$
88 fnressn ${⊢}\left({G}Fn\left(1\dots {N}+1\right)\wedge {N}+1\in \left(1\dots {N}+1\right)\right)\to {{G}↾}_{\left\{{N}+1\right\}}=\left\{⟨{N}+1,{G}\left({N}+1\right)⟩\right\}$
89 87 83 88 syl2anc ${⊢}\left({N}\in {ℕ}_{0}\wedge \left({G}:\left(1\dots {N}+1\right)⟶{A}\wedge {G}\left({N}+1\right)={B}\wedge {F}={{G}↾}_{\left(1\dots {N}\right)}\right)\right)\to {{G}↾}_{\left\{{N}+1\right\}}=\left\{⟨{N}+1,{G}\left({N}+1\right)⟩\right\}$
90 opeq2 ${⊢}{G}\left({N}+1\right)={B}\to ⟨{N}+1,{G}\left({N}+1\right)⟩=⟨{N}+1,{B}⟩$
91 90 sneqd ${⊢}{G}\left({N}+1\right)={B}\to \left\{⟨{N}+1,{G}\left({N}+1\right)⟩\right\}=\left\{⟨{N}+1,{B}⟩\right\}$
92 78 91 syl ${⊢}\left({N}\in {ℕ}_{0}\wedge \left({G}:\left(1\dots {N}+1\right)⟶{A}\wedge {G}\left({N}+1\right)={B}\wedge {F}={{G}↾}_{\left(1\dots {N}\right)}\right)\right)\to \left\{⟨{N}+1,{G}\left({N}+1\right)⟩\right\}=\left\{⟨{N}+1,{B}⟩\right\}$
93 89 92 eqtrd ${⊢}\left({N}\in {ℕ}_{0}\wedge \left({G}:\left(1\dots {N}+1\right)⟶{A}\wedge {G}\left({N}+1\right)={B}\wedge {F}={{G}↾}_{\left(1\dots {N}\right)}\right)\right)\to {{G}↾}_{\left\{{N}+1\right\}}=\left\{⟨{N}+1,{B}⟩\right\}$
94 93 1 syl6reqr ${⊢}\left({N}\in {ℕ}_{0}\wedge \left({G}:\left(1\dots {N}+1\right)⟶{A}\wedge {G}\left({N}+1\right)={B}\wedge {F}={{G}↾}_{\left(1\dots {N}\right)}\right)\right)\to {H}={{G}↾}_{\left\{{N}+1\right\}}$
95 75 94 uneq12d ${⊢}\left({N}\in {ℕ}_{0}\wedge \left({G}:\left(1\dots {N}+1\right)⟶{A}\wedge {G}\left({N}+1\right)={B}\wedge {F}={{G}↾}_{\left(1\dots {N}\right)}\right)\right)\to {F}\cup {H}=\left({{G}↾}_{\left(1\dots {N}\right)}\right)\cup \left({{G}↾}_{\left\{{N}+1\right\}}\right)$
96 simpl ${⊢}\left({N}\in {ℕ}_{0}\wedge \left({G}:\left(1\dots {N}+1\right)⟶{A}\wedge {G}\left({N}+1\right)={B}\wedge {F}={{G}↾}_{\left(1\dots {N}\right)}\right)\right)\to {N}\in {ℕ}_{0}$
97 96 19 eleqtrdi ${⊢}\left({N}\in {ℕ}_{0}\wedge \left({G}:\left(1\dots {N}+1\right)⟶{A}\wedge {G}\left({N}+1\right)={B}\wedge {F}={{G}↾}_{\left(1\dots {N}\right)}\right)\right)\to {N}\in {ℤ}_{\ge \left(1-1\right)}$
98 14 97 21 sylancr ${⊢}\left({N}\in {ℕ}_{0}\wedge \left({G}:\left(1\dots {N}+1\right)⟶{A}\wedge {G}\left({N}+1\right)={B}\wedge {F}={{G}↾}_{\left(1\dots {N}\right)}\right)\right)\to \left(1\dots {N}+1\right)=\left(1\dots {N}\right)\cup \left\{{N}+1\right\}$
99 98 reseq2d ${⊢}\left({N}\in {ℕ}_{0}\wedge \left({G}:\left(1\dots {N}+1\right)⟶{A}\wedge {G}\left({N}+1\right)={B}\wedge {F}={{G}↾}_{\left(1\dots {N}\right)}\right)\right)\to {{G}↾}_{\left(1\dots {N}+1\right)}={{G}↾}_{\left(\left(1\dots {N}\right)\cup \left\{{N}+1\right\}\right)}$
100 resundi ${⊢}{{G}↾}_{\left(\left(1\dots {N}\right)\cup \left\{{N}+1\right\}\right)}=\left({{G}↾}_{\left(1\dots {N}\right)}\right)\cup \left({{G}↾}_{\left\{{N}+1\right\}}\right)$
101 99 100 syl6req ${⊢}\left({N}\in {ℕ}_{0}\wedge \left({G}:\left(1\dots {N}+1\right)⟶{A}\wedge {G}\left({N}+1\right)={B}\wedge {F}={{G}↾}_{\left(1\dots {N}\right)}\right)\right)\to \left({{G}↾}_{\left(1\dots {N}\right)}\right)\cup \left({{G}↾}_{\left\{{N}+1\right\}}\right)={{G}↾}_{\left(1\dots {N}+1\right)}$
102 fnresdm ${⊢}{G}Fn\left(1\dots {N}+1\right)\to {{G}↾}_{\left(1\dots {N}+1\right)}={G}$
103 71 86 102 3syl ${⊢}\left({N}\in {ℕ}_{0}\wedge \left({G}:\left(1\dots {N}+1\right)⟶{A}\wedge {G}\left({N}+1\right)={B}\wedge {F}={{G}↾}_{\left(1\dots {N}\right)}\right)\right)\to {{G}↾}_{\left(1\dots {N}+1\right)}={G}$
104 95 101 103 3eqtrrd ${⊢}\left({N}\in {ℕ}_{0}\wedge \left({G}:\left(1\dots {N}+1\right)⟶{A}\wedge {G}\left({N}+1\right)={B}\wedge {F}={{G}↾}_{\left(1\dots {N}\right)}\right)\right)\to {G}={F}\cup {H}$
105 77 85 104 3jca ${⊢}\left({N}\in {ℕ}_{0}\wedge \left({G}:\left(1\dots {N}+1\right)⟶{A}\wedge {G}\left({N}+1\right)={B}\wedge {F}={{G}↾}_{\left(1\dots {N}\right)}\right)\right)\to \left({F}:\left(1\dots {N}\right)⟶{A}\wedge {B}\in {A}\wedge {G}={F}\cup {H}\right)$
106 70 105 impbida ${⊢}{N}\in {ℕ}_{0}\to \left(\left({F}:\left(1\dots {N}\right)⟶{A}\wedge {B}\in {A}\wedge {G}={F}\cup {H}\right)↔\left({G}:\left(1\dots {N}+1\right)⟶{A}\wedge {G}\left({N}+1\right)={B}\wedge {F}={{G}↾}_{\left(1\dots {N}\right)}\right)\right)$