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 ∃ z x = y z
5 vex ⊢ y ∈ V
6 vex ⊢ z ∈ V
7 5 6 brco ⊢ y I ∘ B z ↔ ∃ 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 ⊢ ∃ x y B x ∧ x I z ↔ ∃ x x = z ∧ y B x
11 breq2 ⊢ x = z → y B x ↔ y B z
12 11 equsexvw ⊢ ∃ x x = z ∧ y B x ↔ y B z
13 7 10 12 3bitri ⊢ y I ∘ B z ↔ y B z
14 13 a1i ⊢ x = y z → y I ∘ B z ↔ y B z
15 eleq1 ⊢ x = y z → x ∈ I ∘ B ↔ y z ∈ I ∘ B
16 df-br ⊢ y I ∘ B z ↔ y z ∈ I ∘ B
17 15 16 bitr4di ⊢ x = y z → x ∈ I ∘ B ↔ y I ∘ B z
18 eleq1 ⊢ x = y z → x ∈ B ↔ y z ∈ B
19 df-br ⊢ y B z ↔ y z ∈ B
20 18 19 bitr4di ⊢ x = y z → x ∈ B ↔ y B z
21 14 17 20 3bitr4d ⊢ x = y z → x ∈ I ∘ B ↔ x ∈ B
22 21 exlimivv ⊢ ∃ y ∃ z x = y z → 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 → ∀ x x ∈ A → x ∈ I ∘ B ↔ ∀ x x ∈ A → x ∈ B
26 df-ss ⊢ A ⊆ I ∘ B ↔ ∀ x x ∈ A → x ∈ I ∘ B
27 df-ss ⊢ A ⊆ B ↔ ∀ x x ∈ 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