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