suctrALT

Description: The successor of a transitive class is transitive. The proof of https://us.metamath.org/other/completeusersproof/suctrvd.html is a Virtual Deduction proof verified by automatically transforming it into the Metamath proof of suctrALT using completeusersproof, which is verified by the Metamath program. The proof of https://us.metamath.org/other/completeusersproof/suctrro.html is a form of the completed proof which preserves the Virtual Deduction proof's step numbers and their ordering. See suctr for the original proof. (Contributed by Alan Sare, 11-Apr-2009) (Revised by Alan Sare, 12-Jun-2018) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		sssucid	$⊢ A \subseteq suc A$
2		id	$⊢ Tr A \to Tr A$
3		id	$⊢ (z \in y \land y \in suc A) \to (z \in y \land y \in suc A)$
4	3	simpld	$⊢ (z \in y \land y \in suc A) \to z \in y$
5		id	$⊢ y \in A \to y \in A$
6		trel	$⊢ Tr A \to ((z \in y \land y \in A) \to z \in A)$
7	6	3impib	$⊢ (Tr A \land z \in y \land y \in A) \to z \in A$
8	7	idiALT	$⊢ (Tr A \land z \in y \land y \in A) \to z \in A$
9	2 4 5 8	syl3an	$⊢ (Tr A \land (z \in y \land y \in suc A) \land y \in A) \to z \in A$
10	1 9	sselid	$⊢ (Tr A \land (z \in y \land y \in suc A) \land y \in A) \to z \in suc A$
11	10	3expia	$⊢ (Tr A \land (z \in y \land y \in suc A)) \to (y \in A \to z \in suc A)$
12	4	adantr	$⊢ ((z \in y \land y \in suc A) \land y = A) \to z \in y$
13		id	$⊢ y = A \to y = A$
14	13	adantl	$⊢ ((z \in y \land y \in suc A) \land y = A) \to y = A$
15	12 14	eleqtrd	$⊢ ((z \in y \land y \in suc A) \land y = A) \to z \in A$
16	1 15	sselid	$⊢ ((z \in y \land y \in suc A) \land y = A) \to z \in suc A$
17	16	ex	$⊢ (z \in y \land y \in suc A) \to (y = A \to z \in suc A)$
18	17	adantl	$⊢ (Tr A \land (z \in y \land y \in suc A)) \to (y = A \to z \in suc A)$
19	3	simprd	$⊢ (z \in y \land y \in suc A) \to y \in suc A$
20		elsuci	$⊢ y \in suc A \to (y \in A \lor y = A)$
21	19 20	syl	$⊢ (z \in y \land y \in suc A) \to (y \in A \lor y = A)$
22	21	adantl	$⊢ (Tr A \land (z \in y \land y \in suc A)) \to (y \in A \lor y = A)$
23	11 18 22	mpjaod	$⊢ (Tr A \land (z \in y \land y \in suc A)) \to z \in suc A$
24	23	ex	$⊢ Tr A \to ((z \in y \land y \in suc A) \to z \in suc A)$
25	24	alrimivv	$⊢ Tr A \to \forall z \forall y ((z \in y \land y \in suc A) \to z \in suc A)$
26		dftr2	$⊢ Tr suc A \leftrightarrow \forall z \forall y ((z \in y \land y \in suc A) \to z \in suc A)$
27	26	biimpri	$⊢ \forall z \forall y ((z \in y \land y \in suc A) \to z \in suc A) \to Tr suc A$
28	25 27	syl	$⊢ Tr A \to Tr suc A$

Metamath Proof Explorer

Theorem suctrALT

Proof