Metamath Proof Explorer

Theorem f1resrcmplf1dlem

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

Ref Expression
Hypotheses f1resrcmplf1dlem.1 
|- ( ph -> C C_ A )
f1resrcmplf1dlem.2 
|- ( ph -> D C_ A )
f1resrcmplf1dlem.3 
|- ( ph -> F : A --> B )
f1resrcmplf1dlem.4 
|- ( ph -> ( ( F " C ) i^i ( F " D ) ) = (/) )
Assertion f1resrcmplf1dlem 
|- ( ph -> ( ( X e. C /\ Y e. D ) -> ( ( F ` X ) = ( F ` Y ) -> X = Y ) ) )

Proof

Step Hyp Ref Expression
1 f1resrcmplf1dlem.1 
 |-  ( ph -> C C_ A )
2 f1resrcmplf1dlem.2 
 |-  ( ph -> D C_ A )
3 f1resrcmplf1dlem.3 
 |-  ( ph -> F : A --> B )
4 f1resrcmplf1dlem.4 
 |-  ( ph -> ( ( F " C ) i^i ( F " D ) ) = (/) )
5 3 ffnd 
 |-  ( ph -> F Fn A )
6 fnfvima 
 |-  ( ( F Fn A /\ C C_ A /\ X e. C ) -> ( F ` X ) e. ( F " C ) )
7 5 6 syl3an1 
 |-  ( ( ph /\ C C_ A /\ X e. C ) -> ( F ` X ) e. ( F " C ) )
8 1 7 syl3an2 
 |-  ( ( ph /\ ph /\ X e. C ) -> ( F ` X ) e. ( F " C ) )
9 8 3anidm12 
 |-  ( ( ph /\ X e. C ) -> ( F ` X ) e. ( F " C ) )
10 9 ex 
 |-  ( ph -> ( X e. C -> ( F ` X ) e. ( F " C ) ) )
11 fnfvima 
 |-  ( ( F Fn A /\ D C_ A /\ Y e. D ) -> ( F ` Y ) e. ( F " D ) )
12 5 11 syl3an1 
 |-  ( ( ph /\ D C_ A /\ Y e. D ) -> ( F ` Y ) e. ( F " D ) )
13 2 12 syl3an2 
 |-  ( ( ph /\ ph /\ Y e. D ) -> ( F ` Y ) e. ( F " D ) )
14 13 3anidm12 
 |-  ( ( ph /\ Y e. D ) -> ( F ` Y ) e. ( F " D ) )
15 14 ex 
 |-  ( ph -> ( Y e. D -> ( F ` Y ) e. ( F " D ) ) )
16 disjne 
 |-  ( ( ( ( F " C ) i^i ( F " D ) ) = (/) /\ ( F ` X ) e. ( F " C ) /\ ( F ` Y ) e. ( F " D ) ) -> ( F ` X ) =/= ( F ` Y ) )
17 4 16 syl3an1 
 |-  ( ( ph /\ ( F ` X ) e. ( F " C ) /\ ( F ` Y ) e. ( F " D ) ) -> ( F ` X ) =/= ( F ` Y ) )
18 17 3expib 
 |-  ( ph -> ( ( ( F ` X ) e. ( F " C ) /\ ( F ` Y ) e. ( F " D ) ) -> ( F ` X ) =/= ( F ` Y ) ) )
19 neneq 
 |-  ( ( F ` X ) =/= ( F ` Y ) -> -. ( F ` X ) = ( F ` Y ) )
20 19 pm2.21d 
 |-  ( ( F ` X ) =/= ( F ` Y ) -> ( ( F ` X ) = ( F ` Y ) -> X = Y ) )
21 18 20 syl6 
 |-  ( ph -> ( ( ( F ` X ) e. ( F " C ) /\ ( F ` Y ) e. ( F " D ) ) -> ( ( F ` X ) = ( F ` Y ) -> X = Y ) ) )
22 10 15 21 syl2and 
 |-  ( ph -> ( ( X e. C /\ Y e. D ) -> ( ( F ` X ) = ( F ` Y ) -> X = Y ) ) )