This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fnpr2g

Description: A function whose domain has at most two elements can be represented as a set of at most two ordered pairs. (Contributed by Thierry Arnoux, 12-Jul-2020)

Ref Expression
Assertion fnpr2g ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐹 Fn { 𝐴 , 𝐵 } ↔ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ) )

Proof

Step Hyp Ref Expression
1 preq1 ⊢ ( 𝑎 = 𝐴 → { 𝑎 , 𝑏 } = { 𝐴 , 𝑏 } )
2 1 fneq2d ⊢ ( 𝑎 = 𝐴 → ( 𝐹 Fn { 𝑎 , 𝑏 } ↔ 𝐹 Fn { 𝐴 , 𝑏 } ) )
3 id ⊢ ( 𝑎 = 𝐴 → 𝑎 = 𝐴 )
4 fveq2 ⊢ ( 𝑎 = 𝐴 → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝐴 ) )
5 3 4 opeq12d ⊢ ( 𝑎 = 𝐴 → ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ = ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ )
6 5 preq1d ⊢ ( 𝑎 = 𝐴 → { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ , ⟨ 𝑏 , ( 𝐹 ‘ 𝑏 ) ⟩ } = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝑏 , ( 𝐹 ‘ 𝑏 ) ⟩ } )
7 6 eqeq2d ⊢ ( 𝑎 = 𝐴 → ( 𝐹 = { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ , ⟨ 𝑏 , ( 𝐹 ‘ 𝑏 ) ⟩ } ↔ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝑏 , ( 𝐹 ‘ 𝑏 ) ⟩ } ) )
8 2 7 bibi12d ⊢ ( 𝑎 = 𝐴 → ( ( 𝐹 Fn { 𝑎 , 𝑏 } ↔ 𝐹 = { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ , ⟨ 𝑏 , ( 𝐹 ‘ 𝑏 ) ⟩ } ) ↔ ( 𝐹 Fn { 𝐴 , 𝑏 } ↔ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝑏 , ( 𝐹 ‘ 𝑏 ) ⟩ } ) ) )
9 preq2 ⊢ ( 𝑏 = 𝐵 → { 𝐴 , 𝑏 } = { 𝐴 , 𝐵 } )
10 9 fneq2d ⊢ ( 𝑏 = 𝐵 → ( 𝐹 Fn { 𝐴 , 𝑏 } ↔ 𝐹 Fn { 𝐴 , 𝐵 } ) )
11 id ⊢ ( 𝑏 = 𝐵 → 𝑏 = 𝐵 )
12 fveq2 ⊢ ( 𝑏 = 𝐵 → ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝐵 ) )
13 11 12 opeq12d ⊢ ( 𝑏 = 𝐵 → ⟨ 𝑏 , ( 𝐹 ‘ 𝑏 ) ⟩ = ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ )
14 13 preq2d ⊢ ( 𝑏 = 𝐵 → { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝑏 , ( 𝐹 ‘ 𝑏 ) ⟩ } = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } )
15 14 eqeq2d ⊢ ( 𝑏 = 𝐵 → ( 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝑏 , ( 𝐹 ‘ 𝑏 ) ⟩ } ↔ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ) )
16 10 15 bibi12d ⊢ ( 𝑏 = 𝐵 → ( ( 𝐹 Fn { 𝐴 , 𝑏 } ↔ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝑏 , ( 𝐹 ‘ 𝑏 ) ⟩ } ) ↔ ( 𝐹 Fn { 𝐴 , 𝐵 } ↔ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ) ) )
17 vex ⊢ 𝑎 ∈ V
18 vex ⊢ 𝑏 ∈ V
19 17 18 fnprb ⊢ ( 𝐹 Fn { 𝑎 , 𝑏 } ↔ 𝐹 = { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ , ⟨ 𝑏 , ( 𝐹 ‘ 𝑏 ) ⟩ } )
20 8 16 19 vtocl2g ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐹 Fn { 𝐴 , 𝐵 } ↔ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ) )