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 { 𝐴 , 𝐵 } ↔ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ) )