Theorem wetrep

Description: On a class well-ordered by membership, the membership predicate is transitive. (Contributed by NM, 22-Apr-1994)

	Ref	Expression
Assertion	wetrep	⊢ ( ( E We 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑧 ) → 𝑥 ∈ 𝑧 ) )

Proof

Step	Hyp	Ref	Expression
1		weso	⊢ ( E We 𝐴 → E Or 𝐴 )
2		sotr	⊢ ( ( E Or 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ( ( 𝑥 E 𝑦 ∧ 𝑦 E 𝑧 ) → 𝑥 E 𝑧 ) )
3	1 2	sylan	⊢ ( ( E We 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ( ( 𝑥 E 𝑦 ∧ 𝑦 E 𝑧 ) → 𝑥 E 𝑧 ) )
4		epel	⊢ ( 𝑥 E 𝑦 ↔ 𝑥 ∈ 𝑦 )
5		epel	⊢ ( 𝑦 E 𝑧 ↔ 𝑦 ∈ 𝑧 )
6	4 5	anbi12i	⊢ ( ( 𝑥 E 𝑦 ∧ 𝑦 E 𝑧 ) ↔ ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑧 ) )
7		epel	⊢ ( 𝑥 E 𝑧 ↔ 𝑥 ∈ 𝑧 )
8	3 6 7	3imtr3g	⊢ ( ( E We 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑧 ) → 𝑥 ∈ 𝑧 ) )