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

Metamath Proof Explorer

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 ⊢ ( ∀ 𝑦 ∃* 𝑢 𝑢 𝑅 𝑦 → ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ≀ 𝑅 𝑦 ∧ 𝑦 ≀ 𝑅 𝑧 ) → 𝑥 ≀ 𝑅 𝑧 ) )