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 ( 𝐺 Fn 2o → { ⟨ ∅ , ( 𝐺 ‘ ∅ ) ⟩ , ⟨ 1o , ( 𝐺 ‘ 1o ) ⟩ } = 𝐺 )

Proof

Step Hyp Ref Expression
1 fvex ⊢ ( 𝐺 ‘ ∅ ) ∈ V
2 fvex ⊢ ( 𝐺 ‘ 1o ) ∈ V
3 fnpr2o ⊢ ( ( ( 𝐺 ‘ ∅ ) ∈ V ∧ ( 𝐺 ‘ 1o ) ∈ V ) → { ⟨ ∅ , ( 𝐺 ‘ ∅ ) ⟩ , ⟨ 1o , ( 𝐺 ‘ 1o ) ⟩ } Fn 2o )
4 1 2 3 mp2an ⊢ { ⟨ ∅ , ( 𝐺 ‘ ∅ ) ⟩ , ⟨ 1o , ( 𝐺 ‘ 1o ) ⟩ } Fn 2o
5 4 a1i ⊢ ( 𝐺 Fn 2o → { ⟨ ∅ , ( 𝐺 ‘ ∅ ) ⟩ , ⟨ 1o , ( 𝐺 ‘ 1o ) ⟩ } Fn 2o )
6 id ⊢ ( 𝐺 Fn 2o → 𝐺 Fn 2o )
7 elpri ⊢ ( 𝑘 ∈ { ∅ , 1o } → ( 𝑘 = ∅ ∨ 𝑘 = 1o ) )
8 df2o3 ⊢ 2o = { ∅ , 1o }
9 7 8 eleq2s ⊢ ( 𝑘 ∈ 2o → ( 𝑘 = ∅ ∨ 𝑘 = 1o ) )
10 fvpr0o ⊢ ( ( 𝐺 ‘ ∅ ) ∈ V → ( { ⟨ ∅ , ( 𝐺 ‘ ∅ ) ⟩ , ⟨ 1o , ( 𝐺 ‘ 1o ) ⟩ } ‘ ∅ ) = ( 𝐺 ‘ ∅ ) )
11 1 10 ax-mp ⊢ ( { ⟨ ∅ , ( 𝐺 ‘ ∅ ) ⟩ , ⟨ 1o , ( 𝐺 ‘ 1o ) ⟩ } ‘ ∅ ) = ( 𝐺 ‘ ∅ )
12 fveq2 ⊢ ( 𝑘 = ∅ → ( { ⟨ ∅ , ( 𝐺 ‘ ∅ ) ⟩ , ⟨ 1o , ( 𝐺 ‘ 1o ) ⟩ } ‘ 𝑘 ) = ( { ⟨ ∅ , ( 𝐺 ‘ ∅ ) ⟩ , ⟨ 1o , ( 𝐺 ‘ 1o ) ⟩ } ‘ ∅ ) )
13 fveq2 ⊢ ( 𝑘 = ∅ → ( 𝐺 ‘ 𝑘 ) = ( 𝐺 ‘ ∅ ) )
14 11 12 13 3eqtr4a ⊢ ( 𝑘 = ∅ → ( { ⟨ ∅ , ( 𝐺 ‘ ∅ ) ⟩ , ⟨ 1o , ( 𝐺 ‘ 1o ) ⟩ } ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) )
15 fvpr1o ⊢ ( ( 𝐺 ‘ 1o ) ∈ V → ( { ⟨ ∅ , ( 𝐺 ‘ ∅ ) ⟩ , ⟨ 1o , ( 𝐺 ‘ 1o ) ⟩ } ‘ 1o ) = ( 𝐺 ‘ 1o ) )
16 2 15 ax-mp ⊢ ( { ⟨ ∅ , ( 𝐺 ‘ ∅ ) ⟩ , ⟨ 1o , ( 𝐺 ‘ 1o ) ⟩ } ‘ 1o ) = ( 𝐺 ‘ 1o )
17 fveq2 ⊢ ( 𝑘 = 1o → ( { ⟨ ∅ , ( 𝐺 ‘ ∅ ) ⟩ , ⟨ 1o , ( 𝐺 ‘ 1o ) ⟩ } ‘ 𝑘 ) = ( { ⟨ ∅ , ( 𝐺 ‘ ∅ ) ⟩ , ⟨ 1o , ( 𝐺 ‘ 1o ) ⟩ } ‘ 1o ) )
18 fveq2 ⊢ ( 𝑘 = 1o → ( 𝐺 ‘ 𝑘 ) = ( 𝐺 ‘ 1o ) )
19 16 17 18 3eqtr4a ⊢ ( 𝑘 = 1o → ( { ⟨ ∅ , ( 𝐺 ‘ ∅ ) ⟩ , ⟨ 1o , ( 𝐺 ‘ 1o ) ⟩ } ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) )
20 14 19 jaoi ⊢ ( ( 𝑘 = ∅ ∨ 𝑘 = 1o ) → ( { ⟨ ∅ , ( 𝐺 ‘ ∅ ) ⟩ , ⟨ 1o , ( 𝐺 ‘ 1o ) ⟩ } ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) )
21 9 20 syl ⊢ ( 𝑘 ∈ 2o → ( { ⟨ ∅ , ( 𝐺 ‘ ∅ ) ⟩ , ⟨ 1o , ( 𝐺 ‘ 1o ) ⟩ } ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) )
22 21 adantl ⊢ ( ( 𝐺 Fn 2o ∧ 𝑘 ∈ 2o ) → ( { ⟨ ∅ , ( 𝐺 ‘ ∅ ) ⟩ , ⟨ 1o , ( 𝐺 ‘ 1o ) ⟩ } ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) )
23 5 6 22 eqfnfvd ⊢ ( 𝐺 Fn 2o → { ⟨ ∅ , ( 𝐺 ‘ ∅ ) ⟩ , ⟨ 1o , ( 𝐺 ‘ 1o ) ⟩ } = 𝐺 )