Theorem 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 𝐴 ∧ 𝐵 ∈ 𝐴 ) → Ord 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		eleq1	⊢ ( 𝑥 = 𝐵 → ( 𝑥 ∈ 𝐴 ↔ 𝐵 ∈ 𝐴 ) )
2	1	anbi2d	⊢ ( 𝑥 = 𝐵 → ( ( Ord 𝐴 ∧ 𝑥 ∈ 𝐴 ) ↔ ( Ord 𝐴 ∧ 𝐵 ∈ 𝐴 ) ) )
3		ordeq	⊢ ( 𝑥 = 𝐵 → ( Ord 𝑥 ↔ Ord 𝐵 ) )
4	2 3	imbi12d	⊢ ( 𝑥 = 𝐵 → ( ( ( Ord 𝐴 ∧ 𝑥 ∈ 𝐴 ) → Ord 𝑥 ) ↔ ( ( Ord 𝐴 ∧ 𝐵 ∈ 𝐴 ) → Ord 𝐵 ) ) )
5		simpll	⊢ ( ( ( Ord 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) ) → Ord 𝐴 )
6		3anrot	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) ↔ ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) )
7		3anass	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) ) )
8	6 7	bitr3i	⊢ ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) ) )
9		ordtr	⊢ ( Ord 𝐴 → Tr 𝐴 )
10		trel3	⊢ ( Tr 𝐴 → ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 ) )
11	9 10	syl	⊢ ( Ord 𝐴 → ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 ) )
12	8 11	biimtrrid	⊢ ( Ord 𝐴 → ( ( 𝑥 ∈ 𝐴 ∧ ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) ) → 𝑧 ∈ 𝐴 ) )
13	12	impl	⊢ ( ( ( Ord 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) ) → 𝑧 ∈ 𝐴 )
14		trel	⊢ ( Tr 𝐴 → ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ 𝐴 ) )
15	9 14	syl	⊢ ( Ord 𝐴 → ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ 𝐴 ) )
16	15	expcomd	⊢ ( Ord 𝐴 → ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐴 ) ) )
17	16	imp31	⊢ ( ( ( Ord 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ 𝐴 )
18	17	adantrl	⊢ ( ( ( Ord 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) ) → 𝑦 ∈ 𝐴 )
19		simplr	⊢ ( ( ( Ord 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) ) → 𝑥 ∈ 𝐴 )
20		ordwe	⊢ ( Ord 𝐴 → E We 𝐴 )
21		wetrep	⊢ ( ( E We 𝐴 ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ) → ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) )
22	20 21	sylan	⊢ ( ( Ord 𝐴 ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ) → ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) )
23	5 13 18 19 22	syl13anc	⊢ ( ( ( Ord 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) ) → ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) )
24	23	ex	⊢ ( ( Ord 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) ) )
25	24	pm2.43d	⊢ ( ( Ord 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) )
26	25	alrimivv	⊢ ( ( Ord 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) )
27		dftr2	⊢ ( Tr 𝑥 ↔ ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) )
28	26 27	sylibr	⊢ ( ( Ord 𝐴 ∧ 𝑥 ∈ 𝐴 ) → Tr 𝑥 )
29		trss	⊢ ( Tr 𝐴 → ( 𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐴 ) )
30	9 29	syl	⊢ ( Ord 𝐴 → ( 𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐴 ) )
31		wess	⊢ ( 𝑥 ⊆ 𝐴 → ( E We 𝐴 → E We 𝑥 ) )
32	30 20 31	syl6ci	⊢ ( Ord 𝐴 → ( 𝑥 ∈ 𝐴 → E We 𝑥 ) )
33	32	imp	⊢ ( ( Ord 𝐴 ∧ 𝑥 ∈ 𝐴 ) → E We 𝑥 )
34		df-ord	⊢ ( Ord 𝑥 ↔ ( Tr 𝑥 ∧ E We 𝑥 ) )
35	28 33 34	sylanbrc	⊢ ( ( Ord 𝐴 ∧ 𝑥 ∈ 𝐴 ) → Ord 𝑥 )
36	4 35	vtoclg	⊢ ( 𝐵 ∈ 𝐴 → ( ( Ord 𝐴 ∧ 𝐵 ∈ 𝐴 ) → Ord 𝐵 ) )
37	36	anabsi7	⊢ ( ( Ord 𝐴 ∧ 𝐵 ∈ 𝐴 ) → Ord 𝐵 )