Metamath Proof Explorer

Theorem resf1ext2b

Description: Extension of an injection which is a restriction of a function. (Contributed by AV, 3-Oct-2025)

Ref Expression
Assertion resf1ext2b ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) → ( ( Fun ◡ ( 𝐹 ↾ 𝐶 ) ∧ ( 𝐹 ‘ 𝑋 ) ∉ ( 𝐹 “ 𝐶 ) ) ↔ Fun ◡ ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ) )

Proof

Step Hyp Ref Expression
1 fssres ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐶 ⊆ 𝐴 ) → ( 𝐹 ↾ 𝐶 ) : 𝐶 ⟶ 𝐵 )
2 1 3adant2 ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) → ( 𝐹 ↾ 𝐶 ) : 𝐶 ⟶ 𝐵 )
3 df-f1 ⊢ ( ( 𝐹 ↾ 𝐶 ) : 𝐶 –1-1→ 𝐵 ↔ ( ( 𝐹 ↾ 𝐶 ) : 𝐶 ⟶ 𝐵 ∧ Fun ◡ ( 𝐹 ↾ 𝐶 ) ) )
4 resf1extb ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) → ( ( ( 𝐹 ↾ 𝐶 ) : 𝐶 –1-1→ 𝐵 ∧ ( 𝐹 ‘ 𝑋 ) ∉ ( 𝐹 “ 𝐶 ) ) ↔ ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) : ( 𝐶 ∪ { 𝑋 } ) –1-1→ 𝐵 ) )
5 df-f1 ⊢ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) : ( 𝐶 ∪ { 𝑋 } ) –1-1→ 𝐵 ↔ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) : ( 𝐶 ∪ { 𝑋 } ) ⟶ 𝐵 ∧ Fun ◡ ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ) )
6 5 simprbi ⊢ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) : ( 𝐶 ∪ { 𝑋 } ) –1-1→ 𝐵 → Fun ◡ ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) )
7 4 6 biimtrdi ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) → ( ( ( 𝐹 ↾ 𝐶 ) : 𝐶 –1-1→ 𝐵 ∧ ( 𝐹 ‘ 𝑋 ) ∉ ( 𝐹 “ 𝐶 ) ) → Fun ◡ ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ) )
8 7 expd ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) → ( ( 𝐹 ↾ 𝐶 ) : 𝐶 –1-1→ 𝐵 → ( ( 𝐹 ‘ 𝑋 ) ∉ ( 𝐹 “ 𝐶 ) → Fun ◡ ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ) ) )
9 3 8 biimtrrid ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) → ( ( ( 𝐹 ↾ 𝐶 ) : 𝐶 ⟶ 𝐵 ∧ Fun ◡ ( 𝐹 ↾ 𝐶 ) ) → ( ( 𝐹 ‘ 𝑋 ) ∉ ( 𝐹 “ 𝐶 ) → Fun ◡ ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ) ) )
10 2 9 mpand ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) → ( Fun ◡ ( 𝐹 ↾ 𝐶 ) → ( ( 𝐹 ‘ 𝑋 ) ∉ ( 𝐹 “ 𝐶 ) → Fun ◡ ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ) ) )
11 10 impd ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) → ( ( Fun ◡ ( 𝐹 ↾ 𝐶 ) ∧ ( 𝐹 ‘ 𝑋 ) ∉ ( 𝐹 “ 𝐶 ) ) → Fun ◡ ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ) )
12 simp1 ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) → 𝐹 : 𝐴 ⟶ 𝐵 )
13 simp3 ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) → 𝐶 ⊆ 𝐴 )
14 eldifi ⊢ ( 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) → 𝑋 ∈ 𝐴 )
15 14 snssd ⊢ ( 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) → { 𝑋 } ⊆ 𝐴 )
16 15 3ad2ant2 ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) → { 𝑋 } ⊆ 𝐴 )
17 13 16 unssd ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) → ( 𝐶 ∪ { 𝑋 } ) ⊆ 𝐴 )
18 12 17 fssresd ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) → ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) : ( 𝐶 ∪ { 𝑋 } ) ⟶ 𝐵 )
19 3 simprbi ⊢ ( ( 𝐹 ↾ 𝐶 ) : 𝐶 –1-1→ 𝐵 → Fun ◡ ( 𝐹 ↾ 𝐶 ) )
20 19 anim1i ⊢ ( ( ( 𝐹 ↾ 𝐶 ) : 𝐶 –1-1→ 𝐵 ∧ ( 𝐹 ‘ 𝑋 ) ∉ ( 𝐹 “ 𝐶 ) ) → ( Fun ◡ ( 𝐹 ↾ 𝐶 ) ∧ ( 𝐹 ‘ 𝑋 ) ∉ ( 𝐹 “ 𝐶 ) ) )
21 4 20 biimtrrdi ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) → ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) : ( 𝐶 ∪ { 𝑋 } ) –1-1→ 𝐵 → ( Fun ◡ ( 𝐹 ↾ 𝐶 ) ∧ ( 𝐹 ‘ 𝑋 ) ∉ ( 𝐹 “ 𝐶 ) ) ) )
22 5 21 biimtrrid ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) → ( ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) : ( 𝐶 ∪ { 𝑋 } ) ⟶ 𝐵 ∧ Fun ◡ ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ) → ( Fun ◡ ( 𝐹 ↾ 𝐶 ) ∧ ( 𝐹 ‘ 𝑋 ) ∉ ( 𝐹 “ 𝐶 ) ) ) )
23 18 22 mpand ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) → ( Fun ◡ ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) → ( Fun ◡ ( 𝐹 ↾ 𝐶 ) ∧ ( 𝐹 ‘ 𝑋 ) ∉ ( 𝐹 “ 𝐶 ) ) ) )
24 11 23 impbid ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) → ( ( Fun ◡ ( 𝐹 ↾ 𝐶 ) ∧ ( 𝐹 ‘ 𝑋 ) ∉ ( 𝐹 “ 𝐶 ) ) ↔ Fun ◡ ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ) )