Theorem trcoss

Description: Sufficient condition for the transitivity of cosets by R . (Contributed by Peter Mazsa, 26-Dec-2018)

	Ref	Expression
Assertion	trcoss	⊢ ( ∀ 𝑦 ∃* 𝑢 𝑢 𝑅 𝑦 → ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ≀ 𝑅 𝑦 ∧ 𝑦 ≀ 𝑅 𝑧 ) → 𝑥 ≀ 𝑅 𝑧 ) )

Proof

Step	Hyp	Ref	Expression
1		moantr	⊢ ( ∃* 𝑢 𝑢 𝑅 𝑦 → ( ( ∃ 𝑢 ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑅 𝑦 ) ∧ ∃ 𝑢 ( 𝑢 𝑅 𝑦 ∧ 𝑢 𝑅 𝑧 ) ) → ∃ 𝑢 ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑅 𝑧 ) ) )
2		brcoss	⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) → ( 𝑥 ≀ 𝑅 𝑦 ↔ ∃ 𝑢 ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑅 𝑦 ) ) )
3	2	el2v	⊢ ( 𝑥 ≀ 𝑅 𝑦 ↔ ∃ 𝑢 ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑅 𝑦 ) )
4		brcoss	⊢ ( ( 𝑦 ∈ V ∧ 𝑧 ∈ V ) → ( 𝑦 ≀ 𝑅 𝑧 ↔ ∃ 𝑢 ( 𝑢 𝑅 𝑦 ∧ 𝑢 𝑅 𝑧 ) ) )
5	4	el2v	⊢ ( 𝑦 ≀ 𝑅 𝑧 ↔ ∃ 𝑢 ( 𝑢 𝑅 𝑦 ∧ 𝑢 𝑅 𝑧 ) )
6	3 5	anbi12i	⊢ ( ( 𝑥 ≀ 𝑅 𝑦 ∧ 𝑦 ≀ 𝑅 𝑧 ) ↔ ( ∃ 𝑢 ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑅 𝑦 ) ∧ ∃ 𝑢 ( 𝑢 𝑅 𝑦 ∧ 𝑢 𝑅 𝑧 ) ) )
7		brcoss	⊢ ( ( 𝑥 ∈ V ∧ 𝑧 ∈ V ) → ( 𝑥 ≀ 𝑅 𝑧 ↔ ∃ 𝑢 ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑅 𝑧 ) ) )
8	7	el2v	⊢ ( 𝑥 ≀ 𝑅 𝑧 ↔ ∃ 𝑢 ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑅 𝑧 ) )
9	1 6 8	3imtr4g	⊢ ( ∃* 𝑢 𝑢 𝑅 𝑦 → ( ( 𝑥 ≀ 𝑅 𝑦 ∧ 𝑦 ≀ 𝑅 𝑧 ) → 𝑥 ≀ 𝑅 𝑧 ) )
10	9	alrimiv	⊢ ( ∃* 𝑢 𝑢 𝑅 𝑦 → ∀ 𝑧 ( ( 𝑥 ≀ 𝑅 𝑦 ∧ 𝑦 ≀ 𝑅 𝑧 ) → 𝑥 ≀ 𝑅 𝑧 ) )
11	10	alimi	⊢ ( ∀ 𝑦 ∃* 𝑢 𝑢 𝑅 𝑦 → ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ≀ 𝑅 𝑦 ∧ 𝑦 ≀ 𝑅 𝑧 ) → 𝑥 ≀ 𝑅 𝑧 ) )
12	11	alrimiv	⊢ ( ∀ 𝑦 ∃* 𝑢 𝑢 𝑅 𝑦 → ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ≀ 𝑅 𝑦 ∧ 𝑦 ≀ 𝑅 𝑧 ) → 𝑥 ≀ 𝑅 𝑧 ) )