Metamath Proof Explorer

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 ⊢ G Fn 2 𝑜 → ∅ G ⁡ ∅ 1 𝑜 G ⁡ 1 𝑜 = G

Proof

Step Hyp Ref Expression
1 fvex ⊢ G ⁡ ∅ ∈ V
2 fvex ⊢ G ⁡ 1 𝑜 ∈ V
3 fnpr2o ⊢ G ⁡ ∅ ∈ V ∧ G ⁡ 1 𝑜 ∈ V → ∅ G ⁡ ∅ 1 𝑜 G ⁡ 1 𝑜 Fn 2 𝑜
4 1 2 3 mp2an ⊢ ∅ G ⁡ ∅ 1 𝑜 G ⁡ 1 𝑜 Fn 2 𝑜
5 4 a1i ⊢ G Fn 2 𝑜 → ∅ G ⁡ ∅ 1 𝑜 G ⁡ 1 𝑜 Fn 2 𝑜
6 id ⊢ G Fn 2 𝑜 → G Fn 2 𝑜
7 elpri ⊢ k ∈ ∅ 1 𝑜 → k = ∅ ∨ k = 1 𝑜
8 df2o3 ⊢ 2 𝑜 = ∅ 1 𝑜
9 7 8 eleq2s ⊢ k ∈ 2 𝑜 → k = ∅ ∨ k = 1 𝑜
10 fvpr0o ⊢ G ⁡ ∅ ∈ V → ∅ G ⁡ ∅ 1 𝑜 G ⁡ 1 𝑜 ⁡ ∅ = G ⁡ ∅
11 1 10 ax-mp ⊢ ∅ G ⁡ ∅ 1 𝑜 G ⁡ 1 𝑜 ⁡ ∅ = G ⁡ ∅
12 fveq2 ⊢ k = ∅ → ∅ G ⁡ ∅ 1 𝑜 G ⁡ 1 𝑜 ⁡ k = ∅ G ⁡ ∅ 1 𝑜 G ⁡ 1 𝑜 ⁡ ∅
13 fveq2 ⊢ k = ∅ → G ⁡ k = G ⁡ ∅
14 11 12 13 3eqtr4a ⊢ k = ∅ → ∅ G ⁡ ∅ 1 𝑜 G ⁡ 1 𝑜 ⁡ k = G ⁡ k
15 fvpr1o ⊢ G ⁡ 1 𝑜 ∈ V → ∅ G ⁡ ∅ 1 𝑜 G ⁡ 1 𝑜 ⁡ 1 𝑜 = G ⁡ 1 𝑜
16 2 15 ax-mp ⊢ ∅ G ⁡ ∅ 1 𝑜 G ⁡ 1 𝑜 ⁡ 1 𝑜 = G ⁡ 1 𝑜
17 fveq2 ⊢ k = 1 𝑜 → ∅ G ⁡ ∅ 1 𝑜 G ⁡ 1 𝑜 ⁡ k = ∅ G ⁡ ∅ 1 𝑜 G ⁡ 1 𝑜 ⁡ 1 𝑜
18 fveq2 ⊢ k = 1 𝑜 → G ⁡ k = G ⁡ 1 𝑜
19 16 17 18 3eqtr4a ⊢ k = 1 𝑜 → ∅ G ⁡ ∅ 1 𝑜 G ⁡ 1 𝑜 ⁡ k = G ⁡ k
20 14 19 jaoi ⊢ k = ∅ ∨ k = 1 𝑜 → ∅ G ⁡ ∅ 1 𝑜 G ⁡ 1 𝑜 ⁡ k = G ⁡ k
21 9 20 syl ⊢ k ∈ 2 𝑜 → ∅ G ⁡ ∅ 1 𝑜 G ⁡ 1 𝑜 ⁡ k = G ⁡ k
22 21 adantl ⊢ G Fn 2 𝑜 ∧ k ∈ 2 𝑜 → ∅ G ⁡ ∅ 1 𝑜 G ⁡ 1 𝑜 ⁡ k = G ⁡ k
23 5 6 22 eqfnfvd ⊢ G Fn 2 𝑜 → ∅ G ⁡ ∅ 1 𝑜 G ⁡ 1 𝑜 = G