Metamath Proof Explorer

Theorem f1resrcmplf1dlem

Description: Lemma for f1resrcmplf1d . (Contributed by BTernaryTau, 27-Sep-2023)

Ref Expression
Hypotheses f1resrcmplf1dlem.1 ⊢ ( 𝜑 → 𝐶 ⊆ 𝐴 )
f1resrcmplf1dlem.2 ⊢ ( 𝜑 → 𝐷 ⊆ 𝐴 )
f1resrcmplf1dlem.3 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
f1resrcmplf1dlem.4 ⊢ ( 𝜑 → ( ( 𝐹 “ 𝐶 ) ∩ ( 𝐹 “ 𝐷 ) ) = ∅ )
Assertion f1resrcmplf1dlem ( 𝜑 → ( ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐷 ) → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 f1resrcmplf1dlem.1 ⊢ ( 𝜑 → 𝐶 ⊆ 𝐴 )
2 f1resrcmplf1dlem.2 ⊢ ( 𝜑 → 𝐷 ⊆ 𝐴 )
3 f1resrcmplf1dlem.3 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
4 f1resrcmplf1dlem.4 ⊢ ( 𝜑 → ( ( 𝐹 “ 𝐶 ) ∩ ( 𝐹 “ 𝐷 ) ) = ∅ )
5 3 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
6 fnfvima ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐶 ⊆ 𝐴 ∧ 𝑋 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑋 ) ∈ ( 𝐹 “ 𝐶 ) )
7 5 6 syl3an1 ⊢ ( ( 𝜑 ∧ 𝐶 ⊆ 𝐴 ∧ 𝑋 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑋 ) ∈ ( 𝐹 “ 𝐶 ) )
8 1 7 syl3an2 ⊢ ( ( 𝜑 ∧ 𝜑 ∧ 𝑋 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑋 ) ∈ ( 𝐹 “ 𝐶 ) )
9 8 3anidm12 ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑋 ) ∈ ( 𝐹 “ 𝐶 ) )
10 9 ex ⊢ ( 𝜑 → ( 𝑋 ∈ 𝐶 → ( 𝐹 ‘ 𝑋 ) ∈ ( 𝐹 “ 𝐶 ) ) )
11 fnfvima ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐷 ⊆ 𝐴 ∧ 𝑌 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑌 ) ∈ ( 𝐹 “ 𝐷 ) )
12 5 11 syl3an1 ⊢ ( ( 𝜑 ∧ 𝐷 ⊆ 𝐴 ∧ 𝑌 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑌 ) ∈ ( 𝐹 “ 𝐷 ) )
13 2 12 syl3an2 ⊢ ( ( 𝜑 ∧ 𝜑 ∧ 𝑌 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑌 ) ∈ ( 𝐹 “ 𝐷 ) )
14 13 3anidm12 ⊢ ( ( 𝜑 ∧ 𝑌 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑌 ) ∈ ( 𝐹 “ 𝐷 ) )
15 14 ex ⊢ ( 𝜑 → ( 𝑌 ∈ 𝐷 → ( 𝐹 ‘ 𝑌 ) ∈ ( 𝐹 “ 𝐷 ) ) )
16 disjne ⊢ ( ( ( ( 𝐹 “ 𝐶 ) ∩ ( 𝐹 “ 𝐷 ) ) = ∅ ∧ ( 𝐹 ‘ 𝑋 ) ∈ ( 𝐹 “ 𝐶 ) ∧ ( 𝐹 ‘ 𝑌 ) ∈ ( 𝐹 “ 𝐷 ) ) → ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) )
17 4 16 syl3an1 ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑋 ) ∈ ( 𝐹 “ 𝐶 ) ∧ ( 𝐹 ‘ 𝑌 ) ∈ ( 𝐹 “ 𝐷 ) ) → ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) )
18 17 3expib ⊢ ( 𝜑 → ( ( ( 𝐹 ‘ 𝑋 ) ∈ ( 𝐹 “ 𝐶 ) ∧ ( 𝐹 ‘ 𝑌 ) ∈ ( 𝐹 “ 𝐷 ) ) → ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) ) )
19 neneq ⊢ ( ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) → ¬ ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) )
20 19 pm2.21d ⊢ ( ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) )
21 18 20 syl6 ⊢ ( 𝜑 → ( ( ( 𝐹 ‘ 𝑋 ) ∈ ( 𝐹 “ 𝐶 ) ∧ ( 𝐹 ‘ 𝑌 ) ∈ ( 𝐹 “ 𝐷 ) ) → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) ) )
22 10 15 21 syl2and ⊢ ( 𝜑 → ( ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐷 ) → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) ) )