ordelord

Description: An element of an ordinal class is ordinal. Proposition 7.6 of TakeutiZaring p. 36. Lemma 1.3 of Schloeder p. 1. (Contributed by NM, 23-Apr-1994)

		Ref	Expression
	Assertion	ordelord	$⊢ (Ord A \land B \in A) \to Ord B$

Proof

Step	Hyp	Ref	Expression
1		eleq1	$⊢ x = B \to (x \in A \leftrightarrow B \in A)$
2	1	anbi2d	$⊢ x = B \to ((Ord A \land x \in A) \leftrightarrow (Ord A \land B \in A))$
3		ordeq	$⊢ x = B \to (Ord x \leftrightarrow Ord B)$
4	2 3	imbi12d	$⊢ x = B \to (((Ord A \land x \in A) \to Ord x) \leftrightarrow ((Ord A \land B \in A) \to Ord B))$
5		simpll	$⊢ ((Ord A \land x \in A) \land (z \in y \land y \in x)) \to Ord A$
6		3anrot	$⊢ (x \in A \land z \in y \land y \in x) \leftrightarrow (z \in y \land y \in x \land x \in A)$
7		3anass	$⊢ (x \in A \land z \in y \land y \in x) \leftrightarrow (x \in A \land (z \in y \land y \in x))$
8	6 7	bitr3i	$⊢ (z \in y \land y \in x \land x \in A) \leftrightarrow (x \in A \land (z \in y \land y \in x))$
9		ordtr	$⊢ Ord A \to Tr A$
10		trel3	$⊢ Tr A \to ((z \in y \land y \in x \land x \in A) \to z \in A)$
11	9 10	syl	$⊢ Ord A \to ((z \in y \land y \in x \land x \in A) \to z \in A)$
12	8 11	biimtrrid	$⊢ Ord A \to ((x \in A \land (z \in y \land y \in x)) \to z \in A)$
13	12	impl	$⊢ ((Ord A \land x \in A) \land (z \in y \land y \in x)) \to z \in A$
14		trel	$⊢ Tr A \to ((y \in x \land x \in A) \to y \in A)$
15	9 14	syl	$⊢ Ord A \to ((y \in x \land x \in A) \to y \in A)$
16	15	expcomd	$⊢ Ord A \to (x \in A \to (y \in x \to y \in A))$
17	16	imp31	$⊢ ((Ord A \land x \in A) \land y \in x) \to y \in A$
18	17	adantrl	$⊢ ((Ord A \land x \in A) \land (z \in y \land y \in x)) \to y \in A$
19		simplr	$⊢ ((Ord A \land x \in A) \land (z \in y \land y \in x)) \to x \in A$
20		ordwe	$⊢ Ord A \to E We A$
21		wetrep	$⊢ (E We A \land (z \in A \land y \in A \land x \in A)) \to ((z \in y \land y \in x) \to z \in x)$
22	20 21	sylan	$⊢ (Ord A \land (z \in A \land y \in A \land x \in A)) \to ((z \in y \land y \in x) \to z \in x)$
23	5 13 18 19 22	syl13anc	$⊢ ((Ord A \land x \in A) \land (z \in y \land y \in x)) \to ((z \in y \land y \in x) \to z \in x)$
24	23	ex	$⊢ (Ord A \land x \in A) \to ((z \in y \land y \in x) \to ((z \in y \land y \in x) \to z \in x))$
25	24	pm2.43d	$⊢ (Ord A \land x \in A) \to ((z \in y \land y \in x) \to z \in x)$
26	25	alrimivv	$⊢ (Ord A \land x \in A) \to \forall z \forall y ((z \in y \land y \in x) \to z \in x)$
27		dftr2	$⊢ Tr x \leftrightarrow \forall z \forall y ((z \in y \land y \in x) \to z \in x)$
28	26 27	sylibr	$⊢ (Ord A \land x \in A) \to Tr x$
29		trss	$⊢ Tr A \to (x \in A \to x \subseteq A)$
30	9 29	syl	$⊢ Ord A \to (x \in A \to x \subseteq A)$
31		wess	$⊢ x \subseteq A \to (E We A \to E We x)$
32	30 20 31	syl6ci	$⊢ Ord A \to (x \in A \to E We x)$
33	32	imp	$⊢ (Ord A \land x \in A) \to E We x$
34		df-ord	$⊢ Ord x \leftrightarrow (Tr x \land E We x)$
35	28 33 34	sylanbrc	$⊢ (Ord A \land x \in A) \to Ord x$
36	4 35	vtoclg	$⊢ B \in A \to ((Ord A \land B \in A) \to Ord B)$
37	36	anabsi7	$⊢ (Ord A \land B \in A) \to Ord B$

Metamath Proof Explorer

Theorem ordelord

Proof