Metamath Proof Explorer

Theorem ssrel

Description: A subclass relationship depends only on a relation's ordered pairs. Theorem 3.2(i) of Monk1 p. 33. (Contributed by NM, 2-Aug-1994) (Proof shortened by Andrew Salmon, 27-Aug-2011) Remove dependency on ax-sep , ax-nul , ax-pr . (Revised by KP, 25-Oct-2021)

Ref Expression
Assertion ssrel 
|- ( Rel A -> ( A C_ B <-> A. x A. y ( <. x , y >. e. A -> <. x , y >. e. B ) ) )

Proof

Step Hyp Ref Expression
1 ssel 
 |-  ( A C_ B -> ( <. x , y >. e. A -> <. x , y >. e. B ) )
2 1 alrimivv 
 |-  ( A C_ B -> A. x A. y ( <. x , y >. e. A -> <. x , y >. e. B ) )
3 df-rel 
 |-  ( Rel A <-> A C_ ( _V X. _V ) )
4 dfss2 
 |-  ( A C_ ( _V X. _V ) <-> A. z ( z e. A -> z e. ( _V X. _V ) ) )
5 3 4 sylbb 
 |-  ( Rel A -> A. z ( z e. A -> z e. ( _V X. _V ) ) )
6 df-xp 
 |-  ( _V X. _V ) = { <. x , y >. | ( x e. _V /\ y e. _V ) }
7 df-opab 
 |-  { <. x , y >. | ( x e. _V /\ y e. _V ) } = { z | E. x E. y ( z = <. x , y >. /\ ( x e. _V /\ y e. _V ) ) }
8 6 7 eqtri 
 |-  ( _V X. _V ) = { z | E. x E. y ( z = <. x , y >. /\ ( x e. _V /\ y e. _V ) ) }
9 8 abeq2i 
 |-  ( z e. ( _V X. _V ) <-> E. x E. y ( z = <. x , y >. /\ ( x e. _V /\ y e. _V ) ) )
10 simpl 
 |-  ( ( z = <. x , y >. /\ ( x e. _V /\ y e. _V ) ) -> z = <. x , y >. )
11 10 2eximi 
 |-  ( E. x E. y ( z = <. x , y >. /\ ( x e. _V /\ y e. _V ) ) -> E. x E. y z = <. x , y >. )
12 9 11 sylbi 
 |-  ( z e. ( _V X. _V ) -> E. x E. y z = <. x , y >. )
13 12 imim2i 
 |-  ( ( z e. A -> z e. ( _V X. _V ) ) -> ( z e. A -> E. x E. y z = <. x , y >. ) )
14 5 13 sylg 
 |-  ( Rel A -> A. z ( z e. A -> E. x E. y z = <. x , y >. ) )
15 eleq1 
 |-  ( z = <. x , y >. -> ( z e. A <-> <. x , y >. e. A ) )
16 eleq1 
 |-  ( z = <. x , y >. -> ( z e. B <-> <. x , y >. e. B ) )
17 15 16 imbi12d 
 |-  ( z = <. x , y >. -> ( ( z e. A -> z e. B ) <-> ( <. x , y >. e. A -> <. x , y >. e. B ) ) )
18 17 biimprcd 
 |-  ( ( <. x , y >. e. A -> <. x , y >. e. B ) -> ( z = <. x , y >. -> ( z e. A -> z e. B ) ) )
19 18 2alimi 
 |-  ( A. x A. y ( <. x , y >. e. A -> <. x , y >. e. B ) -> A. x A. y ( z = <. x , y >. -> ( z e. A -> z e. B ) ) )
20 19.23vv 
 |-  ( A. x A. y ( z = <. x , y >. -> ( z e. A -> z e. B ) ) <-> ( E. x E. y z = <. x , y >. -> ( z e. A -> z e. B ) ) )
21 19 20 sylib 
 |-  ( A. x A. y ( <. x , y >. e. A -> <. x , y >. e. B ) -> ( E. x E. y z = <. x , y >. -> ( z e. A -> z e. B ) ) )
22 21 com23 
 |-  ( A. x A. y ( <. x , y >. e. A -> <. x , y >. e. B ) -> ( z e. A -> ( E. x E. y z = <. x , y >. -> z e. B ) ) )
23 22 a2d 
 |-  ( A. x A. y ( <. x , y >. e. A -> <. x , y >. e. B ) -> ( ( z e. A -> E. x E. y z = <. x , y >. ) -> ( z e. A -> z e. B ) ) )
24 23 alimdv 
 |-  ( A. x A. y ( <. x , y >. e. A -> <. x , y >. e. B ) -> ( A. z ( z e. A -> E. x E. y z = <. x , y >. ) -> A. z ( z e. A -> z e. B ) ) )
25 14 24 syl5 
 |-  ( A. x A. y ( <. x , y >. e. A -> <. x , y >. e. B ) -> ( Rel A -> A. z ( z e. A -> z e. B ) ) )
26 dfss2 
 |-  ( A C_ B <-> A. z ( z e. A -> z e. B ) )
27 25 26 syl6ibr 
 |-  ( A. x A. y ( <. x , y >. e. A -> <. x , y >. e. B ) -> ( Rel A -> A C_ B ) )
28 27 com12 
 |-  ( Rel A -> ( A. x A. y ( <. x , y >. e. A -> <. x , y >. e. B ) -> A C_ B ) )
29 2 28 impbid2 
 |-  ( Rel A -> ( A C_ B <-> A. x A. y ( <. x , y >. e. A -> <. x , y >. e. B ) ) )