Metamath Proof Explorer

Theorem ssrelrel

Description: A subclass relationship determined by ordered triples. Use relrelss to express the antecedent in terms of the relation predicate. (Contributed by NM, 17-Dec-2008) (Proof shortened by Andrew Salmon, 27-Aug-2011)

Ref Expression
Assertion ssrelrel 
|- ( A C_ ( ( _V X. _V ) X. _V ) -> ( A C_ B <-> A. x A. y A. z ( <. <. x , y >. , z >. e. A -> <. <. x , y >. , z >. e. B ) ) )

Proof

Step Hyp Ref Expression
1 ssel 
 |-  ( A C_ B -> ( <. <. x , y >. , z >. e. A -> <. <. x , y >. , z >. e. B ) )
2 1 alrimiv 
 |-  ( A C_ B -> A. z ( <. <. x , y >. , z >. e. A -> <. <. x , y >. , z >. e. B ) )
3 2 alrimivv 
 |-  ( A C_ B -> A. x A. y A. z ( <. <. x , y >. , z >. e. A -> <. <. x , y >. , z >. e. B ) )
4 elvvv 
 |-  ( w e. ( ( _V X. _V ) X. _V ) <-> E. x E. y E. z w = <. <. x , y >. , z >. )
5 eleq1 
 |-  ( w = <. <. x , y >. , z >. -> ( w e. A <-> <. <. x , y >. , z >. e. A ) )
6 eleq1 
 |-  ( w = <. <. x , y >. , z >. -> ( w e. B <-> <. <. x , y >. , z >. e. B ) )
7 5 6 imbi12d 
 |-  ( w = <. <. x , y >. , z >. -> ( ( w e. A -> w e. B ) <-> ( <. <. x , y >. , z >. e. A -> <. <. x , y >. , z >. e. B ) ) )
8 7 biimprcd 
 |-  ( ( <. <. x , y >. , z >. e. A -> <. <. x , y >. , z >. e. B ) -> ( w = <. <. x , y >. , z >. -> ( w e. A -> w e. B ) ) )
9 8 alimi 
 |-  ( A. z ( <. <. x , y >. , z >. e. A -> <. <. x , y >. , z >. e. B ) -> A. z ( w = <. <. x , y >. , z >. -> ( w e. A -> w e. B ) ) )
10 19.23v 
 |-  ( A. z ( w = <. <. x , y >. , z >. -> ( w e. A -> w e. B ) ) <-> ( E. z w = <. <. x , y >. , z >. -> ( w e. A -> w e. B ) ) )
11 9 10 sylib 
 |-  ( A. z ( <. <. x , y >. , z >. e. A -> <. <. x , y >. , z >. e. B ) -> ( E. z w = <. <. x , y >. , z >. -> ( w e. A -> w e. B ) ) )
12 11 2alimi 
 |-  ( A. x A. y A. z ( <. <. x , y >. , z >. e. A -> <. <. x , y >. , z >. e. B ) -> A. x A. y ( E. z w = <. <. x , y >. , z >. -> ( w e. A -> w e. B ) ) )
13 19.23vv 
 |-  ( A. x A. y ( E. z w = <. <. x , y >. , z >. -> ( w e. A -> w e. B ) ) <-> ( E. x E. y E. z w = <. <. x , y >. , z >. -> ( w e. A -> w e. B ) ) )
14 12 13 sylib 
 |-  ( A. x A. y A. z ( <. <. x , y >. , z >. e. A -> <. <. x , y >. , z >. e. B ) -> ( E. x E. y E. z w = <. <. x , y >. , z >. -> ( w e. A -> w e. B ) ) )
15 4 14 syl5bi 
 |-  ( A. x A. y A. z ( <. <. x , y >. , z >. e. A -> <. <. x , y >. , z >. e. B ) -> ( w e. ( ( _V X. _V ) X. _V ) -> ( w e. A -> w e. B ) ) )
16 15 com23 
 |-  ( A. x A. y A. z ( <. <. x , y >. , z >. e. A -> <. <. x , y >. , z >. e. B ) -> ( w e. A -> ( w e. ( ( _V X. _V ) X. _V ) -> w e. B ) ) )
17 16 a2d 
 |-  ( A. x A. y A. z ( <. <. x , y >. , z >. e. A -> <. <. x , y >. , z >. e. B ) -> ( ( w e. A -> w e. ( ( _V X. _V ) X. _V ) ) -> ( w e. A -> w e. B ) ) )
18 17 alimdv 
 |-  ( A. x A. y A. z ( <. <. x , y >. , z >. e. A -> <. <. x , y >. , z >. e. B ) -> ( A. w ( w e. A -> w e. ( ( _V X. _V ) X. _V ) ) -> A. w ( w e. A -> w e. B ) ) )
19 dfss2 
 |-  ( A C_ ( ( _V X. _V ) X. _V ) <-> A. w ( w e. A -> w e. ( ( _V X. _V ) X. _V ) ) )
20 dfss2 
 |-  ( A C_ B <-> A. w ( w e. A -> w e. B ) )
21 18 19 20 3imtr4g 
 |-  ( A. x A. y A. z ( <. <. x , y >. , z >. e. A -> <. <. x , y >. , z >. e. B ) -> ( A C_ ( ( _V X. _V ) X. _V ) -> A C_ B ) )
22 21 com12 
 |-  ( A C_ ( ( _V X. _V ) X. _V ) -> ( A. x A. y A. z ( <. <. x , y >. , z >. e. A -> <. <. x , y >. , z >. e. B ) -> A C_ B ) )
23 3 22 impbid2 
 |-  ( A C_ ( ( _V X. _V ) X. _V ) -> ( A C_ B <-> A. x A. y A. z ( <. <. x , y >. , z >. e. A -> <. <. x , y >. , z >. e. B ) ) )