Metamath Proof Explorer

Theorem releldmdifi

Description: One way of expressing membership in the difference of domains of two nested relations. (Contributed by AV, 26-Oct-2023)

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

Proof

Step Hyp Ref Expression
1 eldif 
 |-  ( C e. ( dom A \ dom B ) <-> ( C e. dom A /\ -. C e. dom B ) )
2 releldm2 
 |-  ( Rel A -> ( C e. dom A <-> E. x e. A ( 1st ` x ) = C ) )
3 2 adantr 
 |-  ( ( Rel A /\ B C_ A ) -> ( C e. dom A <-> E. x e. A ( 1st ` x ) = C ) )
4 3 anbi1d 
 |-  ( ( Rel A /\ B C_ A ) -> ( ( C e. dom A /\ -. C e. dom B ) <-> ( E. x e. A ( 1st ` x ) = C /\ -. C e. dom B ) ) )
5 1 4 bitrid 
 |-  ( ( Rel A /\ B C_ A ) -> ( C e. ( dom A \ dom B ) <-> ( E. x e. A ( 1st ` x ) = C /\ -. C e. dom B ) ) )
6 simprl 
 |-  ( ( ( Rel A /\ B C_ A ) /\ ( E. x e. A ( 1st ` x ) = C /\ -. C e. dom B ) ) -> E. x e. A ( 1st ` x ) = C )
7 relss 
 |-  ( B C_ A -> ( Rel A -> Rel B ) )
8 7 impcom 
 |-  ( ( Rel A /\ B C_ A ) -> Rel B )
9 1stdm 
 |-  ( ( Rel B /\ x e. B ) -> ( 1st ` x ) e. dom B )
10 8 9 sylan 
 |-  ( ( ( Rel A /\ B C_ A ) /\ x e. B ) -> ( 1st ` x ) e. dom B )
11 eleq1 
 |-  ( ( 1st ` x ) = C -> ( ( 1st ` x ) e. dom B <-> C e. dom B ) )
12 10 11 syl5ibcom 
 |-  ( ( ( Rel A /\ B C_ A ) /\ x e. B ) -> ( ( 1st ` x ) = C -> C e. dom B ) )
13 12 rexlimdva 
 |-  ( ( Rel A /\ B C_ A ) -> ( E. x e. B ( 1st ` x ) = C -> C e. dom B ) )
14 13 con3d 
 |-  ( ( Rel A /\ B C_ A ) -> ( -. C e. dom B -> -. E. x e. B ( 1st ` x ) = C ) )
15 ralnex 
 |-  ( A. x e. B -. ( 1st ` x ) = C <-> -. E. x e. B ( 1st ` x ) = C )
16 14 15 syl6ibr 
 |-  ( ( Rel A /\ B C_ A ) -> ( -. C e. dom B -> A. x e. B -. ( 1st ` x ) = C ) )
17 16 adantld 
 |-  ( ( Rel A /\ B C_ A ) -> ( ( E. x e. A ( 1st ` x ) = C /\ -. C e. dom B ) -> A. x e. B -. ( 1st ` x ) = C ) )
18 17 imp 
 |-  ( ( ( Rel A /\ B C_ A ) /\ ( E. x e. A ( 1st ` x ) = C /\ -. C e. dom B ) ) -> A. x e. B -. ( 1st ` x ) = C )
19 rexdifi 
 |-  ( ( E. x e. A ( 1st ` x ) = C /\ A. x e. B -. ( 1st ` x ) = C ) -> E. x e. ( A \ B ) ( 1st ` x ) = C )
20 6 18 19 syl2anc 
 |-  ( ( ( Rel A /\ B C_ A ) /\ ( E. x e. A ( 1st ` x ) = C /\ -. C e. dom B ) ) -> E. x e. ( A \ B ) ( 1st ` x ) = C )
21 20 ex 
 |-  ( ( Rel A /\ B C_ A ) -> ( ( E. x e. A ( 1st ` x ) = C /\ -. C e. dom B ) -> E. x e. ( A \ B ) ( 1st ` x ) = C ) )
22 5 21 sylbid 
 |-  ( ( Rel A /\ B C_ A ) -> ( C e. ( dom A \ dom B ) -> E. x e. ( A \ B ) ( 1st ` x ) = C ) )