fseq1m1p1 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > fseq1m1p1		Structured version Visualization version GIF version

Theorem fseq1m1p1 12399

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

**Hypothesis**
Ref	Expression
fseq1m1p1.1	⊢ 𝐻 = {⟨𝑁, 𝐵⟩}

**Assertion**
Ref	Expression
fseq1m1p1	⊢ (𝑁 ∈ ℕ → ((𝐹:(1...(𝑁 − 1))⟶𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐺 = (𝐹 ∪ 𝐻)) ↔ (𝐺:(1...𝑁)⟶𝐴 ∧ (𝐺‘𝑁) = 𝐵 ∧ 𝐹 = (𝐺 ↾ (1...(𝑁 − 1))))))

**Proof of Theorem fseq1m1p1**
Step	Hyp	Ref	Expression
1		nnm1nn0 11319	. . 3 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ₀)
2		eqid 2620	. . . 4 ⊢ {⟨((𝑁 − 1) + 1), 𝐵⟩} = {⟨((𝑁 − 1) + 1), 𝐵⟩}
3	2	fseq1p1m1 12398	. . 3 ⊢ ((𝑁 − 1) ∈ ℕ₀ → ((𝐹:(1...(𝑁 − 1))⟶𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐺 = (𝐹 ∪ {⟨((𝑁 − 1) + 1), 𝐵⟩})) ↔ (𝐺:(1...((𝑁 − 1) + 1))⟶𝐴 ∧ (𝐺‘((𝑁 − 1) + 1)) = 𝐵 ∧ 𝐹 = (𝐺 ↾ (1...(𝑁 − 1))))))
4	1, 3	syl 17	. 2 ⊢ (𝑁 ∈ ℕ → ((𝐹:(1...(𝑁 − 1))⟶𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐺 = (𝐹 ∪ {⟨((𝑁 − 1) + 1), 𝐵⟩})) ↔ (𝐺:(1...((𝑁 − 1) + 1))⟶𝐴 ∧ (𝐺‘((𝑁 − 1) + 1)) = 𝐵 ∧ 𝐹 = (𝐺 ↾ (1...(𝑁 − 1))))))
5		nncn 11013	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
6		ax-1cn 9979	. . . . . . . . 9 ⊢ 1 ∈ ℂ
7		npcan 10275	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑁 − 1) + 1) = 𝑁)
8	5, 6, 7	sylancl 693	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → ((𝑁 − 1) + 1) = 𝑁)
9	8	opeq1d 4399	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → ⟨((𝑁 − 1) + 1), 𝐵⟩ = ⟨𝑁, 𝐵⟩)
10	9	sneqd 4180	. . . . . 6 ⊢ (𝑁 ∈ ℕ → {⟨((𝑁 − 1) + 1), 𝐵⟩} = {⟨𝑁, 𝐵⟩})
11		fseq1m1p1.1	. . . . . 6 ⊢ 𝐻 = {⟨𝑁, 𝐵⟩}
12	10, 11	syl6eqr 2672	. . . . 5 ⊢ (𝑁 ∈ ℕ → {⟨((𝑁 − 1) + 1), 𝐵⟩} = 𝐻)
13	12	uneq2d 3759	. . . 4 ⊢ (𝑁 ∈ ℕ → (𝐹 ∪ {⟨((𝑁 − 1) + 1), 𝐵⟩}) = (𝐹 ∪ 𝐻))
14	13	eqeq2d 2630	. . 3 ⊢ (𝑁 ∈ ℕ → (𝐺 = (𝐹 ∪ {⟨((𝑁 − 1) + 1), 𝐵⟩}) ↔ 𝐺 = (𝐹 ∪ 𝐻)))
15	14	3anbi3d 1403	. 2 ⊢ (𝑁 ∈ ℕ → ((𝐹:(1...(𝑁 − 1))⟶𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐺 = (𝐹 ∪ {⟨((𝑁 − 1) + 1), 𝐵⟩})) ↔ (𝐹:(1...(𝑁 − 1))⟶𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐺 = (𝐹 ∪ 𝐻))))
16	8	oveq2d 6651	. . . 4 ⊢ (𝑁 ∈ ℕ → (1...((𝑁 − 1) + 1)) = (1...𝑁))
17	16	feq2d 6018	. . 3 ⊢ (𝑁 ∈ ℕ → (𝐺:(1...((𝑁 − 1) + 1))⟶𝐴 ↔ 𝐺:(1...𝑁)⟶𝐴))
18	8	fveq2d 6182	. . . 4 ⊢ (𝑁 ∈ ℕ → (𝐺‘((𝑁 − 1) + 1)) = (𝐺‘𝑁))
19	18	eqeq1d 2622	. . 3 ⊢ (𝑁 ∈ ℕ → ((𝐺‘((𝑁 − 1) + 1)) = 𝐵 ↔ (𝐺‘𝑁) = 𝐵))
20	17, 19	3anbi12d 1398	. 2 ⊢ (𝑁 ∈ ℕ → ((𝐺:(1...((𝑁 − 1) + 1))⟶𝐴 ∧ (𝐺‘((𝑁 − 1) + 1)) = 𝐵 ∧ 𝐹 = (𝐺 ↾ (1...(𝑁 − 1)))) ↔ (𝐺:(1...𝑁)⟶𝐴 ∧ (𝐺‘𝑁) = 𝐵 ∧ 𝐹 = (𝐺 ↾ (1...(𝑁 − 1))))))
21	4, 15, 20	3bitr3d 298	1 ⊢ (𝑁 ∈ ℕ → ((𝐹:(1...(𝑁 − 1))⟶𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐺 = (𝐹 ∪ 𝐻)) ↔ (𝐺:(1...𝑁)⟶𝐴 ∧ (𝐺‘𝑁) = 𝐵 ∧ 𝐹 = (𝐺 ↾ (1...(𝑁 − 1))))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 196 ∧ w3a 1036 = wceq 1481 ∈ wcel 1988 ∪ cun 3565 {csn 4168 ⟨cop 4174 ↾ cres 5106 ⟶wf 5872 ‘cfv 5876 (class class class)co 6635 ℂcc 9919 1c1 9922 + caddc 9924 − cmin 10251 ℕcn 11005 ℕ₀cn0 11277 ...cfz 12311

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1720 ax-4 1735 ax-5 1837 ax-6 1886 ax-7 1933 ax-8 1990 ax-9 1997 ax-10 2017 ax-11 2032 ax-12 2045 ax-13 2244 ax-ext 2600 ax-sep 4772 ax-nul 4780 ax-pow 4834 ax-pr 4897 ax-un 6934 ax-cnex 9977 ax-resscn 9978 ax-1cn 9979 ax-icn 9980 ax-addcl 9981 ax-addrcl 9982 ax-mulcl 9983 ax-mulrcl 9984 ax-mulcom 9985 ax-addass 9986 ax-mulass 9987 ax-distr 9988 ax-i2m1 9989 ax-1ne0 9990 ax-1rid 9991 ax-rnegex 9992 ax-rrecex 9993 ax-cnre 9994 ax-pre-lttri 9995 ax-pre-lttrn 9996 ax-pre-ltadd 9997 ax-pre-mulgt0 9998

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1037 df-3an 1038 df-tru 1484 df-ex 1703 df-nf 1708 df-sb 1879 df-eu 2472 df-mo 2473 df-clab 2607 df-cleq 2613 df-clel 2616 df-nfc 2751 df-ne 2792 df-nel 2895 df-ral 2914 df-rex 2915 df-reu 2916 df-rab 2918 df-v 3197 df-sbc 3430 df-csb 3527 df-dif 3570 df-un 3572 df-in 3574 df-ss 3581 df-pss 3583 df-nul 3908 df-if 4078 df-pw 4151 df-sn 4169 df-pr 4171 df-tp 4173 df-op 4175 df-uni 4428 df-iun 4513 df-br 4645 df-opab 4704 df-mpt 4721 df-tr 4744 df-id 5014 df-eprel 5019 df-po 5025 df-so 5026 df-fr 5063 df-we 5065 df-xp 5110 df-rel 5111 df-cnv 5112 df-co 5113 df-dm 5114 df-rn 5115 df-res 5116 df-ima 5117 df-pred 5668 df-ord 5714 df-on 5715 df-lim 5716 df-suc 5717 df-iota 5839 df-fun 5878 df-fn 5879 df-f 5880 df-f1 5881 df-fo 5882 df-f1o 5883 df-fv 5884 df-riota 6596 df-ov 6638 df-oprab 6639 df-mpt2 6640 df-om 7051 df-1st 7153 df-2nd 7154 df-wrecs 7392 df-recs 7453 df-rdg 7491 df-er 7727 df-en 7941 df-dom 7942 df-sdom 7943 df-pnf 10061 df-mnf 10062 df-xr 10063 df-ltxr 10064 df-le 10065 df-sub 10253 df-neg 10254 df-nn 11006 df-n0 11278 df-z 11363 df-uz 11673 df-fz 12312

This theorem is referenced by: (None)

W3C validator