Metamath Proof Explorer


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.

1:: |- (. ( Ord A /\ B e. A ) ->. ( Ord A /\ B e. A ) ).
2:1: |- (. ( Ord A /\ B e. A ) ->. Ord A ).
3:1: |- (. ( Ord A /\ B e. A ) ->. B e. A ).
4:2: |- (. ( Ord A /\ B e. A ) ->. Tr A ).
5:2: |- (. ( Ord A /\ B e. A ) ->. A. x e. A A. y e. A ( x e. y \/ x = y \/ y e. x ) ).
6:4,3: |- (. ( Ord A /\ B e. A ) ->. B C_ A ).
7:6,6,5: |- (. ( Ord A /\ B e. A ) ->. A. x e. B A. y e. B ( x e. y \/ x = y \/ y e. x ) ).
8:: |- ( ( x e. y \/ x = y \/ y e. x ) <-> ( x e. y \/ y e. x \/ x = y ) )
9:8: |- A. y ( ( x e. y \/ x = y \/ y e. x ) <-> ( x e. y \/ y e. x \/ x = y ) )
10:9: |- A. y e. A ( ( x e. y \/ x = y \/ y e. x ) <-> ( x e. y \/ y e. x \/ x = y ) )
11:10: |- ( A. y e. A ( x e. y \/ x = y \/ y e. x ) <-> A. y e. A ( x e. y \/ y e. x \/ x = y ) )
12:11: |- A. x ( A. y e. A ( x e. y \/ x = y \/ y e. x ) <-> A. y e. A ( x e. y \/ y e. x \/ x = y ) )
13:12: |- A. x e. A ( A. y e. A ( x e. y \/ x = y \/ y e. x ) <-> A. y e. A ( x e. y \/ y e. x \/ x = y ) )
14:13: |- ( A. x e. A A. y e. A ( x e. y \/ x = y \/ y e. x ) <-> A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) )
15:14,5: |- (. ( Ord A /\ B e. A ) ->. A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) ).
16:4,15,3: |- (. ( Ord A /\ B e. A ) ->. Tr B ).
17:16,7: |- (. ( Ord A /\ B e. A ) ->. Ord B ).
qed:17: |- ( ( Ord A /\ B e. A ) -> Ord B )
(Contributed by Alan Sare, 12-Feb-2012) (Proof modification is discouraged.) (New usage is discouraged.)

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