Theorem eltrrels3

Description: Element of the class of transitive relations. (Contributed by Peter Mazsa, 22-Aug-2021)

	Ref	Expression
Assertion	eltrrels3	⊢ ( 𝑅 ∈ TrRels ↔ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ∧ 𝑅 ∈ Rels ) )

Proof

Step	Hyp	Ref	Expression
1		dftrrels3	⊢ TrRels = { 𝑟 ∈ Rels ∣ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) }
2		breq	⊢ ( 𝑟 = 𝑅 → ( 𝑥 𝑟 𝑦 ↔ 𝑥 𝑅 𝑦 ) )
3		breq	⊢ ( 𝑟 = 𝑅 → ( 𝑦 𝑟 𝑧 ↔ 𝑦 𝑅 𝑧 ) )
4	2 3	anbi12d	⊢ ( 𝑟 = 𝑅 → ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) ↔ ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) ) )
5		breq	⊢ ( 𝑟 = 𝑅 → ( 𝑥 𝑟 𝑧 ↔ 𝑥 𝑅 𝑧 ) )
6	4 5	imbi12d	⊢ ( 𝑟 = 𝑅 → ( ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ↔ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) )
7	6	2albidv	⊢ ( 𝑟 = 𝑅 → ( ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ↔ ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) )
8	7	albidv	⊢ ( 𝑟 = 𝑅 → ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) )
9	1 8	rabeqel	⊢ ( 𝑅 ∈ TrRels ↔ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ∧ 𝑅 ∈ Rels ) )