This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ssrelf

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) (Revised by Thierry Arnoux, 6-Nov-2017)

Ref Expression
Hypotheses eqrelrd2.1 
|- F/ x ph
eqrelrd2.2 
|- F/ y ph
eqrelrd2.3 
|- F/_ x A
eqrelrd2.4 
|- F/_ y A
eqrelrd2.5 
|- F/_ x B
eqrelrd2.6 
|- F/_ y B
Assertion ssrelf 
|- ( Rel A -> ( A C_ B <-> A. x A. y ( <. x , y >. e. A -> <. x , y >. e. B ) ) )

Proof

Step Hyp Ref Expression
1 eqrelrd2.1 
 |-  F/ x ph
2 eqrelrd2.2 
 |-  F/ y ph
3 eqrelrd2.3 
 |-  F/_ x A
4 eqrelrd2.4 
 |-  F/_ y A
5 eqrelrd2.5 
 |-  F/_ x B
6 eqrelrd2.6 
 |-  F/_ y B
7 3 5 nfss 
 |-  F/ x A C_ B
8 4 6 nfss 
 |-  F/ y A C_ B
9 ssel 
 |-  ( A C_ B -> ( <. x , y >. e. A -> <. x , y >. e. B ) )
10 8 9 alrimi 
 |-  ( A C_ B -> A. y ( <. x , y >. e. A -> <. x , y >. e. B ) )
11 7 10 alrimi 
 |-  ( A C_ B -> A. x A. y ( <. x , y >. e. A -> <. x , y >. e. B ) )
12 eleq1 
 |-  ( z = <. x , y >. -> ( z e. A <-> <. x , y >. e. A ) )
13 eleq1 
 |-  ( z = <. x , y >. -> ( z e. B <-> <. x , y >. e. B ) )
14 12 13 imbi12d 
 |-  ( z = <. x , y >. -> ( ( z e. A -> z e. B ) <-> ( <. x , y >. e. A -> <. x , y >. e. B ) ) )
15 14 biimprcd 
 |-  ( ( <. x , y >. e. A -> <. x , y >. e. B ) -> ( z = <. x , y >. -> ( z e. A -> z e. B ) ) )
16 15 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 ) ) )
17 4 nfcri 
 |-  F/ y z e. A
18 6 nfcri 
 |-  F/ y z e. B
19 17 18 nfim 
 |-  F/ y ( z e. A -> z e. B )
20 19 19.23 
 |-  ( A. y ( z = <. x , y >. -> ( z e. A -> z e. B ) ) <-> ( E. y z = <. x , y >. -> ( z e. A -> z e. B ) ) )
21 20 albii 
 |-  ( A. x A. y ( z = <. x , y >. -> ( z e. A -> z e. B ) ) <-> A. x ( E. y z = <. x , y >. -> ( z e. A -> z e. B ) ) )
22 3 nfcri 
 |-  F/ x z e. A
23 5 nfcri 
 |-  F/ x z e. B
24 22 23 nfim 
 |-  F/ x ( z e. A -> z e. B )
25 24 19.23 
 |-  ( A. x ( E. y z = <. x , y >. -> ( z e. A -> z e. B ) ) <-> ( E. x E. y z = <. x , y >. -> ( z e. A -> z e. B ) ) )
26 21 25 bitri 
 |-  ( 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 ) ) )
27 16 26 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 ) ) )
28 27 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 ) ) )
29 28 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 ) ) )
30 29 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 ) ) )
31 df-rel 
 |-  ( Rel A <-> A C_ ( _V X. _V ) )
32 df-ss 
 |-  ( A C_ ( _V X. _V ) <-> A. z ( z e. A -> z e. ( _V X. _V ) ) )
33 elvv 
 |-  ( z e. ( _V X. _V ) <-> E. x E. y z = <. x , y >. )
34 33 imbi2i 
 |-  ( ( z e. A -> z e. ( _V X. _V ) ) <-> ( z e. A -> E. x E. y z = <. x , y >. ) )
35 34 albii 
 |-  ( A. z ( z e. A -> z e. ( _V X. _V ) ) <-> A. z ( z e. A -> E. x E. y z = <. x , y >. ) )
36 31 32 35 3bitri 
 |-  ( Rel A <-> A. z ( z e. A -> E. x E. y z = <. x , y >. ) )
37 df-ss 
 |-  ( A C_ B <-> A. z ( z e. A -> z e. B ) )
38 30 36 37 3imtr4g 
 |-  ( A. x A. y ( <. x , y >. e. A -> <. x , y >. e. B ) -> ( Rel A -> A C_ B ) )
39 38 com12 
 |-  ( Rel A -> ( A. x A. y ( <. x , y >. e. A -> <. x , y >. e. B ) -> A C_ B ) )
40 11 39 impbid2 
 |-  ( Rel A -> ( A C_ B <-> A. x A. y ( <. x , y >. e. A -> <. x , y >. e. B ) ) )