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 ⊢ A ∈ V ∧ B ∈ W → F Fn A B ↔ F = A F ⁡ A B F ⁡ B

Proof

Step Hyp Ref Expression
1 preq1 ⊢ a = A → a b = A b
2 1 fneq2d ⊢ a = A → F Fn a b ↔ F Fn A b
3 id ⊢ a = A → a = A
4 fveq2 ⊢ a = A → F ⁡ a = F ⁡ A
5 3 4 opeq12d ⊢ a = A → a F ⁡ a = A F ⁡ A
6 5 preq1d ⊢ a = A → a F ⁡ a b F ⁡ b = A F ⁡ A b F ⁡ b
7 6 eqeq2d ⊢ a = A → F = a F ⁡ a b F ⁡ b ↔ F = A F ⁡ A b F ⁡ b
8 2 7 bibi12d ⊢ a = A → F Fn a b ↔ F = a F ⁡ a b F ⁡ b ↔ F Fn A b ↔ F = A F ⁡ A b F ⁡ b
9 preq2 ⊢ b = B → A b = A B
10 9 fneq2d ⊢ b = B → F Fn A b ↔ F Fn A B
11 id ⊢ b = B → b = B
12 fveq2 ⊢ b = B → F ⁡ b = F ⁡ B
13 11 12 opeq12d ⊢ b = B → b F ⁡ b = B F ⁡ B
14 13 preq2d ⊢ b = B → A F ⁡ A b F ⁡ b = A F ⁡ A B F ⁡ B
15 14 eqeq2d ⊢ b = B → F = A F ⁡ A b F ⁡ b ↔ F = A F ⁡ A B F ⁡ B
16 10 15 bibi12d ⊢ b = B → F Fn A b ↔ F = A F ⁡ A b F ⁡ b ↔ F Fn A B ↔ F = A F ⁡ A B F ⁡ B
17 vex ⊢ a ∈ V
18 vex ⊢ b ∈ V
19 17 18 fnprb ⊢ F Fn a b ↔ F = a F ⁡ a b F ⁡ b
20 8 16 19 vtocl2g ⊢ A ∈ V ∧ B ∈ W → F Fn A B ↔ F = A F ⁡ A B F ⁡ B