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 ) ⟩ } = 𝐺 )