Metamath Proof Explorer


Theorem fressnfv

Description: The value of a function restricted to a singleton. (Contributed by NM, 9-Oct-2004)

Ref Expression
Assertion fressnfv ( ( 𝐹 Fn 𝐴𝐵𝐴 ) → ( ( 𝐹 ↾ { 𝐵 } ) : { 𝐵 } ⟶ 𝐶 ↔ ( 𝐹𝐵 ) ∈ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 sneq ( 𝑥 = 𝐵 → { 𝑥 } = { 𝐵 } )
2 reseq2 ( { 𝑥 } = { 𝐵 } → ( 𝐹 ↾ { 𝑥 } ) = ( 𝐹 ↾ { 𝐵 } ) )
3 2 feq1d ( { 𝑥 } = { 𝐵 } → ( ( 𝐹 ↾ { 𝑥 } ) : { 𝑥 } ⟶ 𝐶 ↔ ( 𝐹 ↾ { 𝐵 } ) : { 𝑥 } ⟶ 𝐶 ) )
4 feq2 ( { 𝑥 } = { 𝐵 } → ( ( 𝐹 ↾ { 𝐵 } ) : { 𝑥 } ⟶ 𝐶 ↔ ( 𝐹 ↾ { 𝐵 } ) : { 𝐵 } ⟶ 𝐶 ) )
5 3 4 bitrd ( { 𝑥 } = { 𝐵 } → ( ( 𝐹 ↾ { 𝑥 } ) : { 𝑥 } ⟶ 𝐶 ↔ ( 𝐹 ↾ { 𝐵 } ) : { 𝐵 } ⟶ 𝐶 ) )
6 1 5 syl ( 𝑥 = 𝐵 → ( ( 𝐹 ↾ { 𝑥 } ) : { 𝑥 } ⟶ 𝐶 ↔ ( 𝐹 ↾ { 𝐵 } ) : { 𝐵 } ⟶ 𝐶 ) )
7 fveq2 ( 𝑥 = 𝐵 → ( 𝐹𝑥 ) = ( 𝐹𝐵 ) )
8 7 eleq1d ( 𝑥 = 𝐵 → ( ( 𝐹𝑥 ) ∈ 𝐶 ↔ ( 𝐹𝐵 ) ∈ 𝐶 ) )
9 6 8 bibi12d ( 𝑥 = 𝐵 → ( ( ( 𝐹 ↾ { 𝑥 } ) : { 𝑥 } ⟶ 𝐶 ↔ ( 𝐹𝑥 ) ∈ 𝐶 ) ↔ ( ( 𝐹 ↾ { 𝐵 } ) : { 𝐵 } ⟶ 𝐶 ↔ ( 𝐹𝐵 ) ∈ 𝐶 ) ) )
10 9 imbi2d ( 𝑥 = 𝐵 → ( ( 𝐹 Fn 𝐴 → ( ( 𝐹 ↾ { 𝑥 } ) : { 𝑥 } ⟶ 𝐶 ↔ ( 𝐹𝑥 ) ∈ 𝐶 ) ) ↔ ( 𝐹 Fn 𝐴 → ( ( 𝐹 ↾ { 𝐵 } ) : { 𝐵 } ⟶ 𝐶 ↔ ( 𝐹𝐵 ) ∈ 𝐶 ) ) ) )
11 fnressn ( ( 𝐹 Fn 𝐴𝑥𝐴 ) → ( 𝐹 ↾ { 𝑥 } ) = { ⟨ 𝑥 , ( 𝐹𝑥 ) ⟩ } )
12 vsnid 𝑥 ∈ { 𝑥 }
13 fvres ( 𝑥 ∈ { 𝑥 } → ( ( 𝐹 ↾ { 𝑥 } ) ‘ 𝑥 ) = ( 𝐹𝑥 ) )
14 12 13 ax-mp ( ( 𝐹 ↾ { 𝑥 } ) ‘ 𝑥 ) = ( 𝐹𝑥 )
15 14 opeq2i 𝑥 , ( ( 𝐹 ↾ { 𝑥 } ) ‘ 𝑥 ) ⟩ = ⟨ 𝑥 , ( 𝐹𝑥 ) ⟩
16 15 sneqi { ⟨ 𝑥 , ( ( 𝐹 ↾ { 𝑥 } ) ‘ 𝑥 ) ⟩ } = { ⟨ 𝑥 , ( 𝐹𝑥 ) ⟩ }
17 16 eqeq2i ( ( 𝐹 ↾ { 𝑥 } ) = { ⟨ 𝑥 , ( ( 𝐹 ↾ { 𝑥 } ) ‘ 𝑥 ) ⟩ } ↔ ( 𝐹 ↾ { 𝑥 } ) = { ⟨ 𝑥 , ( 𝐹𝑥 ) ⟩ } )
18 vex 𝑥 ∈ V
19 18 fsn2 ( ( 𝐹 ↾ { 𝑥 } ) : { 𝑥 } ⟶ 𝐶 ↔ ( ( ( 𝐹 ↾ { 𝑥 } ) ‘ 𝑥 ) ∈ 𝐶 ∧ ( 𝐹 ↾ { 𝑥 } ) = { ⟨ 𝑥 , ( ( 𝐹 ↾ { 𝑥 } ) ‘ 𝑥 ) ⟩ } ) )
20 iba ( ( 𝐹 ↾ { 𝑥 } ) = { ⟨ 𝑥 , ( ( 𝐹 ↾ { 𝑥 } ) ‘ 𝑥 ) ⟩ } → ( ( ( 𝐹 ↾ { 𝑥 } ) ‘ 𝑥 ) ∈ 𝐶 ↔ ( ( ( 𝐹 ↾ { 𝑥 } ) ‘ 𝑥 ) ∈ 𝐶 ∧ ( 𝐹 ↾ { 𝑥 } ) = { ⟨ 𝑥 , ( ( 𝐹 ↾ { 𝑥 } ) ‘ 𝑥 ) ⟩ } ) ) )
21 14 eleq1i ( ( ( 𝐹 ↾ { 𝑥 } ) ‘ 𝑥 ) ∈ 𝐶 ↔ ( 𝐹𝑥 ) ∈ 𝐶 )
22 20 21 bitr3di ( ( 𝐹 ↾ { 𝑥 } ) = { ⟨ 𝑥 , ( ( 𝐹 ↾ { 𝑥 } ) ‘ 𝑥 ) ⟩ } → ( ( ( ( 𝐹 ↾ { 𝑥 } ) ‘ 𝑥 ) ∈ 𝐶 ∧ ( 𝐹 ↾ { 𝑥 } ) = { ⟨ 𝑥 , ( ( 𝐹 ↾ { 𝑥 } ) ‘ 𝑥 ) ⟩ } ) ↔ ( 𝐹𝑥 ) ∈ 𝐶 ) )
23 19 22 bitrid ( ( 𝐹 ↾ { 𝑥 } ) = { ⟨ 𝑥 , ( ( 𝐹 ↾ { 𝑥 } ) ‘ 𝑥 ) ⟩ } → ( ( 𝐹 ↾ { 𝑥 } ) : { 𝑥 } ⟶ 𝐶 ↔ ( 𝐹𝑥 ) ∈ 𝐶 ) )
24 17 23 sylbir ( ( 𝐹 ↾ { 𝑥 } ) = { ⟨ 𝑥 , ( 𝐹𝑥 ) ⟩ } → ( ( 𝐹 ↾ { 𝑥 } ) : { 𝑥 } ⟶ 𝐶 ↔ ( 𝐹𝑥 ) ∈ 𝐶 ) )
25 11 24 syl ( ( 𝐹 Fn 𝐴𝑥𝐴 ) → ( ( 𝐹 ↾ { 𝑥 } ) : { 𝑥 } ⟶ 𝐶 ↔ ( 𝐹𝑥 ) ∈ 𝐶 ) )
26 25 expcom ( 𝑥𝐴 → ( 𝐹 Fn 𝐴 → ( ( 𝐹 ↾ { 𝑥 } ) : { 𝑥 } ⟶ 𝐶 ↔ ( 𝐹𝑥 ) ∈ 𝐶 ) ) )
27 10 26 vtoclga ( 𝐵𝐴 → ( 𝐹 Fn 𝐴 → ( ( 𝐹 ↾ { 𝐵 } ) : { 𝐵 } ⟶ 𝐶 ↔ ( 𝐹𝐵 ) ∈ 𝐶 ) ) )
28 27 impcom ( ( 𝐹 Fn 𝐴𝐵𝐴 ) → ( ( 𝐹 ↾ { 𝐵 } ) : { 𝐵 } ⟶ 𝐶 ↔ ( 𝐹𝐵 ) ∈ 𝐶 ) )