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⊆I∘B↔Rel⁡A∧A⊆B

Proof

Step Hyp Ref Expression
1 relco ⊢Rel⁡I∘B
2 relss ⊢A⊆I∘B→Rel⁡I∘B→Rel⁡A
3 1 2 mpi ⊢A⊆I∘B→Rel⁡A
4 elrel ⊢Rel⁡A∧x∈A→∃y∃zx=yz
5 vex ⊢y∈V
6 vex ⊢z∈V
7 5 6 brco ⊢yI∘Bz↔∃xyBx∧xIz
8 6 ideq ⊢xIz↔x=z
9 8 anbi1ci ⊢yBx∧xIz↔x=z∧yBx
10 9 exbii ⊢∃xyBx∧xIz↔∃xx=z∧yBx
11 breq2 ⊢x=z→yBx↔yBz
12 11 equsexvw ⊢∃xx=z∧yBx↔yBz
13 7 10 12 3bitri ⊢yI∘Bz↔yBz
14 13 a1i ⊢x=yz→yI∘Bz↔yBz
15 eleq1 ⊢x=yz→x∈I∘B↔yz∈I∘B
16 df-br ⊢yI∘Bz↔yz∈I∘B
17 15 16 bitr4di ⊢x=yz→x∈I∘B↔yI∘Bz
18 eleq1 ⊢x=yz→x∈B↔yz∈B
19 df-br ⊢yBz↔yz∈B
20 18 19 bitr4di ⊢x=yz→x∈B↔yBz
21 14 17 20 3bitr4d ⊢x=yz→x∈I∘B↔x∈B
22 21 exlimivv ⊢∃y∃zx=yz→x∈I∘B↔x∈B
23 4 22 syl ⊢Rel⁡A∧x∈A→x∈I∘B↔x∈B
24 23 pm5.74da ⊢Rel⁡A→x∈A→x∈I∘B↔x∈A→x∈B
25 24 albidv ⊢Rel⁡A→∀xx∈A→x∈I∘B↔∀xx∈A→x∈B
26 dfss2 ⊢A⊆I∘B↔∀xx∈A→x∈I∘B
27 dfss2 ⊢A⊆B↔∀xx∈A→x∈B
28 25 26 27 3bitr4g ⊢Rel⁡A→A⊆I∘B↔A⊆B
29 3 28 biadanii ⊢A⊆I∘B↔Rel⁡A∧A⊆B