# 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 ${⊢}\wr \wr {R}\subseteq {S}↔\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left({x}\wr {R}{y}\wedge {y}\wr {R}{z}\right)\to {x}{S}{z}\right)$

### Proof

Step Hyp Ref Expression
1 relcoss ${⊢}\mathrm{Rel}\wr \wr {R}$
2 ssrel3 ${⊢}\mathrm{Rel}\wr \wr {R}\to \left(\wr \wr {R}\subseteq {S}↔\forall {x}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left({x}\wr \wr {R}{z}\to {x}{S}{z}\right)\right)$
3 1 2 ax-mp ${⊢}\wr \wr {R}\subseteq {S}↔\forall {x}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left({x}\wr \wr {R}{z}\to {x}{S}{z}\right)$
4 brcoss ${⊢}\left({x}\in \mathrm{V}\wedge {z}\in \mathrm{V}\right)\to \left({x}\wr \wr {R}{z}↔\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\wr {R}{x}\wedge {y}\wr {R}{z}\right)\right)$
5 4 el2v ${⊢}{x}\wr \wr {R}{z}↔\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\wr {R}{x}\wedge {y}\wr {R}{z}\right)$
6 brcosscnvcoss ${⊢}\left({y}\in \mathrm{V}\wedge {x}\in \mathrm{V}\right)\to \left({y}\wr {R}{x}↔{x}\wr {R}{y}\right)$
7 6 el2v ${⊢}{y}\wr {R}{x}↔{x}\wr {R}{y}$
8 7 anbi1i ${⊢}\left({y}\wr {R}{x}\wedge {y}\wr {R}{z}\right)↔\left({x}\wr {R}{y}\wedge {y}\wr {R}{z}\right)$
9 8 exbii ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\wr {R}{x}\wedge {y}\wr {R}{z}\right)↔\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}\wr {R}{y}\wedge {y}\wr {R}{z}\right)$
10 5 9 bitri ${⊢}{x}\wr \wr {R}{z}↔\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}\wr {R}{y}\wedge {y}\wr {R}{z}\right)$
11 10 imbi1i ${⊢}\left({x}\wr \wr {R}{z}\to {x}{S}{z}\right)↔\left(\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}\wr {R}{y}\wedge {y}\wr {R}{z}\right)\to {x}{S}{z}\right)$
12 19.23v ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}\wr {R}{y}\wedge {y}\wr {R}{z}\right)\to {x}{S}{z}\right)↔\left(\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}\wr {R}{y}\wedge {y}\wr {R}{z}\right)\to {x}{S}{z}\right)$
13 11 12 bitr4i ${⊢}\left({x}\wr \wr {R}{z}\to {x}{S}{z}\right)↔\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}\wr {R}{y}\wedge {y}\wr {R}{z}\right)\to {x}{S}{z}\right)$
14 13 albii ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}\left({x}\wr \wr {R}{z}\to {x}{S}{z}\right)↔\forall {z}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}\wr {R}{y}\wedge {y}\wr {R}{z}\right)\to {x}{S}{z}\right)$
15 alcom ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}\wr {R}{y}\wedge {y}\wr {R}{z}\right)\to {x}{S}{z}\right)↔\forall {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left({x}\wr {R}{y}\wedge {y}\wr {R}{z}\right)\to {x}{S}{z}\right)$
16 14 15 bitri ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}\left({x}\wr \wr {R}{z}\to {x}{S}{z}\right)↔\forall {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left({x}\wr {R}{y}\wedge {y}\wr {R}{z}\right)\to {x}{S}{z}\right)$
17 16 albii ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left({x}\wr \wr {R}{z}\to {x}{S}{z}\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left({x}\wr {R}{y}\wedge {y}\wr {R}{z}\right)\to {x}{S}{z}\right)$
18 3 17 bitri ${⊢}\wr \wr {R}\subseteq {S}↔\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left({x}\wr {R}{y}\wedge {y}\wr {R}{z}\right)\to {x}{S}{z}\right)$