Metamath Proof Explorer

Theorem ssrnres

Description: Two ways to express surjectivity of a restricted and corestricted binary relation (intersection of a binary relation with a Cartesian product): the LHS expresses inclusion in the range of the restricted relation, while the RHS expresses equality with the range of the restricted and corestricted relation. (Contributed by NM, 16-Jan-2006) (Proof shortened by Peter Mazsa, 2-Oct-2022)

Ref Expression
Assertion ssrnres 
|- ( B C_ ran ( C |` A ) <-> ran ( C i^i ( A X. B ) ) = B )

Proof

Step Hyp Ref Expression
1 inss2 
 |-  ( C i^i ( A X. B ) ) C_ ( A X. B )
2 1 rnssi 
 |-  ran ( C i^i ( A X. B ) ) C_ ran ( A X. B )
3 rnxpss 
 |-  ran ( A X. B ) C_ B
4 2 3 sstri 
 |-  ran ( C i^i ( A X. B ) ) C_ B
5 eqss 
 |-  ( ran ( C i^i ( A X. B ) ) = B <-> ( ran ( C i^i ( A X. B ) ) C_ B /\ B C_ ran ( C i^i ( A X. B ) ) ) )
6 4 5 mpbiran 
 |-  ( ran ( C i^i ( A X. B ) ) = B <-> B C_ ran ( C i^i ( A X. B ) ) )
7 inxpssres 
 |-  ( C i^i ( A X. B ) ) C_ ( C |` A )
8 7 rnssi 
 |-  ran ( C i^i ( A X. B ) ) C_ ran ( C |` A )
9 sstr 
 |-  ( ( B C_ ran ( C i^i ( A X. B ) ) /\ ran ( C i^i ( A X. B ) ) C_ ran ( C |` A ) ) -> B C_ ran ( C |` A ) )
10 8 9 mpan2 
 |-  ( B C_ ran ( C i^i ( A X. B ) ) -> B C_ ran ( C |` A ) )
11 ssel 
 |-  ( B C_ ran ( C |` A ) -> ( y e. B -> y e. ran ( C |` A ) ) )
12 vex 
 |-  y e. _V
13 12 elrn2 
 |-  ( y e. ran ( C |` A ) <-> E. x <. x , y >. e. ( C |` A ) )
14 11 13 syl6ib 
 |-  ( B C_ ran ( C |` A ) -> ( y e. B -> E. x <. x , y >. e. ( C |` A ) ) )
15 14 ancld 
 |-  ( B C_ ran ( C |` A ) -> ( y e. B -> ( y e. B /\ E. x <. x , y >. e. ( C |` A ) ) ) )
16 12 elrn2 
 |-  ( y e. ran ( C i^i ( A X. B ) ) <-> E. x <. x , y >. e. ( C i^i ( A X. B ) ) )
17 opelinxp 
 |-  ( <. x , y >. e. ( C i^i ( A X. B ) ) <-> ( ( x e. A /\ y e. B ) /\ <. x , y >. e. C ) )
18 12 opelresi 
 |-  ( <. x , y >. e. ( C |` A ) <-> ( x e. A /\ <. x , y >. e. C ) )
19 18 bianassc 
 |-  ( ( y e. B /\ <. x , y >. e. ( C |` A ) ) <-> ( ( x e. A /\ y e. B ) /\ <. x , y >. e. C ) )
20 17 19 bitr4i 
 |-  ( <. x , y >. e. ( C i^i ( A X. B ) ) <-> ( y e. B /\ <. x , y >. e. ( C |` A ) ) )
21 20 exbii 
 |-  ( E. x <. x , y >. e. ( C i^i ( A X. B ) ) <-> E. x ( y e. B /\ <. x , y >. e. ( C |` A ) ) )
22 19.42v 
 |-  ( E. x ( y e. B /\ <. x , y >. e. ( C |` A ) ) <-> ( y e. B /\ E. x <. x , y >. e. ( C |` A ) ) )
23 16 21 22 3bitri 
 |-  ( y e. ran ( C i^i ( A X. B ) ) <-> ( y e. B /\ E. x <. x , y >. e. ( C |` A ) ) )
24 15 23 syl6ibr 
 |-  ( B C_ ran ( C |` A ) -> ( y e. B -> y e. ran ( C i^i ( A X. B ) ) ) )
25 24 ssrdv 
 |-  ( B C_ ran ( C |` A ) -> B C_ ran ( C i^i ( A X. B ) ) )
26 10 25 impbii 
 |-  ( B C_ ran ( C i^i ( A X. B ) ) <-> B C_ ran ( C |` A ) )
27 6 26 bitr2i 
 |-  ( B C_ ran ( C |` A ) <-> ran ( C i^i ( A X. B ) ) = B )