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	⊢ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ≀ 𝑅 𝑦 ∧ 𝑦 ≀ 𝑅 𝑧 ) → 𝑥 ≀ 𝑅 𝑧 ) ↔ ∀ 𝑥 ∀ 𝑧 ( ( [ 𝑥 ] ≀ 𝑅 ∩ [ 𝑧 ] ≀ 𝑅 ) ≠ ∅ → ( [ 𝑥 ] ◡ 𝑅 ∩ [ 𝑧 ] ◡ 𝑅 ) ≠ ∅ ) )