This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem resf1extb

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

Ref Expression
Assertion resf1extb ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) → ( ( ( 𝐹 ↾ 𝐶 ) : 𝐶 –1-1→ 𝐵 ∧ ( 𝐹 ‘ 𝑋 ) ∉ ( 𝐹 “ 𝐶 ) ) ↔ ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) : ( 𝐶 ∪ { 𝑋 } ) –1-1→ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) → 𝐹 : 𝐴 ⟶ 𝐵 )
2 simp3 ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) → 𝐶 ⊆ 𝐴 )
3 eldifi ⊢ ( 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) → 𝑋 ∈ 𝐴 )
4 3 snssd ⊢ ( 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) → { 𝑋 } ⊆ 𝐴 )
5 4 3ad2ant2 ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) → { 𝑋 } ⊆ 𝐴 )
6 2 5 unssd ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) → ( 𝐶 ∪ { 𝑋 } ) ⊆ 𝐴 )
7 1 6 fssresd ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) → ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) : ( 𝐶 ∪ { 𝑋 } ) ⟶ 𝐵 )
8 7 adantr ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ ( ( 𝐹 ↾ 𝐶 ) : 𝐶 –1-1→ 𝐵 ∧ ( 𝐹 ‘ 𝑋 ) ∉ ( 𝐹 “ 𝐶 ) ) ) → ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) : ( 𝐶 ∪ { 𝑋 } ) ⟶ 𝐵 )
9 elun ⊢ ( 𝑦 ∈ ( 𝐶 ∪ { 𝑋 } ) ↔ ( 𝑦 ∈ 𝐶 ∨ 𝑦 ∈ { 𝑋 } ) )
10 elun ⊢ ( 𝑧 ∈ ( 𝐶 ∪ { 𝑋 } ) ↔ ( 𝑧 ∈ 𝐶 ∨ 𝑧 ∈ { 𝑋 } ) )
11 9 10 anbi12i ⊢ ( ( 𝑦 ∈ ( 𝐶 ∪ { 𝑋 } ) ∧ 𝑧 ∈ ( 𝐶 ∪ { 𝑋 } ) ) ↔ ( ( 𝑦 ∈ 𝐶 ∨ 𝑦 ∈ { 𝑋 } ) ∧ ( 𝑧 ∈ 𝐶 ∨ 𝑧 ∈ { 𝑋 } ) ) )
12 dff14a ⊢ ( ( 𝐹 ↾ 𝐶 ) : 𝐶 –1-1→ 𝐵 ↔ ( ( 𝐹 ↾ 𝐶 ) : 𝐶 ⟶ 𝐵 ∧ ∀ 𝑤 ∈ 𝐶 ∀ 𝑥 ∈ 𝐶 ( 𝑤 ≠ 𝑥 → ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑤 ) ≠ ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑥 ) ) ) )
13 neeq1 ⊢ ( 𝑤 = 𝑦 → ( 𝑤 ≠ 𝑥 ↔ 𝑦 ≠ 𝑥 ) )
14 fveq2 ⊢ ( 𝑤 = 𝑦 → ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑤 ) = ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑦 ) )
15 14 neeq1d ⊢ ( 𝑤 = 𝑦 → ( ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑤 ) ≠ ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑥 ) ↔ ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑦 ) ≠ ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑥 ) ) )
16 13 15 imbi12d ⊢ ( 𝑤 = 𝑦 → ( ( 𝑤 ≠ 𝑥 → ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑤 ) ≠ ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑥 ) ) ↔ ( 𝑦 ≠ 𝑥 → ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑦 ) ≠ ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑥 ) ) ) )
17 neeq2 ⊢ ( 𝑥 = 𝑧 → ( 𝑦 ≠ 𝑥 ↔ 𝑦 ≠ 𝑧 ) )
18 fveq2 ⊢ ( 𝑥 = 𝑧 → ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑥 ) = ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑧 ) )
19 18 neeq2d ⊢ ( 𝑥 = 𝑧 → ( ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑦 ) ≠ ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑥 ) ↔ ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑦 ) ≠ ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑧 ) ) )
20 17 19 imbi12d ⊢ ( 𝑥 = 𝑧 → ( ( 𝑦 ≠ 𝑥 → ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑦 ) ≠ ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑥 ) ) ↔ ( 𝑦 ≠ 𝑧 → ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑦 ) ≠ ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑧 ) ) ) )
21 16 20 rspc2v ⊢ ( ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶 ) → ( ∀ 𝑤 ∈ 𝐶 ∀ 𝑥 ∈ 𝐶 ( 𝑤 ≠ 𝑥 → ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑤 ) ≠ ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑥 ) ) → ( 𝑦 ≠ 𝑧 → ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑦 ) ≠ ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑧 ) ) ) )
22 simpl ⊢ ( ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶 ) → 𝑦 ∈ 𝐶 )
23 22 fvresd ⊢ ( ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶 ) → ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
24 simpr ⊢ ( ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶 ) → 𝑧 ∈ 𝐶 )
25 24 fvresd ⊢ ( ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶 ) → ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑧 ) = ( 𝐹 ‘ 𝑧 ) )
26 23 25 neeq12d ⊢ ( ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶 ) → ( ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑦 ) ≠ ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑧 ) ↔ ( 𝐹 ‘ 𝑦 ) ≠ ( 𝐹 ‘ 𝑧 ) ) )
27 26 imbi2d ⊢ ( ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶 ) → ( ( 𝑦 ≠ 𝑧 → ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑦 ) ≠ ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑧 ) ) ↔ ( 𝑦 ≠ 𝑧 → ( 𝐹 ‘ 𝑦 ) ≠ ( 𝐹 ‘ 𝑧 ) ) ) )
28 27 bi23imp13 ⊢ ( ( ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶 ) ∧ ( 𝑦 ≠ 𝑧 → ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑦 ) ≠ ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑧 ) ) ∧ 𝑦 ≠ 𝑧 ) → ( 𝐹 ‘ 𝑦 ) ≠ ( 𝐹 ‘ 𝑧 ) )
29 elun1 ⊢ ( 𝑦 ∈ 𝐶 → 𝑦 ∈ ( 𝐶 ∪ { 𝑋 } ) )
30 29 adantr ⊢ ( ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶 ) → 𝑦 ∈ ( 𝐶 ∪ { 𝑋 } ) )
31 30 fvresd ⊢ ( ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶 ) → ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
32 elun1 ⊢ ( 𝑧 ∈ 𝐶 → 𝑧 ∈ ( 𝐶 ∪ { 𝑋 } ) )
33 32 adantl ⊢ ( ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶 ) → 𝑧 ∈ ( 𝐶 ∪ { 𝑋 } ) )
34 33 fvresd ⊢ ( ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶 ) → ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑧 ) = ( 𝐹 ‘ 𝑧 ) )
35 31 34 neeq12d ⊢ ( ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶 ) → ( ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑦 ) ≠ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑧 ) ↔ ( 𝐹 ‘ 𝑦 ) ≠ ( 𝐹 ‘ 𝑧 ) ) )
36 35 3ad2ant1 ⊢ ( ( ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶 ) ∧ ( 𝑦 ≠ 𝑧 → ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑦 ) ≠ ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑧 ) ) ∧ 𝑦 ≠ 𝑧 ) → ( ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑦 ) ≠ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑧 ) ↔ ( 𝐹 ‘ 𝑦 ) ≠ ( 𝐹 ‘ 𝑧 ) ) )
37 28 36 mpbird ⊢ ( ( ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶 ) ∧ ( 𝑦 ≠ 𝑧 → ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑦 ) ≠ ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑧 ) ) ∧ 𝑦 ≠ 𝑧 ) → ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑦 ) ≠ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑧 ) )
38 37 3exp ⊢ ( ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶 ) → ( ( 𝑦 ≠ 𝑧 → ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑦 ) ≠ ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑧 ) ) → ( 𝑦 ≠ 𝑧 → ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑦 ) ≠ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑧 ) ) ) )
39 21 38 syldc ⊢ ( ∀ 𝑤 ∈ 𝐶 ∀ 𝑥 ∈ 𝐶 ( 𝑤 ≠ 𝑥 → ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑤 ) ≠ ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑥 ) ) → ( ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶 ) → ( 𝑦 ≠ 𝑧 → ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑦 ) ≠ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑧 ) ) ) )
40 39 adantl ⊢ ( ( ( 𝐹 ↾ 𝐶 ) : 𝐶 ⟶ 𝐵 ∧ ∀ 𝑤 ∈ 𝐶 ∀ 𝑥 ∈ 𝐶 ( 𝑤 ≠ 𝑥 → ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑤 ) ≠ ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑥 ) ) ) → ( ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶 ) → ( 𝑦 ≠ 𝑧 → ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑦 ) ≠ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑧 ) ) ) )
41 40 a1i ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) → ( ( ( 𝐹 ↾ 𝐶 ) : 𝐶 ⟶ 𝐵 ∧ ∀ 𝑤 ∈ 𝐶 ∀ 𝑥 ∈ 𝐶 ( 𝑤 ≠ 𝑥 → ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑤 ) ≠ ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑥 ) ) ) → ( ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶 ) → ( 𝑦 ≠ 𝑧 → ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑦 ) ≠ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑧 ) ) ) ) )
42 12 41 biimtrid ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) → ( ( 𝐹 ↾ 𝐶 ) : 𝐶 –1-1→ 𝐵 → ( ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶 ) → ( 𝑦 ≠ 𝑧 → ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑦 ) ≠ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑧 ) ) ) ) )
43 42 a1dd ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) → ( ( 𝐹 ↾ 𝐶 ) : 𝐶 –1-1→ 𝐵 → ( ( 𝐹 ‘ 𝑋 ) ∉ ( 𝐹 “ 𝐶 ) → ( ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶 ) → ( 𝑦 ≠ 𝑧 → ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑦 ) ≠ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑧 ) ) ) ) ) )
44 43 imp32 ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ ( ( 𝐹 ↾ 𝐶 ) : 𝐶 –1-1→ 𝐵 ∧ ( 𝐹 ‘ 𝑋 ) ∉ ( 𝐹 “ 𝐶 ) ) ) → ( ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶 ) → ( 𝑦 ≠ 𝑧 → ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑦 ) ≠ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑧 ) ) ) )
45 ffn ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 Fn 𝐴 )
46 45 3ad2ant1 ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) → 𝐹 Fn 𝐴 )
47 46 2 fvelimabd ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) → ( ( 𝐹 ‘ 𝑋 ) ∈ ( 𝐹 “ 𝐶 ) ↔ ∃ 𝑥 ∈ 𝐶 ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) ) )
48 47 notbid ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) → ( ¬ ( 𝐹 ‘ 𝑋 ) ∈ ( 𝐹 “ 𝐶 ) ↔ ¬ ∃ 𝑥 ∈ 𝐶 ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) ) )
49 df-nel ⊢ ( ( 𝐹 ‘ 𝑋 ) ∉ ( 𝐹 “ 𝐶 ) ↔ ¬ ( 𝐹 ‘ 𝑋 ) ∈ ( 𝐹 “ 𝐶 ) )
50 ralnex ⊢ ( ∀ 𝑥 ∈ 𝐶 ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) ↔ ¬ ∃ 𝑥 ∈ 𝐶 ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) )
51 48 49 50 3bitr4g ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) → ( ( 𝐹 ‘ 𝑋 ) ∉ ( 𝐹 “ 𝐶 ) ↔ ∀ 𝑥 ∈ 𝐶 ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) ) )
52 df-ne ⊢ ( ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑋 ) ↔ ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) )
53 fveq2 ⊢ ( 𝑥 = 𝑧 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑧 ) )
54 53 neeq1d ⊢ ( 𝑥 = 𝑧 → ( ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑋 ) ↔ ( 𝐹 ‘ 𝑧 ) ≠ ( 𝐹 ‘ 𝑋 ) ) )
55 52 54 bitr3id ⊢ ( 𝑥 = 𝑧 → ( ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) ↔ ( 𝐹 ‘ 𝑧 ) ≠ ( 𝐹 ‘ 𝑋 ) ) )
56 55 rspcv ⊢ ( 𝑧 ∈ 𝐶 → ( ∀ 𝑥 ∈ 𝐶 ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) → ( 𝐹 ‘ 𝑧 ) ≠ ( 𝐹 ‘ 𝑋 ) ) )
57 56 ad2antll ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ { 𝑋 } ∧ 𝑧 ∈ 𝐶 ) ) → ( ∀ 𝑥 ∈ 𝐶 ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) → ( 𝐹 ‘ 𝑧 ) ≠ ( 𝐹 ‘ 𝑋 ) ) )
58 32 ad2antll ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ { 𝑋 } ∧ 𝑧 ∈ 𝐶 ) ) → 𝑧 ∈ ( 𝐶 ∪ { 𝑋 } ) )
59 58 fvresd ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ { 𝑋 } ∧ 𝑧 ∈ 𝐶 ) ) → ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑧 ) = ( 𝐹 ‘ 𝑧 ) )
60 59 eqcomd ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ { 𝑋 } ∧ 𝑧 ∈ 𝐶 ) ) → ( 𝐹 ‘ 𝑧 ) = ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑧 ) )
61 elsni ⊢ ( 𝑦 ∈ { 𝑋 } → 𝑦 = 𝑋 )
62 61 eqcomd ⊢ ( 𝑦 ∈ { 𝑋 } → 𝑋 = 𝑦 )
63 62 ad2antrl ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ { 𝑋 } ∧ 𝑧 ∈ 𝐶 ) ) → 𝑋 = 𝑦 )
64 63 fveq2d ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ { 𝑋 } ∧ 𝑧 ∈ 𝐶 ) ) → ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑦 ) )
65 elun2 ⊢ ( 𝑦 ∈ { 𝑋 } → 𝑦 ∈ ( 𝐶 ∪ { 𝑋 } ) )
66 65 ad2antrl ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ { 𝑋 } ∧ 𝑧 ∈ 𝐶 ) ) → 𝑦 ∈ ( 𝐶 ∪ { 𝑋 } ) )
67 66 fvresd ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ { 𝑋 } ∧ 𝑧 ∈ 𝐶 ) ) → ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
68 64 67 eqtr4d ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ { 𝑋 } ∧ 𝑧 ∈ 𝐶 ) ) → ( 𝐹 ‘ 𝑋 ) = ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑦 ) )
69 60 68 neeq12d ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ { 𝑋 } ∧ 𝑧 ∈ 𝐶 ) ) → ( ( 𝐹 ‘ 𝑧 ) ≠ ( 𝐹 ‘ 𝑋 ) ↔ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑧 ) ≠ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑦 ) ) )
70 69 biimpa ⊢ ( ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ { 𝑋 } ∧ 𝑧 ∈ 𝐶 ) ) ∧ ( 𝐹 ‘ 𝑧 ) ≠ ( 𝐹 ‘ 𝑋 ) ) → ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑧 ) ≠ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑦 ) )
71 70 necomd ⊢ ( ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ { 𝑋 } ∧ 𝑧 ∈ 𝐶 ) ) ∧ ( 𝐹 ‘ 𝑧 ) ≠ ( 𝐹 ‘ 𝑋 ) ) → ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑦 ) ≠ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑧 ) )
72 71 a1d ⊢ ( ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ { 𝑋 } ∧ 𝑧 ∈ 𝐶 ) ) ∧ ( 𝐹 ‘ 𝑧 ) ≠ ( 𝐹 ‘ 𝑋 ) ) → ( 𝑦 ≠ 𝑧 → ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑦 ) ≠ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑧 ) ) )
73 72 ex ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ { 𝑋 } ∧ 𝑧 ∈ 𝐶 ) ) → ( ( 𝐹 ‘ 𝑧 ) ≠ ( 𝐹 ‘ 𝑋 ) → ( 𝑦 ≠ 𝑧 → ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑦 ) ≠ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑧 ) ) ) )
74 57 73 syld ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ { 𝑋 } ∧ 𝑧 ∈ 𝐶 ) ) → ( ∀ 𝑥 ∈ 𝐶 ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) → ( 𝑦 ≠ 𝑧 → ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑦 ) ≠ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑧 ) ) ) )
75 74 a1d ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ { 𝑋 } ∧ 𝑧 ∈ 𝐶 ) ) → ( ( 𝐹 ↾ 𝐶 ) : 𝐶 –1-1→ 𝐵 → ( ∀ 𝑥 ∈ 𝐶 ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) → ( 𝑦 ≠ 𝑧 → ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑦 ) ≠ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑧 ) ) ) ) )
76 75 ex ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) → ( ( 𝑦 ∈ { 𝑋 } ∧ 𝑧 ∈ 𝐶 ) → ( ( 𝐹 ↾ 𝐶 ) : 𝐶 –1-1→ 𝐵 → ( ∀ 𝑥 ∈ 𝐶 ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) → ( 𝑦 ≠ 𝑧 → ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑦 ) ≠ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑧 ) ) ) ) ) )
77 76 com24 ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) → ( ∀ 𝑥 ∈ 𝐶 ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) → ( ( 𝐹 ↾ 𝐶 ) : 𝐶 –1-1→ 𝐵 → ( ( 𝑦 ∈ { 𝑋 } ∧ 𝑧 ∈ 𝐶 ) → ( 𝑦 ≠ 𝑧 → ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑦 ) ≠ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑧 ) ) ) ) ) )
78 51 77 sylbid ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) → ( ( 𝐹 ‘ 𝑋 ) ∉ ( 𝐹 “ 𝐶 ) → ( ( 𝐹 ↾ 𝐶 ) : 𝐶 –1-1→ 𝐵 → ( ( 𝑦 ∈ { 𝑋 } ∧ 𝑧 ∈ 𝐶 ) → ( 𝑦 ≠ 𝑧 → ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑦 ) ≠ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑧 ) ) ) ) ) )
79 78 impcomd ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) → ( ( ( 𝐹 ↾ 𝐶 ) : 𝐶 –1-1→ 𝐵 ∧ ( 𝐹 ‘ 𝑋 ) ∉ ( 𝐹 “ 𝐶 ) ) → ( ( 𝑦 ∈ { 𝑋 } ∧ 𝑧 ∈ 𝐶 ) → ( 𝑦 ≠ 𝑧 → ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑦 ) ≠ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑧 ) ) ) ) )
80 79 imp ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ ( ( 𝐹 ↾ 𝐶 ) : 𝐶 –1-1→ 𝐵 ∧ ( 𝐹 ‘ 𝑋 ) ∉ ( 𝐹 “ 𝐶 ) ) ) → ( ( 𝑦 ∈ { 𝑋 } ∧ 𝑧 ∈ 𝐶 ) → ( 𝑦 ≠ 𝑧 → ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑦 ) ≠ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑧 ) ) ) )
81 fveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) )
82 81 neeq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑋 ) ↔ ( 𝐹 ‘ 𝑦 ) ≠ ( 𝐹 ‘ 𝑋 ) ) )
83 52 82 bitr3id ⊢ ( 𝑥 = 𝑦 → ( ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) ↔ ( 𝐹 ‘ 𝑦 ) ≠ ( 𝐹 ‘ 𝑋 ) ) )
84 83 rspcv ⊢ ( 𝑦 ∈ 𝐶 → ( ∀ 𝑥 ∈ 𝐶 ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) → ( 𝐹 ‘ 𝑦 ) ≠ ( 𝐹 ‘ 𝑋 ) ) )
85 84 ad2antrl ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ { 𝑋 } ) ) → ( ∀ 𝑥 ∈ 𝐶 ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) → ( 𝐹 ‘ 𝑦 ) ≠ ( 𝐹 ‘ 𝑋 ) ) )
86 29 ad2antrl ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ { 𝑋 } ) ) → 𝑦 ∈ ( 𝐶 ∪ { 𝑋 } ) )
87 86 fvresd ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ { 𝑋 } ) ) → ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
88 87 eqcomd ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ { 𝑋 } ) ) → ( 𝐹 ‘ 𝑦 ) = ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑦 ) )
89 elsni ⊢ ( 𝑧 ∈ { 𝑋 } → 𝑧 = 𝑋 )
90 89 eqcomd ⊢ ( 𝑧 ∈ { 𝑋 } → 𝑋 = 𝑧 )
91 90 ad2antll ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ { 𝑋 } ) ) → 𝑋 = 𝑧 )
92 91 fveq2d ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ { 𝑋 } ) ) → ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑧 ) )
93 elun2 ⊢ ( 𝑧 ∈ { 𝑋 } → 𝑧 ∈ ( 𝐶 ∪ { 𝑋 } ) )
94 93 ad2antll ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ { 𝑋 } ) ) → 𝑧 ∈ ( 𝐶 ∪ { 𝑋 } ) )
95 94 fvresd ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ { 𝑋 } ) ) → ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑧 ) = ( 𝐹 ‘ 𝑧 ) )
96 92 95 eqtr4d ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ { 𝑋 } ) ) → ( 𝐹 ‘ 𝑋 ) = ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑧 ) )
97 88 96 neeq12d ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ { 𝑋 } ) ) → ( ( 𝐹 ‘ 𝑦 ) ≠ ( 𝐹 ‘ 𝑋 ) ↔ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑦 ) ≠ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑧 ) ) )
98 97 biimpd ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ { 𝑋 } ) ) → ( ( 𝐹 ‘ 𝑦 ) ≠ ( 𝐹 ‘ 𝑋 ) → ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑦 ) ≠ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑧 ) ) )
99 98 a1dd ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ { 𝑋 } ) ) → ( ( 𝐹 ‘ 𝑦 ) ≠ ( 𝐹 ‘ 𝑋 ) → ( 𝑦 ≠ 𝑧 → ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑦 ) ≠ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑧 ) ) ) )
100 85 99 syld ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ { 𝑋 } ) ) → ( ∀ 𝑥 ∈ 𝐶 ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) → ( 𝑦 ≠ 𝑧 → ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑦 ) ≠ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑧 ) ) ) )
101 100 a1d ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ { 𝑋 } ) ) → ( ( 𝐹 ↾ 𝐶 ) : 𝐶 –1-1→ 𝐵 → ( ∀ 𝑥 ∈ 𝐶 ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) → ( 𝑦 ≠ 𝑧 → ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑦 ) ≠ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑧 ) ) ) ) )
102 101 ex ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) → ( ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ { 𝑋 } ) → ( ( 𝐹 ↾ 𝐶 ) : 𝐶 –1-1→ 𝐵 → ( ∀ 𝑥 ∈ 𝐶 ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) → ( 𝑦 ≠ 𝑧 → ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑦 ) ≠ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑧 ) ) ) ) ) )
103 102 com24 ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) → ( ∀ 𝑥 ∈ 𝐶 ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) → ( ( 𝐹 ↾ 𝐶 ) : 𝐶 –1-1→ 𝐵 → ( ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ { 𝑋 } ) → ( 𝑦 ≠ 𝑧 → ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑦 ) ≠ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑧 ) ) ) ) ) )
104 51 103 sylbid ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) → ( ( 𝐹 ‘ 𝑋 ) ∉ ( 𝐹 “ 𝐶 ) → ( ( 𝐹 ↾ 𝐶 ) : 𝐶 –1-1→ 𝐵 → ( ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ { 𝑋 } ) → ( 𝑦 ≠ 𝑧 → ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑦 ) ≠ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑧 ) ) ) ) ) )
105 104 impcomd ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) → ( ( ( 𝐹 ↾ 𝐶 ) : 𝐶 –1-1→ 𝐵 ∧ ( 𝐹 ‘ 𝑋 ) ∉ ( 𝐹 “ 𝐶 ) ) → ( ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ { 𝑋 } ) → ( 𝑦 ≠ 𝑧 → ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑦 ) ≠ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑧 ) ) ) ) )
106 105 imp ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ ( ( 𝐹 ↾ 𝐶 ) : 𝐶 –1-1→ 𝐵 ∧ ( 𝐹 ‘ 𝑋 ) ∉ ( 𝐹 “ 𝐶 ) ) ) → ( ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ { 𝑋 } ) → ( 𝑦 ≠ 𝑧 → ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑦 ) ≠ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑧 ) ) ) )
107 velsn ⊢ ( 𝑦 ∈ { 𝑋 } ↔ 𝑦 = 𝑋 )
108 velsn ⊢ ( 𝑧 ∈ { 𝑋 } ↔ 𝑧 = 𝑋 )
109 eqtr3 ⊢ ( ( 𝑦 = 𝑋 ∧ 𝑧 = 𝑋 ) → 𝑦 = 𝑧 )
110 eqneqall ⊢ ( 𝑦 = 𝑧 → ( 𝑦 ≠ 𝑧 → ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑦 ) ≠ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑧 ) ) )
111 109 110 syl ⊢ ( ( 𝑦 = 𝑋 ∧ 𝑧 = 𝑋 ) → ( 𝑦 ≠ 𝑧 → ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑦 ) ≠ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑧 ) ) )
112 107 108 111 syl2anb ⊢ ( ( 𝑦 ∈ { 𝑋 } ∧ 𝑧 ∈ { 𝑋 } ) → ( 𝑦 ≠ 𝑧 → ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑦 ) ≠ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑧 ) ) )
113 112 a1i ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ ( ( 𝐹 ↾ 𝐶 ) : 𝐶 –1-1→ 𝐵 ∧ ( 𝐹 ‘ 𝑋 ) ∉ ( 𝐹 “ 𝐶 ) ) ) → ( ( 𝑦 ∈ { 𝑋 } ∧ 𝑧 ∈ { 𝑋 } ) → ( 𝑦 ≠ 𝑧 → ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑦 ) ≠ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑧 ) ) ) )
114 44 80 106 113 ccased ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ ( ( 𝐹 ↾ 𝐶 ) : 𝐶 –1-1→ 𝐵 ∧ ( 𝐹 ‘ 𝑋 ) ∉ ( 𝐹 “ 𝐶 ) ) ) → ( ( ( 𝑦 ∈ 𝐶 ∨ 𝑦 ∈ { 𝑋 } ) ∧ ( 𝑧 ∈ 𝐶 ∨ 𝑧 ∈ { 𝑋 } ) ) → ( 𝑦 ≠ 𝑧 → ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑦 ) ≠ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑧 ) ) ) )
115 11 114 biimtrid ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ ( ( 𝐹 ↾ 𝐶 ) : 𝐶 –1-1→ 𝐵 ∧ ( 𝐹 ‘ 𝑋 ) ∉ ( 𝐹 “ 𝐶 ) ) ) → ( ( 𝑦 ∈ ( 𝐶 ∪ { 𝑋 } ) ∧ 𝑧 ∈ ( 𝐶 ∪ { 𝑋 } ) ) → ( 𝑦 ≠ 𝑧 → ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑦 ) ≠ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑧 ) ) ) )
116 115 ralrimivv ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ ( ( 𝐹 ↾ 𝐶 ) : 𝐶 –1-1→ 𝐵 ∧ ( 𝐹 ‘ 𝑋 ) ∉ ( 𝐹 “ 𝐶 ) ) ) → ∀ 𝑦 ∈ ( 𝐶 ∪ { 𝑋 } ) ∀ 𝑧 ∈ ( 𝐶 ∪ { 𝑋 } ) ( 𝑦 ≠ 𝑧 → ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑦 ) ≠ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑧 ) ) )
117 dff14a ⊢ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) : ( 𝐶 ∪ { 𝑋 } ) –1-1→ 𝐵 ↔ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) : ( 𝐶 ∪ { 𝑋 } ) ⟶ 𝐵 ∧ ∀ 𝑦 ∈ ( 𝐶 ∪ { 𝑋 } ) ∀ 𝑧 ∈ ( 𝐶 ∪ { 𝑋 } ) ( 𝑦 ≠ 𝑧 → ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑦 ) ≠ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑧 ) ) ) )
118 8 116 117 sylanbrc ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ ( ( 𝐹 ↾ 𝐶 ) : 𝐶 –1-1→ 𝐵 ∧ ( 𝐹 ‘ 𝑋 ) ∉ ( 𝐹 “ 𝐶 ) ) ) → ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) : ( 𝐶 ∪ { 𝑋 } ) –1-1→ 𝐵 )
119 fssres ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐶 ⊆ 𝐴 ) → ( 𝐹 ↾ 𝐶 ) : 𝐶 ⟶ 𝐵 )
120 119 3adant2 ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) → ( 𝐹 ↾ 𝐶 ) : 𝐶 ⟶ 𝐵 )
121 120 adantr ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) : ( 𝐶 ∪ { 𝑋 } ) –1-1→ 𝐵 ) → ( 𝐹 ↾ 𝐶 ) : 𝐶 ⟶ 𝐵 )
122 df-f1 ⊢ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) : ( 𝐶 ∪ { 𝑋 } ) –1-1→ 𝐵 ↔ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) : ( 𝐶 ∪ { 𝑋 } ) ⟶ 𝐵 ∧ Fun ◡ ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ) )
123 funres11 ⊢ ( Fun ◡ ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) → Fun ◡ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ↾ 𝐶 ) )
124 122 123 simplbiim ⊢ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) : ( 𝐶 ∪ { 𝑋 } ) –1-1→ 𝐵 → Fun ◡ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ↾ 𝐶 ) )
125 124 adantl ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) : ( 𝐶 ∪ { 𝑋 } ) –1-1→ 𝐵 ) → Fun ◡ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ↾ 𝐶 ) )
126 ssun1 ⊢ 𝐶 ⊆ ( 𝐶 ∪ { 𝑋 } )
127 126 resabs1i ⊢ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ↾ 𝐶 ) = ( 𝐹 ↾ 𝐶 )
128 127 eqcomi ⊢ ( 𝐹 ↾ 𝐶 ) = ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ↾ 𝐶 )
129 128 cnveqi ⊢ ◡ ( 𝐹 ↾ 𝐶 ) = ◡ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ↾ 𝐶 )
130 129 funeqi ⊢ ( Fun ◡ ( 𝐹 ↾ 𝐶 ) ↔ Fun ◡ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ↾ 𝐶 ) )
131 125 130 sylibr ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) : ( 𝐶 ∪ { 𝑋 } ) –1-1→ 𝐵 ) → Fun ◡ ( 𝐹 ↾ 𝐶 ) )
132 df-f1 ⊢ ( ( 𝐹 ↾ 𝐶 ) : 𝐶 –1-1→ 𝐵 ↔ ( ( 𝐹 ↾ 𝐶 ) : 𝐶 ⟶ 𝐵 ∧ Fun ◡ ( 𝐹 ↾ 𝐶 ) ) )
133 121 131 132 sylanbrc ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) : ( 𝐶 ∪ { 𝑋 } ) –1-1→ 𝐵 ) → ( 𝐹 ↾ 𝐶 ) : 𝐶 –1-1→ 𝐵 )
134 elun1 ⊢ ( 𝑥 ∈ 𝐶 → 𝑥 ∈ ( 𝐶 ∪ { 𝑋 } ) )
135 snidg ⊢ ( 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) → 𝑋 ∈ { 𝑋 } )
136 135 3ad2ant2 ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) → 𝑋 ∈ { 𝑋 } )
137 elun2 ⊢ ( 𝑋 ∈ { 𝑋 } → 𝑋 ∈ ( 𝐶 ∪ { 𝑋 } ) )
138 136 137 syl ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) → 𝑋 ∈ ( 𝐶 ∪ { 𝑋 } ) )
139 neeq1 ⊢ ( 𝑦 = 𝑥 → ( 𝑦 ≠ 𝑧 ↔ 𝑥 ≠ 𝑧 ) )
140 fveq2 ⊢ ( 𝑦 = 𝑥 → ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑦 ) = ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑥 ) )
141 140 neeq1d ⊢ ( 𝑦 = 𝑥 → ( ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑦 ) ≠ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑧 ) ↔ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑥 ) ≠ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑧 ) ) )
142 139 141 imbi12d ⊢ ( 𝑦 = 𝑥 → ( ( 𝑦 ≠ 𝑧 → ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑦 ) ≠ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑧 ) ) ↔ ( 𝑥 ≠ 𝑧 → ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑥 ) ≠ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑧 ) ) ) )
143 neeq2 ⊢ ( 𝑧 = 𝑋 → ( 𝑥 ≠ 𝑧 ↔ 𝑥 ≠ 𝑋 ) )
144 fveq2 ⊢ ( 𝑧 = 𝑋 → ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑧 ) = ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑋 ) )
145 144 neeq2d ⊢ ( 𝑧 = 𝑋 → ( ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑥 ) ≠ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑧 ) ↔ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑥 ) ≠ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑋 ) ) )
146 143 145 imbi12d ⊢ ( 𝑧 = 𝑋 → ( ( 𝑥 ≠ 𝑧 → ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑥 ) ≠ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑧 ) ) ↔ ( 𝑥 ≠ 𝑋 → ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑥 ) ≠ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑋 ) ) ) )
147 142 146 rspc2v ⊢ ( ( 𝑥 ∈ ( 𝐶 ∪ { 𝑋 } ) ∧ 𝑋 ∈ ( 𝐶 ∪ { 𝑋 } ) ) → ( ∀ 𝑦 ∈ ( 𝐶 ∪ { 𝑋 } ) ∀ 𝑧 ∈ ( 𝐶 ∪ { 𝑋 } ) ( 𝑦 ≠ 𝑧 → ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑦 ) ≠ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑧 ) ) → ( 𝑥 ≠ 𝑋 → ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑥 ) ≠ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑋 ) ) ) )
148 134 138 147 syl2anr ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ 𝑥 ∈ 𝐶 ) → ( ∀ 𝑦 ∈ ( 𝐶 ∪ { 𝑋 } ) ∀ 𝑧 ∈ ( 𝐶 ∪ { 𝑋 } ) ( 𝑦 ≠ 𝑧 → ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑦 ) ≠ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑧 ) ) → ( 𝑥 ≠ 𝑋 → ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑥 ) ≠ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑋 ) ) ) )
149 148 adantr ⊢ ( ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ 𝑥 ∈ 𝐶 ) ∧ ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) : ( 𝐶 ∪ { 𝑋 } ) ⟶ 𝐵 ) → ( ∀ 𝑦 ∈ ( 𝐶 ∪ { 𝑋 } ) ∀ 𝑧 ∈ ( 𝐶 ∪ { 𝑋 } ) ( 𝑦 ≠ 𝑧 → ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑦 ) ≠ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑧 ) ) → ( 𝑥 ≠ 𝑋 → ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑥 ) ≠ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑋 ) ) ) )
150 eldifn ⊢ ( 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) → ¬ 𝑋 ∈ 𝐶 )
151 nelelne ⊢ ( ¬ 𝑋 ∈ 𝐶 → ( 𝑥 ∈ 𝐶 → 𝑥 ≠ 𝑋 ) )
152 150 151 syl ⊢ ( 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) → ( 𝑥 ∈ 𝐶 → 𝑥 ≠ 𝑋 ) )
153 152 3ad2ant2 ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) → ( 𝑥 ∈ 𝐶 → 𝑥 ≠ 𝑋 ) )
154 153 imp ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ 𝑥 ∈ 𝐶 ) → 𝑥 ≠ 𝑋 )
155 154 adantr ⊢ ( ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ 𝑥 ∈ 𝐶 ) ∧ ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) : ( 𝐶 ∪ { 𝑋 } ) ⟶ 𝐵 ) → 𝑥 ≠ 𝑋 )
156 pm2.27 ⊢ ( 𝑥 ≠ 𝑋 → ( ( 𝑥 ≠ 𝑋 → ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑥 ) ≠ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑋 ) ) → ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑥 ) ≠ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑋 ) ) )
157 155 156 syl ⊢ ( ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ 𝑥 ∈ 𝐶 ) ∧ ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) : ( 𝐶 ∪ { 𝑋 } ) ⟶ 𝐵 ) → ( ( 𝑥 ≠ 𝑋 → ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑥 ) ≠ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑋 ) ) → ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑥 ) ≠ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑋 ) ) )
158 134 adantl ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ 𝑥 ∈ 𝐶 ) → 𝑥 ∈ ( 𝐶 ∪ { 𝑋 } ) )
159 158 adantr ⊢ ( ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ 𝑥 ∈ 𝐶 ) ∧ ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) : ( 𝐶 ∪ { 𝑋 } ) ⟶ 𝐵 ) → 𝑥 ∈ ( 𝐶 ∪ { 𝑋 } ) )
160 159 fvresd ⊢ ( ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ 𝑥 ∈ 𝐶 ) ∧ ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) : ( 𝐶 ∪ { 𝑋 } ) ⟶ 𝐵 ) → ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
161 135 137 syl ⊢ ( 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) → 𝑋 ∈ ( 𝐶 ∪ { 𝑋 } ) )
162 161 3ad2ant2 ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) → 𝑋 ∈ ( 𝐶 ∪ { 𝑋 } ) )
163 162 adantr ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ 𝑥 ∈ 𝐶 ) → 𝑋 ∈ ( 𝐶 ∪ { 𝑋 } ) )
164 163 fvresd ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ 𝑥 ∈ 𝐶 ) → ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑋 ) = ( 𝐹 ‘ 𝑋 ) )
165 164 adantr ⊢ ( ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ 𝑥 ∈ 𝐶 ) ∧ ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) : ( 𝐶 ∪ { 𝑋 } ) ⟶ 𝐵 ) → ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑋 ) = ( 𝐹 ‘ 𝑋 ) )
166 160 165 neeq12d ⊢ ( ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ 𝑥 ∈ 𝐶 ) ∧ ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) : ( 𝐶 ∪ { 𝑋 } ) ⟶ 𝐵 ) → ( ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑥 ) ≠ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑋 ) ↔ ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑋 ) ) )
167 157 166 sylibd ⊢ ( ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ 𝑥 ∈ 𝐶 ) ∧ ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) : ( 𝐶 ∪ { 𝑋 } ) ⟶ 𝐵 ) → ( ( 𝑥 ≠ 𝑋 → ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑥 ) ≠ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑋 ) ) → ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑋 ) ) )
168 149 167 syld ⊢ ( ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ 𝑥 ∈ 𝐶 ) ∧ ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) : ( 𝐶 ∪ { 𝑋 } ) ⟶ 𝐵 ) → ( ∀ 𝑦 ∈ ( 𝐶 ∪ { 𝑋 } ) ∀ 𝑧 ∈ ( 𝐶 ∪ { 𝑋 } ) ( 𝑦 ≠ 𝑧 → ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑦 ) ≠ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑧 ) ) → ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑋 ) ) )
169 168 expimpd ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ 𝑥 ∈ 𝐶 ) → ( ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) : ( 𝐶 ∪ { 𝑋 } ) ⟶ 𝐵 ∧ ∀ 𝑦 ∈ ( 𝐶 ∪ { 𝑋 } ) ∀ 𝑧 ∈ ( 𝐶 ∪ { 𝑋 } ) ( 𝑦 ≠ 𝑧 → ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑦 ) ≠ ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) ‘ 𝑧 ) ) ) → ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑋 ) ) )
170 117 169 biimtrid ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ 𝑥 ∈ 𝐶 ) → ( ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) : ( 𝐶 ∪ { 𝑋 } ) –1-1→ 𝐵 → ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑋 ) ) )
171 170 impancom ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) : ( 𝐶 ∪ { 𝑋 } ) –1-1→ 𝐵 ) → ( 𝑥 ∈ 𝐶 → ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑋 ) ) )
172 171 imp ⊢ ( ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) : ( 𝐶 ∪ { 𝑋 } ) –1-1→ 𝐵 ) ∧ 𝑥 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑋 ) )
173 172 neneqd ⊢ ( ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) : ( 𝐶 ∪ { 𝑋 } ) –1-1→ 𝐵 ) ∧ 𝑥 ∈ 𝐶 ) → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) )
174 173 ralrimiva ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) : ( 𝐶 ∪ { 𝑋 } ) –1-1→ 𝐵 ) → ∀ 𝑥 ∈ 𝐶 ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) )
175 51 adantr ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) : ( 𝐶 ∪ { 𝑋 } ) –1-1→ 𝐵 ) → ( ( 𝐹 ‘ 𝑋 ) ∉ ( 𝐹 “ 𝐶 ) ↔ ∀ 𝑥 ∈ 𝐶 ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) ) )
176 174 175 mpbird ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) : ( 𝐶 ∪ { 𝑋 } ) –1-1→ 𝐵 ) → ( 𝐹 ‘ 𝑋 ) ∉ ( 𝐹 “ 𝐶 ) )
177 133 176 jca ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) : ( 𝐶 ∪ { 𝑋 } ) –1-1→ 𝐵 ) → ( ( 𝐹 ↾ 𝐶 ) : 𝐶 –1-1→ 𝐵 ∧ ( 𝐹 ‘ 𝑋 ) ∉ ( 𝐹 “ 𝐶 ) ) )
178 118 177 impbida ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝐶 ⊆ 𝐴 ) → ( ( ( 𝐹 ↾ 𝐶 ) : 𝐶 –1-1→ 𝐵 ∧ ( 𝐹 ‘ 𝑋 ) ∉ ( 𝐹 “ 𝐶 ) ) ↔ ( 𝐹 ↾ ( 𝐶 ∪ { 𝑋 } ) ) : ( 𝐶 ∪ { 𝑋 } ) –1-1→ 𝐵 ) )