This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ≀ ≀ 𝑅 ⊆ 𝑆 ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ≀ 𝑅 𝑦 ∧ 𝑦 ≀ 𝑅 𝑧 ) → 𝑥 𝑆 𝑧 ) )

Proof

Step Hyp Ref Expression
1 relcoss ⊢ Rel ≀ ≀ 𝑅
2 ssrel3 ⊢ ( Rel ≀ ≀ 𝑅 → ( ≀ ≀ 𝑅 ⊆ 𝑆 ↔ ∀ 𝑥 ∀ 𝑧 ( 𝑥 ≀ ≀ 𝑅 𝑧 → 𝑥 𝑆 𝑧 ) ) )
3 1 2 ax-mp ⊢ ( ≀ ≀ 𝑅 ⊆ 𝑆 ↔ ∀ 𝑥 ∀ 𝑧 ( 𝑥 ≀ ≀ 𝑅 𝑧 → 𝑥 𝑆 𝑧 ) )
4 brcoss ⊢ ( ( 𝑥 ∈ V ∧ 𝑧 ∈ V ) → ( 𝑥 ≀ ≀ 𝑅 𝑧 ↔ ∃ 𝑦 ( 𝑦 ≀ 𝑅 𝑥 ∧ 𝑦 ≀ 𝑅 𝑧 ) ) )
5 4 el2v ⊢ ( 𝑥 ≀ ≀ 𝑅 𝑧 ↔ ∃ 𝑦 ( 𝑦 ≀ 𝑅 𝑥 ∧ 𝑦 ≀ 𝑅 𝑧 ) )
6 brcosscnvcoss ⊢ ( ( 𝑦 ∈ V ∧ 𝑥 ∈ V ) → ( 𝑦 ≀ 𝑅 𝑥 ↔ 𝑥 ≀ 𝑅 𝑦 ) )
7 6 el2v ⊢ ( 𝑦 ≀ 𝑅 𝑥 ↔ 𝑥 ≀ 𝑅 𝑦 )
8 7 anbi1i ⊢ ( ( 𝑦 ≀ 𝑅 𝑥 ∧ 𝑦 ≀ 𝑅 𝑧 ) ↔ ( 𝑥 ≀ 𝑅 𝑦 ∧ 𝑦 ≀ 𝑅 𝑧 ) )
9 8 exbii ⊢ ( ∃ 𝑦 ( 𝑦 ≀ 𝑅 𝑥 ∧ 𝑦 ≀ 𝑅 𝑧 ) ↔ ∃ 𝑦 ( 𝑥 ≀ 𝑅 𝑦 ∧ 𝑦 ≀ 𝑅 𝑧 ) )
10 5 9 bitri ⊢ ( 𝑥 ≀ ≀ 𝑅 𝑧 ↔ ∃ 𝑦 ( 𝑥 ≀ 𝑅 𝑦 ∧ 𝑦 ≀ 𝑅 𝑧 ) )
11 10 imbi1i ⊢ ( ( 𝑥 ≀ ≀ 𝑅 𝑧 → 𝑥 𝑆 𝑧 ) ↔ ( ∃ 𝑦 ( 𝑥 ≀ 𝑅 𝑦 ∧ 𝑦 ≀ 𝑅 𝑧 ) → 𝑥 𝑆 𝑧 ) )
12 19.23v ⊢ ( ∀ 𝑦 ( ( 𝑥 ≀ 𝑅 𝑦 ∧ 𝑦 ≀ 𝑅 𝑧 ) → 𝑥 𝑆 𝑧 ) ↔ ( ∃ 𝑦 ( 𝑥 ≀ 𝑅 𝑦 ∧ 𝑦 ≀ 𝑅 𝑧 ) → 𝑥 𝑆 𝑧 ) )
13 11 12 bitr4i ⊢ ( ( 𝑥 ≀ ≀ 𝑅 𝑧 → 𝑥 𝑆 𝑧 ) ↔ ∀ 𝑦 ( ( 𝑥 ≀ 𝑅 𝑦 ∧ 𝑦 ≀ 𝑅 𝑧 ) → 𝑥 𝑆 𝑧 ) )
14 13 albii ⊢ ( ∀ 𝑧 ( 𝑥 ≀ ≀ 𝑅 𝑧 → 𝑥 𝑆 𝑧 ) ↔ ∀ 𝑧 ∀ 𝑦 ( ( 𝑥 ≀ 𝑅 𝑦 ∧ 𝑦 ≀ 𝑅 𝑧 ) → 𝑥 𝑆 𝑧 ) )
15 alcom ⊢ ( ∀ 𝑧 ∀ 𝑦 ( ( 𝑥 ≀ 𝑅 𝑦 ∧ 𝑦 ≀ 𝑅 𝑧 ) → 𝑥 𝑆 𝑧 ) ↔ ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ≀ 𝑅 𝑦 ∧ 𝑦 ≀ 𝑅 𝑧 ) → 𝑥 𝑆 𝑧 ) )
16 14 15 bitri ⊢ ( ∀ 𝑧 ( 𝑥 ≀ ≀ 𝑅 𝑧 → 𝑥 𝑆 𝑧 ) ↔ ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ≀ 𝑅 𝑦 ∧ 𝑦 ≀ 𝑅 𝑧 ) → 𝑥 𝑆 𝑧 ) )
17 16 albii ⊢ ( ∀ 𝑥 ∀ 𝑧 ( 𝑥 ≀ ≀ 𝑅 𝑧 → 𝑥 𝑆 𝑧 ) ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ≀ 𝑅 𝑦 ∧ 𝑦 ≀ 𝑅 𝑧 ) → 𝑥 𝑆 𝑧 ) )
18 3 17 bitri ⊢ ( ≀ ≀ 𝑅 ⊆ 𝑆 ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ≀ 𝑅 𝑦 ∧ 𝑦 ≀ 𝑅 𝑧 ) → 𝑥 𝑆 𝑧 ) )