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 ⊢ 𝐻 = { ⟨ ( 𝑁 + 1 ) , 𝐵 ⟩ }
Assertion fseq1p1m1 ( 𝑁 ∈ ℕ0 → ( ( 𝐹 : ( 1 ... 𝑁 ) ⟶ 𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐺 = ( 𝐹 ∪ 𝐻 ) ) ↔ ( 𝐺 : ( 1 ... ( 𝑁 + 1 ) ) ⟶ 𝐴 ∧ ( 𝐺 ‘ ( 𝑁 + 1 ) ) = 𝐵 ∧ 𝐹 = ( 𝐺 ↾ ( 1 ... 𝑁 ) ) ) ) )

Proof

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