suctrALT3

Description: The successor of a transitive class is transitive. suctrALT3 is the completed proof in conventional notation of the Virtual Deduction proof https://us.metamath.org/other/completeusersproof/suctralt3vd.html . It was completed manually. The potential for automated derivation from the VD proof exists. See wvd1 for a description of Virtual Deduction. Some sub-theorems of the proof were completed using a unification deduction (e.g., the sub-theorem whose assertion is step 19 used jaoded ). Unification deductions employ Mario Carneiro's metavariable concept. Some sub-theorems were completed using a unification theorem (e.g., the sub-theorem whose assertion is step 24 used dftr2 ) . (Contributed by Alan Sare, 3-Dec-2015) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	suctrALT3	$⊢ 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	2 4 5	trelded	$⊢ (Tr A \land (z \in y \land y \in suc A) \land y \in A) \to z \in A$
7	1 6	sseldi	$⊢ (Tr A \land (z \in y \land y \in suc A) \land y \in A) \to z \in suc A$
8	7	3expia	$⊢ (Tr A \land (z \in y \land y \in suc A)) \to (y \in A \to z \in suc A)$
9		id	$⊢ y = A \to y = A$
10		eleq2	$⊢ y = A \to (z \in y \leftrightarrow z \in A)$
11	10	biimpac	$⊢ (z \in y \land y = A) \to z \in A$
12	4 9 11	syl2an	$⊢ ((z \in y \land y \in suc A) \land y = A) \to z \in A$
13	1 12	sseldi	$⊢ ((z \in y \land y \in suc A) \land y = A) \to z \in suc A$
14	13	ex	$⊢ (z \in y \land y \in suc A) \to (y = A \to z \in suc A)$
15	3	simprd	$⊢ (z \in y \land y \in suc A) \to y \in suc A$
16		elsuci	$⊢ y \in suc A \to (y \in A \lor y = A)$
17	15 16	syl	$⊢ (z \in y \land y \in suc A) \to (y \in A \lor y = A)$
18	8 14 17	jaoded	$⊢ ((Tr A \land (z \in y \land y \in suc A)) \land (z \in y \land y \in suc A) \land (z \in y \land y \in suc A)) \to z \in suc A$
19	18	un2122	$⊢ (Tr A \land (z \in y \land y \in suc A)) \to z \in suc A$
20	19	ex	$⊢ Tr A \to ((z \in y \land y \in suc A) \to z \in suc A)$
21	20	alrimivv	$⊢ Tr A \to \forall z \forall y ((z \in y \land y \in suc A) \to z \in suc A)$
22		dftr2	$⊢ Tr suc A \leftrightarrow \forall z \forall y ((z \in y \land y \in suc A) \to z \in suc A)$
23	22	biimpri	$⊢ \forall z \forall y ((z \in y \land y \in suc A) \to z \in suc A) \to Tr suc A$
24	21 23	syl	$⊢ Tr A \to Tr suc A$
25	24	idiALT	$⊢ Tr A \to Tr suc A$

Metamath Proof Explorer

Theorem suctrALT3

Proof