Metamath Proof Explorer

Theorem ssrel2

Description: A subclass relationship depends only on a relation's ordered pairs. This version of ssrel is restricted to the relation's domain. (Contributed by Thierry Arnoux, 25-Jan-2018)

Ref Expression
Assertion ssrel2 
|- ( R C_ ( A X. B ) -> ( R C_ S <-> A. x e. A A. y e. B ( <. x , y >. e. R -> <. x , y >. e. S ) ) )

Proof

Step Hyp Ref Expression
1 ssel 
 |-  ( R C_ S -> ( <. x , y >. e. R -> <. x , y >. e. S ) )
2 1 a1d 
 |-  ( R C_ S -> ( ( x e. A /\ y e. B ) -> ( <. x , y >. e. R -> <. x , y >. e. S ) ) )
3 2 ralrimivv 
 |-  ( R C_ S -> A. x e. A A. y e. B ( <. x , y >. e. R -> <. x , y >. e. S ) )
4 eleq1 
 |-  ( z = <. x , y >. -> ( z e. R <-> <. x , y >. e. R ) )
5 eleq1 
 |-  ( z = <. x , y >. -> ( z e. S <-> <. x , y >. e. S ) )
6 4 5 imbi12d 
 |-  ( z = <. x , y >. -> ( ( z e. R -> z e. S ) <-> ( <. x , y >. e. R -> <. x , y >. e. S ) ) )
7 6 biimprcd 
 |-  ( ( <. x , y >. e. R -> <. x , y >. e. S ) -> ( z = <. x , y >. -> ( z e. R -> z e. S ) ) )
8 7 2ralimi 
 |-  ( A. x e. A A. y e. B ( <. x , y >. e. R -> <. x , y >. e. S ) -> A. x e. A A. y e. B ( z = <. x , y >. -> ( z e. R -> z e. S ) ) )
9 r19.23v 
 |-  ( A. y e. B ( z = <. x , y >. -> ( z e. R -> z e. S ) ) <-> ( E. y e. B z = <. x , y >. -> ( z e. R -> z e. S ) ) )
10 9 ralbii 
 |-  ( A. x e. A A. y e. B ( z = <. x , y >. -> ( z e. R -> z e. S ) ) <-> A. x e. A ( E. y e. B z = <. x , y >. -> ( z e. R -> z e. S ) ) )
11 r19.23v 
 |-  ( A. x e. A ( E. y e. B z = <. x , y >. -> ( z e. R -> z e. S ) ) <-> ( E. x e. A E. y e. B z = <. x , y >. -> ( z e. R -> z e. S ) ) )
12 10 11 bitri 
 |-  ( A. x e. A A. y e. B ( z = <. x , y >. -> ( z e. R -> z e. S ) ) <-> ( E. x e. A E. y e. B z = <. x , y >. -> ( z e. R -> z e. S ) ) )
13 8 12 sylib 
 |-  ( A. x e. A A. y e. B ( <. x , y >. e. R -> <. x , y >. e. S ) -> ( E. x e. A E. y e. B z = <. x , y >. -> ( z e. R -> z e. S ) ) )
14 13 com23 
 |-  ( A. x e. A A. y e. B ( <. x , y >. e. R -> <. x , y >. e. S ) -> ( z e. R -> ( E. x e. A E. y e. B z = <. x , y >. -> z e. S ) ) )
15 14 a2d 
 |-  ( A. x e. A A. y e. B ( <. x , y >. e. R -> <. x , y >. e. S ) -> ( ( z e. R -> E. x e. A E. y e. B z = <. x , y >. ) -> ( z e. R -> z e. S ) ) )
16 15 alimdv 
 |-  ( A. x e. A A. y e. B ( <. x , y >. e. R -> <. x , y >. e. S ) -> ( A. z ( z e. R -> E. x e. A E. y e. B z = <. x , y >. ) -> A. z ( z e. R -> z e. S ) ) )
17 df-ss 
 |-  ( R C_ ( A X. B ) <-> A. z ( z e. R -> z e. ( A X. B ) ) )
18 elxp2 
 |-  ( z e. ( A X. B ) <-> E. x e. A E. y e. B z = <. x , y >. )
19 18 imbi2i 
 |-  ( ( z e. R -> z e. ( A X. B ) ) <-> ( z e. R -> E. x e. A E. y e. B z = <. x , y >. ) )
20 19 albii 
 |-  ( A. z ( z e. R -> z e. ( A X. B ) ) <-> A. z ( z e. R -> E. x e. A E. y e. B z = <. x , y >. ) )
21 17 20 bitri 
 |-  ( R C_ ( A X. B ) <-> A. z ( z e. R -> E. x e. A E. y e. B z = <. x , y >. ) )
22 df-ss 
 |-  ( R C_ S <-> A. z ( z e. R -> z e. S ) )
23 16 21 22 3imtr4g 
 |-  ( A. x e. A A. y e. B ( <. x , y >. e. R -> <. x , y >. e. S ) -> ( R C_ ( A X. B ) -> R C_ S ) )
24 23 com12 
 |-  ( R C_ ( A X. B ) -> ( A. x e. A A. y e. B ( <. x , y >. e. R -> <. x , y >. e. S ) -> R C_ S ) )
25 3 24 impbid2 
 |-  ( R C_ ( A X. B ) -> ( R C_ S <-> A. x e. A A. y e. B ( <. x , y >. e. R -> <. x , y >. e. S ) ) )