Metamath Proof Explorer

Theorem cocossss

Description: Two ways of saying that cosets by cosets by R is a subclass. (Contributed by Peter Mazsa, 17-Sep-2021)

Ref Expression
Assertion cocossss ⊢ ≀ ≀ R ⊆ S ↔ ∀ x ∀ y ∀ z x ≀ R y ∧ y ≀ R z → x S z

Proof

Step Hyp Ref Expression
1 relcoss ⊢ Rel ⁡ ≀ ≀ R
2 ssrel3 ⊢ Rel ⁡ ≀ ≀ R → ≀ ≀ R ⊆ S ↔ ∀ x ∀ z x ≀ ≀ R z → x S z
3 1 2 ax-mp ⊢ ≀ ≀ R ⊆ S ↔ ∀ x ∀ z x ≀ ≀ R z → x S z
4 brcoss ⊢ x ∈ V ∧ z ∈ V → x ≀ ≀ R z ↔ ∃ y y ≀ R x ∧ y ≀ R z
5 4 el2v ⊢ x ≀ ≀ R z ↔ ∃ y y ≀ R x ∧ y ≀ R z
6 brcosscnvcoss ⊢ y ∈ V ∧ x ∈ V → y ≀ R x ↔ x ≀ R y
7 6 el2v ⊢ y ≀ R x ↔ x ≀ R y
8 7 anbi1i ⊢ y ≀ R x ∧ y ≀ R z ↔ x ≀ R y ∧ y ≀ R z
9 8 exbii ⊢ ∃ y y ≀ R x ∧ y ≀ R z ↔ ∃ y x ≀ R y ∧ y ≀ R z
10 5 9 bitri ⊢ x ≀ ≀ R z ↔ ∃ y x ≀ R y ∧ y ≀ R z
11 10 imbi1i ⊢ x ≀ ≀ R z → x S z ↔ ∃ y x ≀ R y ∧ y ≀ R z → x S z
12 19.23v ⊢ ∀ y x ≀ R y ∧ y ≀ R z → x S z ↔ ∃ y x ≀ R y ∧ y ≀ R z → x S z
13 11 12 bitr4i ⊢ x ≀ ≀ R z → x S z ↔ ∀ y x ≀ R y ∧ y ≀ R z → x S z
14 13 albii ⊢ ∀ z x ≀ ≀ R z → x S z ↔ ∀ z ∀ y x ≀ R y ∧ y ≀ R z → x S z
15 alcom ⊢ ∀ z ∀ y x ≀ R y ∧ y ≀ R z → x S z ↔ ∀ y ∀ z x ≀ R y ∧ y ≀ R z → x S z
16 14 15 bitri ⊢ ∀ z x ≀ ≀ R z → x S z ↔ ∀ y ∀ z x ≀ R y ∧ y ≀ R z → x S z
17 16 albii ⊢ ∀ x ∀ z x ≀ ≀ R z → x S z ↔ ∀ x ∀ y ∀ z x ≀ R y ∧ y ≀ R z → x S z
18 3 17 bitri ⊢ ≀ ≀ R ⊆ S ↔ ∀ x ∀ y ∀ z x ≀ R y ∧ y ≀ R z → x S z