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 syl5bb ⊢ ( ( 𝐹 ↾ { 𝑥 } ) = { ⟨ 𝑥 , ( ( 𝐹 ↾ { 𝑥 } ) ‘ 𝑥 ) ⟩ } → ( ( 𝐹 ↾ { 𝑥 } ) : { 𝑥 } ⟶ 𝐶 ↔ ( 𝐹 ‘ 𝑥 ) ∈ 𝐶 ) )
24 17 23 sylbir ⊢ ( ( 𝐹 ↾ { 𝑥 } ) = { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } → ( ( 𝐹 ↾ { 𝑥 } ) : { 𝑥 } ⟶ 𝐶 ↔ ( 𝐹 ‘ 𝑥 ) ∈ 𝐶 ) )
25 11 24 syl ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ↾ { 𝑥 } ) : { 𝑥 } ⟶ 𝐶 ↔ ( 𝐹 ‘ 𝑥 ) ∈ 𝐶 ) )
26 25 expcom ⊢ ( 𝑥 ∈ 𝐴 → ( 𝐹 Fn 𝐴 → ( ( 𝐹 ↾ { 𝑥 } ) : { 𝑥 } ⟶ 𝐶 ↔ ( 𝐹 ‘ 𝑥 ) ∈ 𝐶 ) ) )
27 10 26 vtoclga ⊢ ( 𝐵 ∈ 𝐴 → ( 𝐹 Fn 𝐴 → ( ( 𝐹 ↾ { 𝐵 } ) : { 𝐵 } ⟶ 𝐶 ↔ ( 𝐹 ‘ 𝐵 ) ∈ 𝐶 ) ) )
28 27 impcom ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( ( 𝐹 ↾ { 𝐵 } ) : { 𝐵 } ⟶ 𝐶 ↔ ( 𝐹 ‘ 𝐵 ) ∈ 𝐶 ) )