Metamath Proof Explorer

Theorem f1resrcmplf1d

Description: If a function's restriction to a subclass of its domain and its restriction to the relative complement of that subclass are both one-to-one, and if the ranges of those two restrictions are disjoint, then the function is itself one-to-one. (Contributed by BTernaryTau, 28-Sep-2023)

Ref Expression
Hypotheses f1resrcmplf1d.1 ⊢ ( 𝜑 → 𝐶 ⊆ 𝐴 )
f1resrcmplf1d.2 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
f1resrcmplf1d.3 ⊢ ( 𝜑 → ( 𝐹 ↾ 𝐶 ) : 𝐶 –1-1→ 𝐵 )
f1resrcmplf1d.4 ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐴 ∖ 𝐶 ) ) : ( 𝐴 ∖ 𝐶 ) –1-1→ 𝐵 )
f1resrcmplf1d.5 ⊢ ( 𝜑 → ( ( 𝐹 “ 𝐶 ) ∩ ( 𝐹 “ ( 𝐴 ∖ 𝐶 ) ) ) = ∅ )
Assertion f1resrcmplf1d ( 𝜑 → 𝐹 : 𝐴 –1-1→ 𝐵 )

Proof

Step Hyp Ref Expression
1 f1resrcmplf1d.1 ⊢ ( 𝜑 → 𝐶 ⊆ 𝐴 )
2 f1resrcmplf1d.2 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
3 f1resrcmplf1d.3 ⊢ ( 𝜑 → ( 𝐹 ↾ 𝐶 ) : 𝐶 –1-1→ 𝐵 )
4 f1resrcmplf1d.4 ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐴 ∖ 𝐶 ) ) : ( 𝐴 ∖ 𝐶 ) –1-1→ 𝐵 )
5 f1resrcmplf1d.5 ⊢ ( 𝜑 → ( ( 𝐹 “ 𝐶 ) ∩ ( 𝐹 “ ( 𝐴 ∖ 𝐶 ) ) ) = ∅ )
6 f1resveqaeq ⊢ ( ( ( 𝐹 ↾ 𝐶 ) : 𝐶 –1-1→ 𝐵 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
7 3 6 sylan ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
8 7 ex ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
9 difssd ⊢ ( 𝜑 → ( 𝐴 ∖ 𝐶 ) ⊆ 𝐴 )
10 1 9 2 5 f1resrcmplf1dlem ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ ( 𝐴 ∖ 𝐶 ) ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
11 incom ⊢ ( ( 𝐹 “ 𝐶 ) ∩ ( 𝐹 “ ( 𝐴 ∖ 𝐶 ) ) ) = ( ( 𝐹 “ ( 𝐴 ∖ 𝐶 ) ) ∩ ( 𝐹 “ 𝐶 ) )
12 11 5 eqtr3id ⊢ ( 𝜑 → ( ( 𝐹 “ ( 𝐴 ∖ 𝐶 ) ) ∩ ( 𝐹 “ 𝐶 ) ) = ∅ )
13 9 1 2 12 f1resrcmplf1dlem ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝑦 ∈ 𝐶 ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
14 f1resveqaeq ⊢ ( ( ( 𝐹 ↾ ( 𝐴 ∖ 𝐶 ) ) : ( 𝐴 ∖ 𝐶 ) –1-1→ 𝐵 ∧ ( 𝑥 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝑦 ∈ ( 𝐴 ∖ 𝐶 ) ) ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
15 4 14 sylan ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝑦 ∈ ( 𝐴 ∖ 𝐶 ) ) ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
16 15 ex ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝑦 ∈ ( 𝐴 ∖ 𝐶 ) ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
17 8 10 13 16 prsrcmpltd ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
18 17 ralrimivv ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
19 dff13 ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
20 2 18 19 sylanbrc ⊢ ( 𝜑 → 𝐹 : 𝐴 –1-1→ 𝐵 )