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 dfss2
 |-  ( A C_ ( _I o. B ) <-> A. x ( x e. A -> x e. ( _I o. B ) ) )
27 dfss2
 |-  ( 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 ) )