Metamath Proof Explorer

Theorem ordelordALT

Description: An element of an ordinal class is ordinal. Proposition 7.6 of TakeutiZaring p. 36. This is an alternate proof of ordelord using the Axiom of Regularity indirectly through dford2 . dford2 is a weaker definition of ordinal number. Given the Axiom of Regularity, it need not be assumed that _E Fr A because this is inferred by the Axiom of Regularity. ordelordALT is ordelordALTVD without virtual deductions and was automatically derived from ordelordALTVD using the tools program translate..without..overwriting.cmd and Metamath's minimize command. (Contributed by Alan Sare, 18-Feb-2012) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion ordelordALT ⊢ Ord ⁡ A ∧ B ∈ A → Ord ⁡ B

Proof

Step Hyp Ref Expression
1 ordtr ⊢ Ord ⁡ A → Tr ⁡ A
2 1 adantr ⊢ Ord ⁡ A ∧ B ∈ A → Tr ⁡ A
3 dford2 ⊢ Ord ⁡ A ↔ Tr ⁡ A ∧ ∀ x ∈ A ∀ y ∈ A x ∈ y ∨ x = y ∨ y ∈ x
4 3 simprbi ⊢ Ord ⁡ A → ∀ x ∈ A ∀ y ∈ A x ∈ y ∨ x = y ∨ y ∈ x
5 4 adantr ⊢ Ord ⁡ A ∧ B ∈ A → ∀ x ∈ A ∀ y ∈ A x ∈ y ∨ x = y ∨ y ∈ x
6 3orcomb ⊢ x ∈ y ∨ x = y ∨ y ∈ x ↔ x ∈ y ∨ y ∈ x ∨ x = y
7 6 2ralbii ⊢ ∀ x ∈ A ∀ y ∈ A x ∈ y ∨ x = y ∨ y ∈ x ↔ ∀ x ∈ A ∀ y ∈ A x ∈ y ∨ y ∈ x ∨ x = y
8 5 7 sylib ⊢ Ord ⁡ A ∧ B ∈ A → ∀ x ∈ A ∀ y ∈ A x ∈ y ∨ y ∈ x ∨ x = y
9 simpr ⊢ Ord ⁡ A ∧ B ∈ A → B ∈ A
10 tratrb ⊢ Tr ⁡ A ∧ ∀ x ∈ A ∀ y ∈ A x ∈ y ∨ y ∈ x ∨ x = y ∧ B ∈ A → Tr ⁡ B
11 2 8 9 10 syl3anc ⊢ Ord ⁡ A ∧ B ∈ A → Tr ⁡ B
12 trss ⊢ Tr ⁡ A → B ∈ A → B ⊆ A
13 2 9 12 sylc ⊢ Ord ⁡ A ∧ B ∈ A → B ⊆ A
14 ssralv2 ⊢ B ⊆ A ∧ B ⊆ A → ∀ x ∈ A ∀ y ∈ A x ∈ y ∨ x = y ∨ y ∈ x → ∀ x ∈ B ∀ y ∈ B x ∈ y ∨ x = y ∨ y ∈ x
15 14 ex ⊢ B ⊆ A → B ⊆ A → ∀ x ∈ A ∀ y ∈ A x ∈ y ∨ x = y ∨ y ∈ x → ∀ x ∈ B ∀ y ∈ B x ∈ y ∨ x = y ∨ y ∈ x
16 13 13 5 15 syl3c ⊢ Ord ⁡ A ∧ B ∈ A → ∀ x ∈ B ∀ y ∈ B x ∈ y ∨ x = y ∨ y ∈ x
17 dford2 ⊢ Ord ⁡ B ↔ Tr ⁡ B ∧ ∀ x ∈ B ∀ y ∈ B x ∈ y ∨ x = y ∨ y ∈ x
18 11 16 17 sylanbrc ⊢ Ord ⁡ A ∧ B ∈ A → Ord ⁡ B