Theorem dftrrel3

Description: Alternate definition of the transitive relation predicate. (Contributed by Peter Mazsa, 22-Aug-2021)

	Ref	Expression
Assertion	dftrrel3	⊢ ( TrRel 𝑅 ↔ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ∧ Rel 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		dftrrel2	⊢ ( TrRel 𝑅 ↔ ( ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ∧ Rel 𝑅 ) )
2		cotr	⊢ ( ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) )
3	2	anbi1i	⊢ ( ( ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ∧ Rel 𝑅 ) ↔ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ∧ Rel 𝑅 ) )
4	1 3	bitri	⊢ ( TrRel 𝑅 ↔ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ∧ Rel 𝑅 ) )