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 1 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ ( 𝐴 ∖ 𝐶 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → 𝐶 ⊆ 𝐴 )
10 difssd ⊢ ( 𝜑 → ( 𝐴 ∖ 𝐶 ) ⊆ 𝐴 )
11 10 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ ( 𝐴 ∖ 𝐶 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → ( 𝐴 ∖ 𝐶 ) ⊆ 𝐴 )
12 2 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ ( 𝐴 ∖ 𝐶 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → 𝐹 : 𝐴 ⟶ 𝐵 )
13 5 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ ( 𝐴 ∖ 𝐶 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → ( ( 𝐹 “ 𝐶 ) ∩ ( 𝐹 “ ( 𝐴 ∖ 𝐶 ) ) ) = ∅ )
14 simp2l ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ ( 𝐴 ∖ 𝐶 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → 𝑥 ∈ 𝐶 )
15 simp2r ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ ( 𝐴 ∖ 𝐶 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → 𝑦 ∈ ( 𝐴 ∖ 𝐶 ) )
16 simp3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ ( 𝐴 ∖ 𝐶 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) )
17 9 11 12 13 14 15 16 f1resrcmplf1dlem ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ ( 𝐴 ∖ 𝐶 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → 𝑥 = 𝑦 )
18 17 3exp ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ ( 𝐴 ∖ 𝐶 ) ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
19 10 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝑦 ∈ 𝐶 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → ( 𝐴 ∖ 𝐶 ) ⊆ 𝐴 )
20 1 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝑦 ∈ 𝐶 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → 𝐶 ⊆ 𝐴 )
21 2 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝑦 ∈ 𝐶 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → 𝐹 : 𝐴 ⟶ 𝐵 )
22 incom ⊢ ( ( 𝐹 “ 𝐶 ) ∩ ( 𝐹 “ ( 𝐴 ∖ 𝐶 ) ) ) = ( ( 𝐹 “ ( 𝐴 ∖ 𝐶 ) ) ∩ ( 𝐹 “ 𝐶 ) )
23 22 5 eqtr3id ⊢ ( 𝜑 → ( ( 𝐹 “ ( 𝐴 ∖ 𝐶 ) ) ∩ ( 𝐹 “ 𝐶 ) ) = ∅ )
24 23 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝑦 ∈ 𝐶 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → ( ( 𝐹 “ ( 𝐴 ∖ 𝐶 ) ) ∩ ( 𝐹 “ 𝐶 ) ) = ∅ )
25 simp2l ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝑦 ∈ 𝐶 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → 𝑥 ∈ ( 𝐴 ∖ 𝐶 ) )
26 simp2r ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝑦 ∈ 𝐶 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → 𝑦 ∈ 𝐶 )
27 simp3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝑦 ∈ 𝐶 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) )
28 19 20 21 24 25 26 27 f1resrcmplf1dlem ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝑦 ∈ 𝐶 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → 𝑥 = 𝑦 )
29 28 3exp ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝑦 ∈ 𝐶 ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
30 f1resveqaeq ⊢ ( ( ( 𝐹 ↾ ( 𝐴 ∖ 𝐶 ) ) : ( 𝐴 ∖ 𝐶 ) –1-1→ 𝐵 ∧ ( 𝑥 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝑦 ∈ ( 𝐴 ∖ 𝐶 ) ) ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
31 4 30 sylan ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝑦 ∈ ( 𝐴 ∖ 𝐶 ) ) ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
32 31 ex ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝐴 ∖ 𝐶 ) ∧ 𝑦 ∈ ( 𝐴 ∖ 𝐶 ) ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
33 8 18 29 32 prsrcmpltd ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
34 33 ralrimivv ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
35 dff13 ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
36 2 34 35 sylanbrc ⊢ ( 𝜑 → 𝐹 : 𝐴 –1-1→ 𝐵 )