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

Metamath Proof Explorer

Theorem sscoid

Description: A condition for subset and composition with identity. (Contributed by Scott Fenton, 13-Apr-2018)

Ref Expression
Assertion sscoid 
|- ( A C_ ( _I o. B ) <-> ( Rel A /\ A C_ B ) )

Proof

Step Hyp Ref Expression
1 relco 
 |-  Rel ( _I o. B )
2 relss 
 |-  ( A C_ ( _I o. B ) -> ( Rel ( _I o. B ) -> Rel A ) )
3 1 2 mpi 
 |-  ( A C_ ( _I o. B ) -> Rel A )
4 elrel 
 |-  ( ( Rel A /\ x e. A ) -> E. y E. z x = <. y , z >. )
5 vex 
 |-  y e. _V
6 vex 
 |-  z e. _V
7 5 6 brco 
 |-  ( y ( _I o. B ) z <-> E. x ( y B x /\ x _I z ) )
8 6 ideq 
 |-  ( x _I z <-> x = z )
9 8 anbi1ci 
 |-  ( ( y B x /\ x _I z ) <-> ( x = z /\ y B x ) )
10 9 exbii 
 |-  ( E. x ( y B x /\ x _I z ) <-> E. x ( x = z /\ y B x ) )
11 breq2 
 |-  ( x = z -> ( y B x <-> y B z ) )
12 11 equsexvw 
 |-  ( E. x ( x = z /\ y B x ) <-> y B z )
13 7 10 12 3bitri 
 |-  ( y ( _I o. B ) z <-> y B z )
14 13 a1i 
 |-  ( x = <. y , z >. -> ( y ( _I o. B ) z <-> y B z ) )
15 eleq1 
 |-  ( x = <. y , z >. -> ( x e. ( _I o. B ) <-> <. y , z >. e. ( _I o. B ) ) )
16 df-br 
 |-  ( y ( _I o. B ) z <-> <. y , z >. e. ( _I o. B ) )
17 15 16 bitr4di 
 |-  ( x = <. y , z >. -> ( x e. ( _I o. B ) <-> y ( _I o. B ) z ) )
18 eleq1 
 |-  ( x = <. y , z >. -> ( x e. B <-> <. y , z >. e. B ) )
19 df-br 
 |-  ( y B z <-> <. y , z >. e. B )
20 18 19 bitr4di 
 |-  ( x = <. y , z >. -> ( x e. B <-> y B z ) )
21 14 17 20 3bitr4d 
 |-  ( x = <. y , z >. -> ( x e. ( _I o. B ) <-> x e. B ) )
22 21 exlimivv 
 |-  ( E. y E. z x = <. y , z >. -> ( x e. ( _I o. B ) <-> x e. B ) )
23 4 22 syl 
 |-  ( ( Rel A /\ x e. A ) -> ( x e. ( _I o. B ) <-> x e. B ) )
24 23 pm5.74da 
 |-  ( Rel A -> ( ( x e. A -> x e. ( _I o. B ) ) <-> ( x e. A -> x e. B ) ) )
25 24 albidv 
 |-  ( Rel A -> ( A. x ( x e. A -> x e. ( _I o. B ) ) <-> A. x ( x e. A -> x e. B ) ) )
26 df-ss 
 |-  ( A C_ ( _I o. B ) <-> A. x ( x e. A -> x e. ( _I o. B ) ) )
27 df-ss 
 |-  ( A C_ B <-> A. x ( x e. A -> x e. B ) )
28 25 26 27 3bitr4g 
 |-  ( Rel A -> ( A C_ ( _I o. B ) <-> A C_ B ) )
29 3 28 biadanii 
 |-  ( A C_ ( _I o. B ) <-> ( Rel A /\ A C_ B ) )