suctrALTcf

Description: The sucessor of a transitive class is transitive. suctrALTcf , using conventional notation, was translated from virtual deduction form, suctrALTcfVD , using a translation program. (Contributed by Alan Sare, 13-Jun-2015) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	suctrALTcf	$⊢ 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		simpl	$⊢ (z \in y \land y \in suc A) \to z \in y$
5	3 4	syl	$⊢ (z \in y \land y \in suc A) \to z \in y$
6		id	$⊢ y \in A \to y \in A$
7		trel	$⊢ Tr A \to ((z \in y \land y \in A) \to z \in A)$
8	7	3impib	$⊢ (Tr A \land z \in y \land y \in A) \to z \in A$
9	2 5 6 8	syl3an	$⊢ (Tr A \land (z \in y \land y \in suc A) \land y \in A) \to z \in A$
10		ssel2	$⊢ (A \subseteq suc A \land z \in A) \to z \in suc A$
11	1 9 10	eel0321old	$⊢ (Tr A \land (z \in y \land y \in suc A) \land y \in A) \to z \in suc A$
12	11	3expia	$⊢ (Tr A \land (z \in y \land y \in suc A)) \to (y \in A \to z \in suc A)$
13		id	$⊢ y = A \to y = A$
14		eleq2	$⊢ y = A \to (z \in y \leftrightarrow z \in A)$
15	14	biimpac	$⊢ (z \in y \land y = A) \to z \in A$
16	5 13 15	syl2an	$⊢ ((z \in y \land y \in suc A) \land y = A) \to z \in A$
17	1 16 10	eel021old	$⊢ ((z \in y \land y \in suc A) \land y = A) \to z \in suc A$
18	17	ex	$⊢ (z \in y \land y \in suc A) \to (y = A \to z \in suc A)$
19		simpr	$⊢ (z \in y \land y \in suc A) \to y \in suc A$
20	3 19	syl	$⊢ (z \in y \land y \in suc A) \to y \in suc A$
21		elsuci	$⊢ y \in suc A \to (y \in A \lor y = A)$
22	20 21	syl	$⊢ (z \in y \land y \in suc A) \to (y \in A \lor y = A)$
23		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))$
24	23	3imp	$⊢ ((y \in A \to z \in suc A) \land (y = A \to z \in suc A) \land (y \in A \lor y = A)) \to z \in suc A$
25	12 18 22 24	eel2122old	$⊢ (Tr A \land (z \in y \land y \in suc A)) \to z \in suc A$
26	25	ex	$⊢ Tr A \to ((z \in y \land y \in suc A) \to z \in suc A)$
27	26	alrimivv	$⊢ Tr A \to \forall z \forall y ((z \in y \land y \in suc A) \to z \in suc A)$
28		dftr2	$⊢ Tr suc A \leftrightarrow \forall z \forall y ((z \in y \land y \in suc A) \to z \in suc A)$
29	28	biimpri	$⊢ \forall z \forall y ((z \in y \land y \in suc A) \to z \in suc A) \to Tr suc A$
30	27 29	syl	$⊢ Tr A \to Tr suc A$
31	30	iin1	$⊢ Tr A \to Tr suc A$

Metamath Proof Explorer

Theorem suctrALTcf

Proof