suctrALT2

Description: Virtual deduction proof of suctr . The sucessor of a transitive class is transitive. This proof was generated automatically from the virtual deduction proof suctrALT2VD using the tools command file translate__without__overwriting__minimize__excluding__duplicates.cmd . (Contributed by Alan Sare, 11-Sep-2011) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		sssucid	$⊢ A \subseteq suc A$
2		trel	$⊢ Tr A \to ((z \in y \land y \in A) \to z \in A)$
3	2	expd	$⊢ Tr A \to (z \in y \to (y \in A \to z \in A))$
4	3	adantrd	$⊢ Tr A \to ((z \in y \land y \in suc A) \to (y \in A \to z \in A))$
5		ssel	$⊢ A \subseteq suc A \to (z \in A \to z \in suc A)$
6	1 4 5	ee03	$⊢ Tr A \to ((z \in y \land y \in suc A) \to (y \in A \to z \in suc A))$
7		simpl	$⊢ (z \in y \land y \in suc A) \to z \in y$
8	7	a1i	$⊢ Tr A \to ((z \in y \land y \in suc A) \to z \in y)$
9		eleq2	$⊢ y = A \to (z \in y \leftrightarrow z \in A)$
10	9	biimpcd	$⊢ z \in y \to (y = A \to z \in A)$
11	8 10	syl6	$⊢ Tr A \to ((z \in y \land y \in suc A) \to (y = A \to z \in A))$
12	1 11 5	ee03	$⊢ Tr A \to ((z \in y \land y \in suc A) \to (y = A \to z \in suc A))$
13		simpr	$⊢ (z \in y \land y \in suc A) \to y \in suc A$
14	13	a1i	$⊢ Tr A \to ((z \in y \land y \in suc A) \to y \in suc A)$
15		elsuci	$⊢ y \in suc A \to (y \in A \lor y = A)$
16	14 15	syl6	$⊢ Tr A \to ((z \in y \land y \in suc A) \to (y \in A \lor y = A))$
17		jao	$⊢ (y \in A \to z \in suc A) \to ((y = A \to z \in suc A) \to ((y \in A \lor y = A) \to z \in suc A))$
18	6 12 16 17	ee222	$⊢ Tr A \to ((z \in y \land y \in suc A) \to z \in suc A)$
19	18	alrimivv	$⊢ Tr A \to \forall z \forall y ((z \in y \land y \in suc A) \to z \in suc A)$
20		dftr2	$⊢ Tr suc A \leftrightarrow \forall z \forall y ((z \in y \land y \in suc A) \to z \in suc A)$
21	19 20	sylibr	$⊢ Tr A \to Tr suc A$

Metamath Proof Explorer

Theorem suctrALT2

Proof