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 2821	. . . . 5 ⊢ (𝑥 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝐵 ∈ 𝐴))
2	1	anbi2d 629	. . . 4 ⊢ (𝑥 = 𝐵 → ((Ord 𝐴 ∧ 𝑥 ∈ 𝐴) ↔ (Ord 𝐴 ∧ 𝐵 ∈ 𝐴)))
3		ordeq 6371	. . . 4 ⊢ (𝑥 = 𝐵 → (Ord 𝑥 ↔ Ord 𝐵))
4	2, 3	imbi12d 344	. . 3 ⊢ (𝑥 = 𝐵 → (((Ord 𝐴 ∧ 𝑥 ∈ 𝐴) → Ord 𝑥) ↔ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → Ord 𝐵)))
5		simpll 765	. . . . . . . . 9 ⊢ (((Ord 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥)) → Ord 𝐴)
6		3anrot 1100	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) ↔ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴))
7		3anass 1095	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) ↔ (𝑥 ∈ 𝐴 ∧ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥)))
8	6, 7	bitr3i 276	. . . . . . . . . . 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 456	. . . . . . . . 9 ⊢ (((Ord 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥)) → 𝑧 ∈ 𝐴)
14		trel 5274	. . . . . . . . . . . . 13 ⊢ (Tr 𝐴 → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐴))
15	9, 14	syl 17	. . . . . . . . . . . 12 ⊢ (Ord 𝐴 → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐴))
16	15	expcomd 417	. . . . . . . . . . 11 ⊢ (Ord 𝐴 → (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐴)))
17	16	imp31 418	. . . . . . . . . 10 ⊢ (((Ord 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝐴)
18	17	adantrl 714	. . . . . . . . 9 ⊢ (((Ord 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥)) → 𝑦 ∈ 𝐴)
19		simplr 767	. . . . . . . . 9 ⊢ (((Ord 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥)) → 𝑥 ∈ 𝐴)
20		ordwe 6377	. . . . . . . . . 10 ⊢ (Ord 𝐴 → E We 𝐴)
21		wetrep 5669	. . . . . . . . . 10 ⊢ (( E We 𝐴 ∧ (𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥))
22	20, 21	sylan 580	. . . . . . . . 9 ⊢ ((Ord 𝐴 ∧ (𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥))
23	5, 13, 18, 19, 22	syl13anc 1372	. . . . . . . 8 ⊢ (((Ord 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥)) → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥))
24	23	ex 413	. . . . . . 7 ⊢ ((Ord 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥)))
25	24	pm2.43d 53	. . . . . 6 ⊢ ((Ord 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥))
26	25	alrimivv 1931	. . . . 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 407	. . . 4 ⊢ ((Ord 𝐴 ∧ 𝑥 ∈ 𝐴) → E We 𝑥)
34		df-ord 6367	. . . 4 ⊢ (Ord 𝑥 ↔ (Tr 𝑥 ∧ E We 𝑥))
35	28, 33, 34	sylanbrc 583	. . 3 ⊢ ((Ord 𝐴 ∧ 𝑥 ∈ 𝐴) → Ord 𝑥)
36	4, 35	vtoclg 3556	. 2 ⊢ (𝐵 ∈ 𝐴 → ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → Ord 𝐵))
37	36	anabsi7 669	1 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → Ord 𝐵)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1087  ∀wal 1539   = wceq 1541   ∈ wcel 2106   ⊆ 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 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ne 2941  df-ral 3062  df-rab 3433  df-v 3476  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  7800  ordsucOLD  7801  ordsucss  7805  ordsucelsuc  7809  ordsucuniel  7811  limsssuc  7838  smores  8351  smo11  8363  smoord  8364  smoword  8365  smogt  8366  smocdmdom  8367  rdglim2  8431  oesuclem  8524  ordtypelem3  9514  r1val1  9780  rankr1ag  9796  fin23lem24  10316  onsuct0  35321  dford3  41757  ordeldif  41998  ordeldifsucon  41999  ordeldif1o  42000  ordnexbtwnsuc  42007  ordpss  43200