Theorem fzprval

Description: Two ways of defining the first two values of a sequence on NN . (Contributed by NM, 5-Sep-2011)

	Ref	Expression
Assertion	fzprval	$$⊢\forall x\in \left(1\dots 2\right)F\left(x\right)=if\left(x=1,A,B\right)\leftrightarrow \left(F\left(1\right)=A\wedge F\left(2\right)=B\right)$$

Proof

Step	Hyp	Ref	Expression
1		fz12pr	$$⊢\left(1\dots 2\right)=\left\{1,2\right\}$$
2	1	raleqi	$$⊢\forall x\in \left(1\dots 2\right)F\left(x\right)=if\left(x=1,A,B\right)\leftrightarrow \forall x\in \left\{1,2\right\}F\left(x\right)=if\left(x=1,A,B\right)$$
3		1ex	$$⊢1\in \mathrm{V}$$
4		2ex	$$⊢2\in \mathrm{V}$$
5		fveq2	$$⊢x=1\to F\left(x\right)=F\left(1\right)$$
6		iftrue	$$⊢x=1\to if\left(x=1,A,B\right)=A$$
7	5 6	eqeq12d	$$⊢x=1\to \left(F\left(x\right)=if\left(x=1,A,B\right)\leftrightarrow F\left(1\right)=A\right)$$
8		fveq2	$$⊢x=2\to F\left(x\right)=F\left(2\right)$$
9		1ne2	$$⊢1\ne 2$$
10	9	necomi	$$⊢2\ne 1$$
11		pm13.181	$$⊢\left(x=2\wedge 2\ne 1\right)\to x\ne 1$$
12	10 11	mpan2	$$⊢x=2\to x\ne 1$$
13	12	neneqd	$$⊢x=2\to \neg x=1$$
14	13	iffalsed	$$⊢x=2\to if\left(x=1,A,B\right)=B$$
15	8 14	eqeq12d	$$⊢x=2\to \left(F\left(x\right)=if\left(x=1,A,B\right)\leftrightarrow F\left(2\right)=B\right)$$
16	3 4 7 15	ralpr	$$⊢\forall x\in \left\{1,2\right\}F\left(x\right)=if\left(x=1,A,B\right)\leftrightarrow \left(F\left(1\right)=A\wedge F\left(2\right)=B\right)$$
17	2 16	bitri	$$⊢\forall x\in \left(1\dots 2\right)F\left(x\right)=if\left(x=1,A,B\right)\leftrightarrow \left(F\left(1\right)=A\wedge F\left(2\right)=B\right)$$