This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐵 )