Metamath Proof Explorer

Theorem cocnv2ss

Description: Characterizing when the composition of a class with a converse is included in another. (Contributed by BJ, 22-Oct-2026)

Ref Expression
Assertion cocnv2ss ⊢ B ∘ A -1 ⊆ C ↔ ∀ x ∀ y ∀ z y A x ∧ y B z → x C z

Proof

Step Hyp Ref Expression
1 cotrg ⊢ B ∘ A -1 ⊆ C ↔ ∀ x ∀ y ∀ z x A -1 y ∧ y B z → x C z
2 vex ⊢ x ∈ V
3 vex ⊢ y ∈ V
4 2 3 brcnv ⊢ x A -1 y ↔ y A x
5 4 anbi1i ⊢ x A -1 y ∧ y B z ↔ y A x ∧ y B z
6 5 imbi1i ⊢ x A -1 y ∧ y B z → x C z ↔ y A x ∧ y B z → x C z
7 6 3albii ⊢ ∀ x ∀ y ∀ z x A -1 y ∧ y B z → x C z ↔ ∀ x ∀ y ∀ z y A x ∧ y B z → x C z
8 1 7 bitri ⊢ B ∘ A -1 ⊆ C ↔ ∀ x ∀ y ∀ z y A x ∧ y B z → x C z