Metamath Proof Explorer

Theorem cnvssco

Description: A condition weaker than reflexivity. (Contributed by RP, 3-Aug-2020)

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

Proof

Step Hyp Ref Expression
1 alcom ⊢ ∀ y ∀ x y x ∈ A -1 → y x ∈ B ∘ C -1 ↔ ∀ x ∀ y y x ∈ A -1 → y x ∈ B ∘ C -1
2 relcnv ⊢ Rel ⁡ A -1
3 ssrel ⊢ Rel ⁡ A -1 → A -1 ⊆ B ∘ C -1 ↔ ∀ y ∀ x y x ∈ A -1 → y x ∈ B ∘ C -1
4 2 3 ax-mp ⊢ A -1 ⊆ B ∘ C -1 ↔ ∀ y ∀ x y x ∈ A -1 → y x ∈ B ∘ C -1
5 19.37v ⊢ ∃ z x A y → x C z ∧ z B y ↔ x A y → ∃ z x C z ∧ z B y
6 vex ⊢ y ∈ V
7 vex ⊢ x ∈ V
8 6 7 brcnv ⊢ y A -1 x ↔ x A y
9 df-br ⊢ y A -1 x ↔ y x ∈ A -1
10 8 9 bitr3i ⊢ x A y ↔ y x ∈ A -1
11 7 6 brco ⊢ x B ∘ C y ↔ ∃ z x C z ∧ z B y
12 6 7 brcnv ⊢ y B ∘ C -1 x ↔ x B ∘ C y
13 df-br ⊢ y B ∘ C -1 x ↔ y x ∈ B ∘ C -1
14 12 13 bitr3i ⊢ x B ∘ C y ↔ y x ∈ B ∘ C -1
15 11 14 bitr3i ⊢ ∃ z x C z ∧ z B y ↔ y x ∈ B ∘ C -1
16 10 15 imbi12i ⊢ x A y → ∃ z x C z ∧ z B y ↔ y x ∈ A -1 → y x ∈ B ∘ C -1
17 5 16 bitri ⊢ ∃ z x A y → x C z ∧ z B y ↔ y x ∈ A -1 → y x ∈ B ∘ C -1
18 17 2albii ⊢ ∀ x ∀ y ∃ z x A y → x C z ∧ z B y ↔ ∀ x ∀ y y x ∈ A -1 → y x ∈ B ∘ C -1
19 1 4 18 3bitr4i ⊢ A -1 ⊆ B ∘ C -1 ↔ ∀ x ∀ y ∃ z x A y → x C z ∧ z B y