Theorem ordelord 6386

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

Assertion

Ref	Expression
ordelord	⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → Ord 𝐵)

Proof of Theorem ordelord

Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eleq1 2820	. . . . 5 ⊢ (𝑥 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝐵 ∈ 𝐴))
2	1	anbi2d 628	. . . 4 ⊢ (𝑥 = 𝐵 → ((Ord 𝐴 ∧ 𝑥 ∈ 𝐴) ↔ (Ord 𝐴 ∧ 𝐵 ∈ 𝐴)))
3		ordeq 6371	. . . 4 ⊢ (𝑥 = 𝐵 → (Ord 𝑥 ↔ Ord 𝐵))
4	2, 3	imbi12d 344	. . 3 ⊢ (𝑥 = 𝐵 → (((Ord 𝐴 ∧ 𝑥 ∈ 𝐴) → Ord 𝑥) ↔ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → Ord 𝐵)))
5		simpll 764	. . . . . . . . 9 ⊢ (((Ord 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥)) → Ord 𝐴)
6		3anrot 1099	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) ↔ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴))
7		3anass 1094	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) ↔ (𝑥 ∈ 𝐴 ∧ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥)))
8	6, 7	bitr3i 277	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) ↔ (𝑥 ∈ 𝐴 ∧ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥)))
9		ordtr 6378	. . . . . . . . . . . 12 ⊢ (Ord 𝐴 → Tr 𝐴)
10		trel3 5275	. . . . . . . . . . . 12 ⊢ (Tr 𝐴 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑧 ∈ 𝐴))
11	9, 10	syl 17	. . . . . . . . . . 11 ⊢ (Ord 𝐴 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑧 ∈ 𝐴))
12	8, 11	biimtrrid 242	. . . . . . . . . 10 ⊢ (Ord 𝐴 → ((𝑥 ∈ 𝐴 ∧ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥)) → 𝑧 ∈ 𝐴))
13	12	impl 455	. . . . . . . . 9 ⊢ (((Ord 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥)) → 𝑧 ∈ 𝐴)
14		trel 5274	. . . . . . . . . . . . 13 ⊢ (Tr 𝐴 → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐴))
15	9, 14	syl 17	. . . . . . . . . . . 12 ⊢ (Ord 𝐴 → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐴))
16	15	expcomd 416	. . . . . . . . . . 11 ⊢ (Ord 𝐴 → (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐴)))
17	16	imp31 417	. . . . . . . . . 10 ⊢ (((Ord 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝐴)
18	17	adantrl 713	. . . . . . . . 9 ⊢ (((Ord 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥)) → 𝑦 ∈ 𝐴)
19		simplr 766	. . . . . . . . 9 ⊢ (((Ord 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥)) → 𝑥 ∈ 𝐴)
20		ordwe 6377	. . . . . . . . . 10 ⊢ (Ord 𝐴 → E We 𝐴)
21		wetrep 5669	. . . . . . . . . 10 ⊢ (( E We 𝐴 ∧ (𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥))
22	20, 21	sylan 579	. . . . . . . . 9 ⊢ ((Ord 𝐴 ∧ (𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥))
23	5, 13, 18, 19, 22	syl13anc 1371	. . . . . . . 8 ⊢ (((Ord 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥)) → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥))
24	23	ex 412	. . . . . . 7 ⊢ ((Ord 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥)))
25	24	pm2.43d 53	. . . . . 6 ⊢ ((Ord 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥))
26	25	alrimivv 1930	. . . . 5 ⊢ ((Ord 𝐴 ∧ 𝑥 ∈ 𝐴) → ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥))
27		dftr2 5267	. . . . 5 ⊢ (Tr 𝑥 ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥))
28	26, 27	sylibr 233	. . . 4 ⊢ ((Ord 𝐴 ∧ 𝑥 ∈ 𝐴) → Tr 𝑥)
29		trss 5276	. . . . . . 7 ⊢ (Tr 𝐴 → (𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐴))
30	9, 29	syl 17	. . . . . 6 ⊢ (Ord 𝐴 → (𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐴))
31		wess 5663	. . . . . 6 ⊢ (𝑥 ⊆ 𝐴 → ( E We 𝐴 → E We 𝑥))
32	30, 20, 31	syl6ci 71	. . . . 5 ⊢ (Ord 𝐴 → (𝑥 ∈ 𝐴 → E We 𝑥))
33	32	imp 406	. . . 4 ⊢ ((Ord 𝐴 ∧ 𝑥 ∈ 𝐴) → E We 𝑥)
34		df-ord 6367	. . . 4 ⊢ (Ord 𝑥 ↔ (Tr 𝑥 ∧ E We 𝑥))
35	28, 33, 34	sylanbrc 582	. . 3 ⊢ ((Ord 𝐴 ∧ 𝑥 ∈ 𝐴) → Ord 𝑥)
36	4, 35	vtoclg 3542	. 2 ⊢ (𝐵 ∈ 𝐴 → ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → Ord 𝐵))
37	36	anabsi7 668	1 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → Ord 𝐵)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086  ∀wal 1538   = wceq 1540   ∈ wcel 2105   ⊆ wss 3948  Tr wtr 5265   E cep 5579   We wwe 5630  Ord word 6363

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702  ax-sep 5299  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-ne 2940  df-ral 3061  df-rab 3432  df-v 3475  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-tr 5266  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-ord 6367

This theorem is referenced by:  tron  6387  ordelon  6388  ordtr2  6408  ordintdif  6414  ordsuc  7804  ordsucOLD  7805  ordsucss  7809  ordsucelsuc  7813  ordsucuniel  7815  limsssuc  7842  smores  8355  smo11  8367  smoord  8368  smoword  8369  smogt  8370  smocdmdom  8371  rdglim2  8435  oesuclem  8528  ordtypelem3  9518  r1val1  9784  rankr1ag  9800  fin23lem24  10320  onsuct0  35630  dford3  42070  ordeldif  42311  ordeldifsucon  42312  ordeldif1o  42313  ordnexbtwnsuc  42320  ordpss  43513