Theorem ordelordALTVD

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. The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. ordelordALT is ordelordALTVD without virtual deductions and was automatically derived from ordelordALTVD using the tools program translate..without..overwriting.cmd and the Metamath program "MM-PA> MINIMIZE__WITH *" command.

	Ref	Expression
Assertion	ordelordALTVD	⊢ ( ( Ord 𝐴 ∧ 𝐵 ∈ 𝐴 ) → Ord 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		idn1	⊢ (    ( Ord 𝐴 ∧ 𝐵 ∈ 𝐴 )    ▶    ( Ord 𝐴 ∧ 𝐵 ∈ 𝐴 )    )
2		simpl	⊢ ( ( Ord 𝐴 ∧ 𝐵 ∈ 𝐴 ) → Ord 𝐴 )
3	1 2	e1a	⊢ (    ( Ord 𝐴 ∧ 𝐵 ∈ 𝐴 )    ▶    Ord 𝐴    )
4		ordtr	⊢ ( Ord 𝐴 → Tr 𝐴 )
5	3 4	e1a	⊢ (    ( Ord 𝐴 ∧ 𝐵 ∈ 𝐴 )    ▶    Tr 𝐴    )
6		dford2	⊢ ( Ord 𝐴 ↔ ( Tr 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥 ) ) )
7	6	simprbi	⊢ ( Ord 𝐴 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥 ) )
8	3 7	e1a	⊢ (    ( Ord 𝐴 ∧ 𝐵 ∈ 𝐴 )    ▶    ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥 )    )
9		3orcomb	⊢ ( ( 𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥 ) ↔ ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) )
10	9	ax-gen	⊢ ∀ 𝑦 ( ( 𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥 ) ↔ ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) )
11		alral	⊢ ( ∀ 𝑦 ( ( 𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥 ) ↔ ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ) → ∀ 𝑦 ∈ 𝐴 ( ( 𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥 ) ↔ ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ) )
12	10 11	e0a	⊢ ∀ 𝑦 ∈ 𝐴 ( ( 𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥 ) ↔ ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) )
13		ralbi	⊢ ( ∀ 𝑦 ∈ 𝐴 ( ( 𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥 ) ↔ ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ) → ( ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥 ) ↔ ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ) )
14	12 13	e0a	⊢ ( ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥 ) ↔ ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) )
15	14	ax-gen	⊢ ∀ 𝑥 ( ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥 ) ↔ ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) )
16		alral	⊢ ( ∀ 𝑥 ( ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥 ) ↔ ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ) → ∀ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥 ) ↔ ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ) )
17	15 16	e0a	⊢ ∀ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥 ) ↔ ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) )
18		ralbi	⊢ ( ∀ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥 ) ↔ ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ) )
19	17 18	e0a	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) )
20	8 19	e1bi	⊢ (    ( Ord 𝐴 ∧ 𝐵 ∈ 𝐴 )    ▶    ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 )    )
21		simpr	⊢ ( ( Ord 𝐴 ∧ 𝐵 ∈ 𝐴 ) → 𝐵 ∈ 𝐴 )
22	1 21	e1a	⊢ (    ( Ord 𝐴 ∧ 𝐵 ∈ 𝐴 )    ▶    𝐵 ∈ 𝐴    )
23		tratrb	⊢ ( ( Tr 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ∧ 𝐵 ∈ 𝐴 ) → Tr 𝐵 )
24	23	3exp	⊢ ( Tr 𝐴 → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) → ( 𝐵 ∈ 𝐴 → Tr 𝐵 ) ) )
25	5 20 22 24	e111	⊢ (    ( Ord 𝐴 ∧ 𝐵 ∈ 𝐴 )    ▶    Tr 𝐵    )
26		trss	⊢ ( Tr 𝐴 → ( 𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴 ) )
27	5 22 26	e11	⊢ (    ( Ord 𝐴 ∧ 𝐵 ∈ 𝐴 )    ▶    𝐵 ⊆ 𝐴    )
28		ssralv2	⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥 ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥 ) ) )
29	28	ex	⊢ ( 𝐵 ⊆ 𝐴 → ( 𝐵 ⊆ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥 ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥 ) ) ) )
30	27 27 8 29	e111	⊢ (    ( Ord 𝐴 ∧ 𝐵 ∈ 𝐴 )    ▶    ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥 )    )
31		dford2	⊢ ( Ord 𝐵 ↔ ( Tr 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥 ) ) )
32	31	simplbi2	⊢ ( Tr 𝐵 → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥 ) → Ord 𝐵 ) )
33	25 30 32	e11	⊢ (    ( Ord 𝐴 ∧ 𝐵 ∈ 𝐴 )    ▶    Ord 𝐵    )
34	33	in1	⊢ ( ( Ord 𝐴 ∧ 𝐵 ∈ 𝐴 ) → Ord 𝐵 )