Theorem xpsfeq

Description: A function on 2o is determined by its values at zero and one. (Contributed by Mario Carneiro, 27-Aug-2015)

	Ref	Expression
Assertion	xpsfeq	$$⊢GFn{2}_{𝑜}\to \left\{⟨\varnothing ,G\left(\varnothing \right)⟩,⟨1_{𝑜},G\left(1_{𝑜}\right)⟩\right\}=G$$

Proof

Step	Hyp	Ref	Expression
1		fvex	$$⊢G\left(\varnothing \right)\in \mathrm{V}$$
2		fvex	$$⊢G\left(1_{𝑜}\right)\in \mathrm{V}$$
3		fnpr2o	$$⊢\left(G\left(\varnothing \right)\in \mathrm{V}\wedge G\left(1_{𝑜}\right)\in \mathrm{V}\right)\to \left\{⟨\varnothing ,G\left(\varnothing \right)⟩,⟨1_{𝑜},G\left(1_{𝑜}\right)⟩\right\}Fn{2}_{𝑜}$$
4	1 2 3	mp2an	$$⊢\left\{⟨\varnothing ,G\left(\varnothing \right)⟩,⟨1_{𝑜},G\left(1_{𝑜}\right)⟩\right\}Fn{2}_{𝑜}$$
5	4	a1i	$$⊢GFn{2}_{𝑜}\to \left\{⟨\varnothing ,G\left(\varnothing \right)⟩,⟨1_{𝑜},G\left(1_{𝑜}\right)⟩\right\}Fn{2}_{𝑜}$$
6		id	$$⊢GFn{2}_{𝑜}\to GFn{2}_{𝑜}$$
7		elpri	$$⊢k\in \left\{\varnothing ,1_{𝑜}\right\}\to \left(k=\varnothing \vee k=1_{𝑜}\right)$$
8		df2o3	$$⊢2_{𝑜}=\left\{\varnothing ,1_{𝑜}\right\}$$
9	7 8	eleq2s	$$⊢k\in 2_{𝑜}\to \left(k=\varnothing \vee k=1_{𝑜}\right)$$
10		fvpr0o	$$⊢G\left(\varnothing \right)\in \mathrm{V}\to \left\{⟨\varnothing ,G\left(\varnothing \right)⟩,⟨1_{𝑜},G\left(1_{𝑜}\right)⟩\right\}\left(\varnothing \right)=G\left(\varnothing \right)$$
11	1 10	ax-mp	$$⊢\left\{⟨\varnothing ,G\left(\varnothing \right)⟩,⟨1_{𝑜},G\left(1_{𝑜}\right)⟩\right\}\left(\varnothing \right)=G\left(\varnothing \right)$$
12		fveq2	$$⊢k=\varnothing \to \left\{⟨\varnothing ,G\left(\varnothing \right)⟩,⟨1_{𝑜},G\left(1_{𝑜}\right)⟩\right\}\left(k\right)=\left\{⟨\varnothing ,G\left(\varnothing \right)⟩,⟨1_{𝑜},G\left(1_{𝑜}\right)⟩\right\}\left(\varnothing \right)$$
13		fveq2	$$⊢k=\varnothing \to G\left(k\right)=G\left(\varnothing \right)$$
14	11 12 13	3eqtr4a	$$⊢k=\varnothing \to \left\{⟨\varnothing ,G\left(\varnothing \right)⟩,⟨1_{𝑜},G\left(1_{𝑜}\right)⟩\right\}\left(k\right)=G\left(k\right)$$
15		fvpr1o	$$⊢G\left(1_{𝑜}\right)\in \mathrm{V}\to \left\{⟨\varnothing ,G\left(\varnothing \right)⟩,⟨1_{𝑜},G\left(1_{𝑜}\right)⟩\right\}\left(1_{𝑜}\right)=G\left(1_{𝑜}\right)$$
16	2 15	ax-mp	$$⊢\left\{⟨\varnothing ,G\left(\varnothing \right)⟩,⟨1_{𝑜},G\left(1_{𝑜}\right)⟩\right\}\left(1_{𝑜}\right)=G\left(1_{𝑜}\right)$$
17		fveq2	$$⊢k=1_{𝑜}\to \left\{⟨\varnothing ,G\left(\varnothing \right)⟩,⟨1_{𝑜},G\left(1_{𝑜}\right)⟩\right\}\left(k\right)=\left\{⟨\varnothing ,G\left(\varnothing \right)⟩,⟨1_{𝑜},G\left(1_{𝑜}\right)⟩\right\}\left(1_{𝑜}\right)$$
18		fveq2	$$⊢k=1_{𝑜}\to G\left(k\right)=G\left(1_{𝑜}\right)$$
19	16 17 18	3eqtr4a	$$⊢k=1_{𝑜}\to \left\{⟨\varnothing ,G\left(\varnothing \right)⟩,⟨1_{𝑜},G\left(1_{𝑜}\right)⟩\right\}\left(k\right)=G\left(k\right)$$
20	14 19	jaoi	$$⊢\left(k=\varnothing \vee k=1_{𝑜}\right)\to \left\{⟨\varnothing ,G\left(\varnothing \right)⟩,⟨1_{𝑜},G\left(1_{𝑜}\right)⟩\right\}\left(k\right)=G\left(k\right)$$
21	9 20	syl	$$⊢k\in 2_{𝑜}\to \left\{⟨\varnothing ,G\left(\varnothing \right)⟩,⟨1_{𝑜},G\left(1_{𝑜}\right)⟩\right\}\left(k\right)=G\left(k\right)$$
22	21	adantl	$$⊢\left(GFn{2}_{𝑜}\wedge k\in 2_{𝑜}\right)\to \left\{⟨\varnothing ,G\left(\varnothing \right)⟩,⟨1_{𝑜},G\left(1_{𝑜}\right)⟩\right\}\left(k\right)=G\left(k\right)$$
23	5 6 22	eqfnfvd	$$⊢GFn{2}_{𝑜}\to \left\{⟨\varnothing ,G\left(\varnothing \right)⟩,⟨1_{𝑜},G\left(1_{𝑜}\right)⟩\right\}=G$$