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

Metamath Proof Explorer

Theorem trcoss2

Description: Equivalent expressions for the transitivity of cosets by R . (Contributed by Peter Mazsa, 4-Jul-2020) (Revised by Peter Mazsa, 16-Oct-2021)

Ref Expression
Assertion trcoss2 ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ≀ 𝑅 𝑦 ∧ 𝑦 ≀ 𝑅 𝑧 ) → 𝑥 ≀ 𝑅 𝑧 ) ↔ ∀ 𝑥 ∀ 𝑧 ( ( [ 𝑥 ] ≀ 𝑅 ∩ [ 𝑧 ] ≀ 𝑅 ) ≠ ∅ → ( [ 𝑥 ] ◡ 𝑅 ∩ [ 𝑧 ] ◡ 𝑅 ) ≠ ∅ ) )

Proof

Step Hyp Ref Expression
1 alcom ⊢ ( ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ≀ 𝑅 𝑦 ∧ 𝑦 ≀ 𝑅 𝑧 ) → 𝑥 ≀ 𝑅 𝑧 ) ↔ ∀ 𝑧 ∀ 𝑦 ( ( 𝑥 ≀ 𝑅 𝑦 ∧ 𝑦 ≀ 𝑅 𝑧 ) → 𝑥 ≀ 𝑅 𝑧 ) )
2 1 albii ⊢ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ≀ 𝑅 𝑦 ∧ 𝑦 ≀ 𝑅 𝑧 ) → 𝑥 ≀ 𝑅 𝑧 ) ↔ ∀ 𝑥 ∀ 𝑧 ∀ 𝑦 ( ( 𝑥 ≀ 𝑅 𝑦 ∧ 𝑦 ≀ 𝑅 𝑧 ) → 𝑥 ≀ 𝑅 𝑧 ) )
3 19.23v ⊢ ( ∀ 𝑦 ( 𝑦 ∈ ( [ 𝑥 ] ≀ 𝑅 ∩ [ 𝑧 ] ≀ 𝑅 ) → ( [ 𝑥 ] ◡ 𝑅 ∩ [ 𝑧 ] ◡ 𝑅 ) ≠ ∅ ) ↔ ( ∃ 𝑦 𝑦 ∈ ( [ 𝑥 ] ≀ 𝑅 ∩ [ 𝑧 ] ≀ 𝑅 ) → ( [ 𝑥 ] ◡ 𝑅 ∩ [ 𝑧 ] ◡ 𝑅 ) ≠ ∅ ) )
4 eleccossin ⊢ ( ( 𝑦 ∈ V ∧ 𝑧 ∈ V ) → ( 𝑦 ∈ ( [ 𝑥 ] ≀ 𝑅 ∩ [ 𝑧 ] ≀ 𝑅 ) ↔ ( 𝑥 ≀ 𝑅 𝑦 ∧ 𝑦 ≀ 𝑅 𝑧 ) ) )
5 4 el2v ⊢ ( 𝑦 ∈ ( [ 𝑥 ] ≀ 𝑅 ∩ [ 𝑧 ] ≀ 𝑅 ) ↔ ( 𝑥 ≀ 𝑅 𝑦 ∧ 𝑦 ≀ 𝑅 𝑧 ) )
6 5 bicomi ⊢ ( ( 𝑥 ≀ 𝑅 𝑦 ∧ 𝑦 ≀ 𝑅 𝑧 ) ↔ 𝑦 ∈ ( [ 𝑥 ] ≀ 𝑅 ∩ [ 𝑧 ] ≀ 𝑅 ) )
7 brcoss3 ⊢ ( ( 𝑥 ∈ V ∧ 𝑧 ∈ V ) → ( 𝑥 ≀ 𝑅 𝑧 ↔ ( [ 𝑥 ] ◡ 𝑅 ∩ [ 𝑧 ] ◡ 𝑅 ) ≠ ∅ ) )
8 7 el2v ⊢ ( 𝑥 ≀ 𝑅 𝑧 ↔ ( [ 𝑥 ] ◡ 𝑅 ∩ [ 𝑧 ] ◡ 𝑅 ) ≠ ∅ )
9 6 8 imbi12i ⊢ ( ( ( 𝑥 ≀ 𝑅 𝑦 ∧ 𝑦 ≀ 𝑅 𝑧 ) → 𝑥 ≀ 𝑅 𝑧 ) ↔ ( 𝑦 ∈ ( [ 𝑥 ] ≀ 𝑅 ∩ [ 𝑧 ] ≀ 𝑅 ) → ( [ 𝑥 ] ◡ 𝑅 ∩ [ 𝑧 ] ◡ 𝑅 ) ≠ ∅ ) )
10 9 albii ⊢ ( ∀ 𝑦 ( ( 𝑥 ≀ 𝑅 𝑦 ∧ 𝑦 ≀ 𝑅 𝑧 ) → 𝑥 ≀ 𝑅 𝑧 ) ↔ ∀ 𝑦 ( 𝑦 ∈ ( [ 𝑥 ] ≀ 𝑅 ∩ [ 𝑧 ] ≀ 𝑅 ) → ( [ 𝑥 ] ◡ 𝑅 ∩ [ 𝑧 ] ◡ 𝑅 ) ≠ ∅ ) )
11 n0 ⊢ ( ( [ 𝑥 ] ≀ 𝑅 ∩ [ 𝑧 ] ≀ 𝑅 ) ≠ ∅ ↔ ∃ 𝑦 𝑦 ∈ ( [ 𝑥 ] ≀ 𝑅 ∩ [ 𝑧 ] ≀ 𝑅 ) )
12 11 imbi1i ⊢ ( ( ( [ 𝑥 ] ≀ 𝑅 ∩ [ 𝑧 ] ≀ 𝑅 ) ≠ ∅ → ( [ 𝑥 ] ◡ 𝑅 ∩ [ 𝑧 ] ◡ 𝑅 ) ≠ ∅ ) ↔ ( ∃ 𝑦 𝑦 ∈ ( [ 𝑥 ] ≀ 𝑅 ∩ [ 𝑧 ] ≀ 𝑅 ) → ( [ 𝑥 ] ◡ 𝑅 ∩ [ 𝑧 ] ◡ 𝑅 ) ≠ ∅ ) )
13 3 10 12 3bitr4i ⊢ ( ∀ 𝑦 ( ( 𝑥 ≀ 𝑅 𝑦 ∧ 𝑦 ≀ 𝑅 𝑧 ) → 𝑥 ≀ 𝑅 𝑧 ) ↔ ( ( [ 𝑥 ] ≀ 𝑅 ∩ [ 𝑧 ] ≀ 𝑅 ) ≠ ∅ → ( [ 𝑥 ] ◡ 𝑅 ∩ [ 𝑧 ] ◡ 𝑅 ) ≠ ∅ ) )
14 13 2albii ⊢ ( ∀ 𝑥 ∀ 𝑧 ∀ 𝑦 ( ( 𝑥 ≀ 𝑅 𝑦 ∧ 𝑦 ≀ 𝑅 𝑧 ) → 𝑥 ≀ 𝑅 𝑧 ) ↔ ∀ 𝑥 ∀ 𝑧 ( ( [ 𝑥 ] ≀ 𝑅 ∩ [ 𝑧 ] ≀ 𝑅 ) ≠ ∅ → ( [ 𝑥 ] ◡ 𝑅 ∩ [ 𝑧 ] ◡ 𝑅 ) ≠ ∅ ) )
15 2 14 bitri ⊢ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ≀ 𝑅 𝑦 ∧ 𝑦 ≀ 𝑅 𝑧 ) → 𝑥 ≀ 𝑅 𝑧 ) ↔ ∀ 𝑥 ∀ 𝑧 ( ( [ 𝑥 ] ≀ 𝑅 ∩ [ 𝑧 ] ≀ 𝑅 ) ≠ ∅ → ( [ 𝑥 ] ◡ 𝑅 ∩ [ 𝑧 ] ◡ 𝑅 ) ≠ ∅ ) )