Metamath Proof Explorer

Theorem dford4

Description: dford3 expressed in primitives to demonstrate shortness. (Contributed by Stefan O'Rear, 28-Oct-2014)

Ref Expression
Assertion dford4 ⊢Ord⁡N↔∀a∀b∀ca∈N∧b∈a→b∈N∧c∈b→c∈a

Proof

Step Hyp Ref Expression
1 dford3 ⊢Ord⁡N↔Tr⁡N∧∀a∈NTr⁡a
2 dftr2 ⊢Tr⁡N↔∀b∀ab∈a∧a∈N→b∈N
3 19.3v ⊢∀ca∈N∧b∈a→b∈N↔a∈N∧b∈a→b∈N
4 ancom ⊢a∈N∧b∈a↔b∈a∧a∈N
5 4 imbi1i ⊢a∈N∧b∈a→b∈N↔b∈a∧a∈N→b∈N
6 3 5 bitri ⊢∀ca∈N∧b∈a→b∈N↔b∈a∧a∈N→b∈N
7 6 2albii ⊢∀a∀b∀ca∈N∧b∈a→b∈N↔∀a∀bb∈a∧a∈N→b∈N
8 alcom ⊢∀a∀bb∈a∧a∈N→b∈N↔∀b∀ab∈a∧a∈N→b∈N
9 7 8 bitri ⊢∀a∀b∀ca∈N∧b∈a→b∈N↔∀b∀ab∈a∧a∈N→b∈N
10 2 9 bitr4i ⊢Tr⁡N↔∀a∀b∀ca∈N∧b∈a→b∈N
11 df-ral ⊢∀a∈NTr⁡a↔∀aa∈N→Tr⁡a
12 dftr2 ⊢Tr⁡a↔∀c∀bc∈b∧b∈a→c∈a
13 12 imbi2i ⊢a∈N→Tr⁡a↔a∈N→∀c∀bc∈b∧b∈a→c∈a
14 nfv ⊢Ⅎca∈N
15 nfv ⊢Ⅎba∈N
16 14 15 19.21-2 ⊢∀c∀ba∈N→c∈b∧b∈a→c∈a↔a∈N→∀c∀bc∈b∧b∈a→c∈a
17 13 16 bitr4i ⊢a∈N→Tr⁡a↔∀c∀ba∈N→c∈b∧b∈a→c∈a
18 impexp ⊢a∈N∧c∈b∧b∈a→c∈a↔a∈N→c∈b∧b∈a→c∈a
19 ancom ⊢c∈b∧b∈a↔b∈a∧c∈b
20 19 anbi2i ⊢a∈N∧c∈b∧b∈a↔a∈N∧b∈a∧c∈b
21 anass ⊢a∈N∧b∈a∧c∈b↔a∈N∧b∈a∧c∈b
22 20 21 bitr4i ⊢a∈N∧c∈b∧b∈a↔a∈N∧b∈a∧c∈b
23 22 imbi1i ⊢a∈N∧c∈b∧b∈a→c∈a↔a∈N∧b∈a∧c∈b→c∈a
24 18 23 bitr3i ⊢a∈N→c∈b∧b∈a→c∈a↔a∈N∧b∈a∧c∈b→c∈a
25 impexp ⊢a∈N∧b∈a∧c∈b→c∈a↔a∈N∧b∈a→c∈b→c∈a
26 24 25 bitri ⊢a∈N→c∈b∧b∈a→c∈a↔a∈N∧b∈a→c∈b→c∈a
27 26 2albii ⊢∀c∀ba∈N→c∈b∧b∈a→c∈a↔∀c∀ba∈N∧b∈a→c∈b→c∈a
28 alcom ⊢∀c∀ba∈N∧b∈a→c∈b→c∈a↔∀b∀ca∈N∧b∈a→c∈b→c∈a
29 17 27 28 3bitri ⊢a∈N→Tr⁡a↔∀b∀ca∈N∧b∈a→c∈b→c∈a
30 29 albii ⊢∀aa∈N→Tr⁡a↔∀a∀b∀ca∈N∧b∈a→c∈b→c∈a
31 11 30 bitri ⊢∀a∈NTr⁡a↔∀a∀b∀ca∈N∧b∈a→c∈b→c∈a
32 10 31 anbi12i ⊢Tr⁡N∧∀a∈NTr⁡a↔∀a∀b∀ca∈N∧b∈a→b∈N∧∀a∀b∀ca∈N∧b∈a→c∈b→c∈a
33 19.26 ⊢∀a∀b∀ca∈N∧b∈a→b∈N∧∀b∀ca∈N∧b∈a→c∈b→c∈a↔∀a∀b∀ca∈N∧b∈a→b∈N∧∀a∀b∀ca∈N∧b∈a→c∈b→c∈a
34 32 33 bitr4i ⊢Tr⁡N∧∀a∈NTr⁡a↔∀a∀b∀ca∈N∧b∈a→b∈N∧∀b∀ca∈N∧b∈a→c∈b→c∈a
35 19.26-2 ⊢∀b∀ca∈N∧b∈a→b∈N∧a∈N∧b∈a→c∈b→c∈a↔∀b∀ca∈N∧b∈a→b∈N∧∀b∀ca∈N∧b∈a→c∈b→c∈a
36 pm4.76 ⊢a∈N∧b∈a→b∈N∧a∈N∧b∈a→c∈b→c∈a↔a∈N∧b∈a→b∈N∧c∈b→c∈a
37 36 2albii ⊢∀b∀ca∈N∧b∈a→b∈N∧a∈N∧b∈a→c∈b→c∈a↔∀b∀ca∈N∧b∈a→b∈N∧c∈b→c∈a
38 35 37 bitr3i ⊢∀b∀ca∈N∧b∈a→b∈N∧∀b∀ca∈N∧b∈a→c∈b→c∈a↔∀b∀ca∈N∧b∈a→b∈N∧c∈b→c∈a
39 38 albii ⊢∀a∀b∀ca∈N∧b∈a→b∈N∧∀b∀ca∈N∧b∈a→c∈b→c∈a↔∀a∀b∀ca∈N∧b∈a→b∈N∧c∈b→c∈a
40 1 34 39 3bitri ⊢Ord⁡N↔∀a∀b∀ca∈N∧b∈a→b∈N∧c∈b→c∈a