Metamath Proof Explorer

Theorem funeldmdif

Description: Two ways of expressing membership in the difference of domains of two nested functions. (Contributed by AV, 27-Oct-2023)

Ref Expression
Assertion funeldmdif 
|- ( ( Fun A /\ B C_ A ) -> ( C e. ( dom A \ dom B ) <-> E. x e. ( A \ B ) ( 1st ` x ) = C ) )

Proof

Step Hyp Ref Expression
1 funrel 
 |-  ( Fun A -> Rel A )
2 releldmdifi 
 |-  ( ( Rel A /\ B C_ A ) -> ( C e. ( dom A \ dom B ) -> E. x e. ( A \ B ) ( 1st ` x ) = C ) )
3 1 2 sylan 
 |-  ( ( Fun A /\ B C_ A ) -> ( C e. ( dom A \ dom B ) -> E. x e. ( A \ B ) ( 1st ` x ) = C ) )
4 eldif 
 |-  ( x e. ( A \ B ) <-> ( x e. A /\ -. x e. B ) )
5 1stdm 
 |-  ( ( Rel A /\ x e. A ) -> ( 1st ` x ) e. dom A )
6 5 ex 
 |-  ( Rel A -> ( x e. A -> ( 1st ` x ) e. dom A ) )
7 1 6 syl 
 |-  ( Fun A -> ( x e. A -> ( 1st ` x ) e. dom A ) )
8 7 adantr 
 |-  ( ( Fun A /\ B C_ A ) -> ( x e. A -> ( 1st ` x ) e. dom A ) )
9 8 com12 
 |-  ( x e. A -> ( ( Fun A /\ B C_ A ) -> ( 1st ` x ) e. dom A ) )
10 9 adantr 
 |-  ( ( x e. A /\ -. x e. B ) -> ( ( Fun A /\ B C_ A ) -> ( 1st ` x ) e. dom A ) )
11 10 impcom 
 |-  ( ( ( Fun A /\ B C_ A ) /\ ( x e. A /\ -. x e. B ) ) -> ( 1st ` x ) e. dom A )
12 funelss 
 |-  ( ( Fun A /\ B C_ A /\ x e. A ) -> ( ( 1st ` x ) e. dom B -> x e. B ) )
13 12 3expa 
 |-  ( ( ( Fun A /\ B C_ A ) /\ x e. A ) -> ( ( 1st ` x ) e. dom B -> x e. B ) )
14 13 con3d 
 |-  ( ( ( Fun A /\ B C_ A ) /\ x e. A ) -> ( -. x e. B -> -. ( 1st ` x ) e. dom B ) )
15 14 impr 
 |-  ( ( ( Fun A /\ B C_ A ) /\ ( x e. A /\ -. x e. B ) ) -> -. ( 1st ` x ) e. dom B )
16 11 15 eldifd 
 |-  ( ( ( Fun A /\ B C_ A ) /\ ( x e. A /\ -. x e. B ) ) -> ( 1st ` x ) e. ( dom A \ dom B ) )
17 16 3adant3 
 |-  ( ( ( Fun A /\ B C_ A ) /\ ( x e. A /\ -. x e. B ) /\ ( 1st ` x ) = C ) -> ( 1st ` x ) e. ( dom A \ dom B ) )
18 eleq1 
 |-  ( ( 1st ` x ) = C -> ( ( 1st ` x ) e. ( dom A \ dom B ) <-> C e. ( dom A \ dom B ) ) )
19 18 3ad2ant3 
 |-  ( ( ( Fun A /\ B C_ A ) /\ ( x e. A /\ -. x e. B ) /\ ( 1st ` x ) = C ) -> ( ( 1st ` x ) e. ( dom A \ dom B ) <-> C e. ( dom A \ dom B ) ) )
20 17 19 mpbid 
 |-  ( ( ( Fun A /\ B C_ A ) /\ ( x e. A /\ -. x e. B ) /\ ( 1st ` x ) = C ) -> C e. ( dom A \ dom B ) )
21 20 3exp 
 |-  ( ( Fun A /\ B C_ A ) -> ( ( x e. A /\ -. x e. B ) -> ( ( 1st ` x ) = C -> C e. ( dom A \ dom B ) ) ) )
22 4 21 syl5bi 
 |-  ( ( Fun A /\ B C_ A ) -> ( x e. ( A \ B ) -> ( ( 1st ` x ) = C -> C e. ( dom A \ dom B ) ) ) )
23 22 rexlimdv 
 |-  ( ( Fun A /\ B C_ A ) -> ( E. x e. ( A \ B ) ( 1st ` x ) = C -> C e. ( dom A \ dom B ) ) )
24 3 23 impbid 
 |-  ( ( Fun A /\ B C_ A ) -> ( C e. ( dom A \ dom B ) <-> E. x e. ( A \ B ) ( 1st ` x ) = C ) )