Metamath Proof Explorer


Theorem fnprb

Description: A function whose domain has at most two elements can be represented as a set of at most two ordered pairs. (Contributed by FL, 26-Jun-2011) (Proof shortened by Scott Fenton, 12-Oct-2017) Eliminate unnecessary antecedent A =/= B . (Revised by NM, 29-Dec-2018)

Ref Expression
Hypotheses fnprb.a 𝐴 ∈ V
fnprb.b 𝐵 ∈ V
Assertion fnprb ( 𝐹 Fn { 𝐴 , 𝐵 } ↔ 𝐹 = { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹𝐵 ) ⟩ } )

Proof

Step Hyp Ref Expression
1 fnprb.a 𝐴 ∈ V
2 fnprb.b 𝐵 ∈ V
3 1 fnsnb ( 𝐹 Fn { 𝐴 } ↔ 𝐹 = { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ } )
4 dfsn2 { 𝐴 } = { 𝐴 , 𝐴 }
5 4 fneq2i ( 𝐹 Fn { 𝐴 } ↔ 𝐹 Fn { 𝐴 , 𝐴 } )
6 dfsn2 { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ } = { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ , ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ }
7 6 eqeq2i ( 𝐹 = { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ } ↔ 𝐹 = { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ , ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ } )
8 3 5 7 3bitr3i ( 𝐹 Fn { 𝐴 , 𝐴 } ↔ 𝐹 = { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ , ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ } )
9 8 a1i ( 𝐴 = 𝐵 → ( 𝐹 Fn { 𝐴 , 𝐴 } ↔ 𝐹 = { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ , ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ } ) )
10 preq2 ( 𝐴 = 𝐵 → { 𝐴 , 𝐴 } = { 𝐴 , 𝐵 } )
11 10 fneq2d ( 𝐴 = 𝐵 → ( 𝐹 Fn { 𝐴 , 𝐴 } ↔ 𝐹 Fn { 𝐴 , 𝐵 } ) )
12 id ( 𝐴 = 𝐵𝐴 = 𝐵 )
13 fveq2 ( 𝐴 = 𝐵 → ( 𝐹𝐴 ) = ( 𝐹𝐵 ) )
14 12 13 opeq12d ( 𝐴 = 𝐵 → ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ = ⟨ 𝐵 , ( 𝐹𝐵 ) ⟩ )
15 14 preq2d ( 𝐴 = 𝐵 → { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ , ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ } = { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹𝐵 ) ⟩ } )
16 15 eqeq2d ( 𝐴 = 𝐵 → ( 𝐹 = { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ , ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ } ↔ 𝐹 = { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹𝐵 ) ⟩ } ) )
17 9 11 16 3bitr3d ( 𝐴 = 𝐵 → ( 𝐹 Fn { 𝐴 , 𝐵 } ↔ 𝐹 = { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹𝐵 ) ⟩ } ) )
18 fndm ( 𝐹 Fn { 𝐴 , 𝐵 } → dom 𝐹 = { 𝐴 , 𝐵 } )
19 fvex ( 𝐹𝐴 ) ∈ V
20 fvex ( 𝐹𝐵 ) ∈ V
21 19 20 dmprop dom { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹𝐵 ) ⟩ } = { 𝐴 , 𝐵 }
22 18 21 eqtr4di ( 𝐹 Fn { 𝐴 , 𝐵 } → dom 𝐹 = dom { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹𝐵 ) ⟩ } )
23 22 adantl ( ( 𝐴𝐵𝐹 Fn { 𝐴 , 𝐵 } ) → dom 𝐹 = dom { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹𝐵 ) ⟩ } )
24 18 adantl ( ( 𝐴𝐵𝐹 Fn { 𝐴 , 𝐵 } ) → dom 𝐹 = { 𝐴 , 𝐵 } )
25 24 eleq2d ( ( 𝐴𝐵𝐹 Fn { 𝐴 , 𝐵 } ) → ( 𝑥 ∈ dom 𝐹𝑥 ∈ { 𝐴 , 𝐵 } ) )
26 vex 𝑥 ∈ V
27 26 elpr ( 𝑥 ∈ { 𝐴 , 𝐵 } ↔ ( 𝑥 = 𝐴𝑥 = 𝐵 ) )
28 1 19 fvpr1 ( 𝐴𝐵 → ( { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹𝐵 ) ⟩ } ‘ 𝐴 ) = ( 𝐹𝐴 ) )
29 28 adantr ( ( 𝐴𝐵𝐹 Fn { 𝐴 , 𝐵 } ) → ( { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹𝐵 ) ⟩ } ‘ 𝐴 ) = ( 𝐹𝐴 ) )
30 29 eqcomd ( ( 𝐴𝐵𝐹 Fn { 𝐴 , 𝐵 } ) → ( 𝐹𝐴 ) = ( { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹𝐵 ) ⟩ } ‘ 𝐴 ) )
31 fveq2 ( 𝑥 = 𝐴 → ( 𝐹𝑥 ) = ( 𝐹𝐴 ) )
32 fveq2 ( 𝑥 = 𝐴 → ( { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹𝐵 ) ⟩ } ‘ 𝑥 ) = ( { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹𝐵 ) ⟩ } ‘ 𝐴 ) )
33 31 32 eqeq12d ( 𝑥 = 𝐴 → ( ( 𝐹𝑥 ) = ( { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹𝐵 ) ⟩ } ‘ 𝑥 ) ↔ ( 𝐹𝐴 ) = ( { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹𝐵 ) ⟩ } ‘ 𝐴 ) ) )
34 30 33 syl5ibrcom ( ( 𝐴𝐵𝐹 Fn { 𝐴 , 𝐵 } ) → ( 𝑥 = 𝐴 → ( 𝐹𝑥 ) = ( { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹𝐵 ) ⟩ } ‘ 𝑥 ) ) )
35 2 20 fvpr2 ( 𝐴𝐵 → ( { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹𝐵 ) ⟩ } ‘ 𝐵 ) = ( 𝐹𝐵 ) )
36 35 adantr ( ( 𝐴𝐵𝐹 Fn { 𝐴 , 𝐵 } ) → ( { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹𝐵 ) ⟩ } ‘ 𝐵 ) = ( 𝐹𝐵 ) )
37 36 eqcomd ( ( 𝐴𝐵𝐹 Fn { 𝐴 , 𝐵 } ) → ( 𝐹𝐵 ) = ( { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹𝐵 ) ⟩ } ‘ 𝐵 ) )
38 fveq2 ( 𝑥 = 𝐵 → ( 𝐹𝑥 ) = ( 𝐹𝐵 ) )
39 fveq2 ( 𝑥 = 𝐵 → ( { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹𝐵 ) ⟩ } ‘ 𝑥 ) = ( { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹𝐵 ) ⟩ } ‘ 𝐵 ) )
40 38 39 eqeq12d ( 𝑥 = 𝐵 → ( ( 𝐹𝑥 ) = ( { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹𝐵 ) ⟩ } ‘ 𝑥 ) ↔ ( 𝐹𝐵 ) = ( { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹𝐵 ) ⟩ } ‘ 𝐵 ) ) )
41 37 40 syl5ibrcom ( ( 𝐴𝐵𝐹 Fn { 𝐴 , 𝐵 } ) → ( 𝑥 = 𝐵 → ( 𝐹𝑥 ) = ( { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹𝐵 ) ⟩ } ‘ 𝑥 ) ) )
42 34 41 jaod ( ( 𝐴𝐵𝐹 Fn { 𝐴 , 𝐵 } ) → ( ( 𝑥 = 𝐴𝑥 = 𝐵 ) → ( 𝐹𝑥 ) = ( { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹𝐵 ) ⟩ } ‘ 𝑥 ) ) )
43 27 42 syl5bi ( ( 𝐴𝐵𝐹 Fn { 𝐴 , 𝐵 } ) → ( 𝑥 ∈ { 𝐴 , 𝐵 } → ( 𝐹𝑥 ) = ( { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹𝐵 ) ⟩ } ‘ 𝑥 ) ) )
44 25 43 sylbid ( ( 𝐴𝐵𝐹 Fn { 𝐴 , 𝐵 } ) → ( 𝑥 ∈ dom 𝐹 → ( 𝐹𝑥 ) = ( { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹𝐵 ) ⟩ } ‘ 𝑥 ) ) )
45 44 ralrimiv ( ( 𝐴𝐵𝐹 Fn { 𝐴 , 𝐵 } ) → ∀ 𝑥 ∈ dom 𝐹 ( 𝐹𝑥 ) = ( { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹𝐵 ) ⟩ } ‘ 𝑥 ) )
46 fnfun ( 𝐹 Fn { 𝐴 , 𝐵 } → Fun 𝐹 )
47 1 2 19 20 funpr ( 𝐴𝐵 → Fun { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹𝐵 ) ⟩ } )
48 eqfunfv ( ( Fun 𝐹 ∧ Fun { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹𝐵 ) ⟩ } ) → ( 𝐹 = { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹𝐵 ) ⟩ } ↔ ( dom 𝐹 = dom { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹𝐵 ) ⟩ } ∧ ∀ 𝑥 ∈ dom 𝐹 ( 𝐹𝑥 ) = ( { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹𝐵 ) ⟩ } ‘ 𝑥 ) ) ) )
49 46 47 48 syl2anr ( ( 𝐴𝐵𝐹 Fn { 𝐴 , 𝐵 } ) → ( 𝐹 = { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹𝐵 ) ⟩ } ↔ ( dom 𝐹 = dom { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹𝐵 ) ⟩ } ∧ ∀ 𝑥 ∈ dom 𝐹 ( 𝐹𝑥 ) = ( { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹𝐵 ) ⟩ } ‘ 𝑥 ) ) ) )
50 23 45 49 mpbir2and ( ( 𝐴𝐵𝐹 Fn { 𝐴 , 𝐵 } ) → 𝐹 = { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹𝐵 ) ⟩ } )
51 df-fn ( { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹𝐵 ) ⟩ } Fn { 𝐴 , 𝐵 } ↔ ( Fun { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹𝐵 ) ⟩ } ∧ dom { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹𝐵 ) ⟩ } = { 𝐴 , 𝐵 } ) )
52 47 21 51 sylanblrc ( 𝐴𝐵 → { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹𝐵 ) ⟩ } Fn { 𝐴 , 𝐵 } )
53 fneq1 ( 𝐹 = { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹𝐵 ) ⟩ } → ( 𝐹 Fn { 𝐴 , 𝐵 } ↔ { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹𝐵 ) ⟩ } Fn { 𝐴 , 𝐵 } ) )
54 53 biimprd ( 𝐹 = { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹𝐵 ) ⟩ } → ( { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹𝐵 ) ⟩ } Fn { 𝐴 , 𝐵 } → 𝐹 Fn { 𝐴 , 𝐵 } ) )
55 52 54 mpan9 ( ( 𝐴𝐵𝐹 = { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹𝐵 ) ⟩ } ) → 𝐹 Fn { 𝐴 , 𝐵 } )
56 50 55 impbida ( 𝐴𝐵 → ( 𝐹 Fn { 𝐴 , 𝐵 } ↔ 𝐹 = { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹𝐵 ) ⟩ } ) )
57 17 56 pm2.61ine ( 𝐹 Fn { 𝐴 , 𝐵 } ↔ 𝐹 = { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹𝐵 ) ⟩ } )