suctr

Description: The successor of a transitive class is transitive. (Contributed by Alan Sare, 11-Apr-2009) (Proof shortened by JJ, 24-Sep-2021)

		Ref	Expression
	Assertion	suctr	$⊢ Tr A \to Tr suc A$

Step	Hyp	Ref	Expression
1		elsuci	$⊢ y \in suc A \to (y \in A \lor y = A)$
2		trel	$⊢ Tr A \to ((z \in y \land y \in A) \to z \in A)$
3	2	expdimp	$⊢ (Tr A \land z \in y) \to (y \in A \to z \in A)$
4		eleq2	$⊢ y = A \to (z \in y \leftrightarrow z \in A)$
5	4	biimpcd	$⊢ z \in y \to (y = A \to z \in A)$
6	5	adantl	$⊢ (Tr A \land z \in y) \to (y = A \to z \in A)$
7	3 6	jaod	$⊢ (Tr A \land z \in y) \to ((y \in A \lor y = A) \to z \in A)$
8	1 7	syl5	$⊢ (Tr A \land z \in y) \to (y \in suc A \to z \in A)$
9	8	expimpd	$⊢ Tr A \to ((z \in y \land y \in suc A) \to z \in A)$
10		elelsuc	$⊢ z \in A \to z \in suc A$
11	9 10	syl6	$⊢ Tr A \to ((z \in y \land y \in suc A) \to z \in suc A)$
12	11	alrimivv	$⊢ Tr A \to \forall z \forall y ((z \in y \land y \in suc A) \to z \in suc A)$
13		dftr2	$⊢ Tr suc A \leftrightarrow \forall z \forall y ((z \in y \land y \in suc A) \to z \in suc A)$
14	12 13	sylibr	$⊢ Tr A \to Tr suc A$

Metamath Proof Explorer