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