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 ∀ c a ∈ N ∧ b ∈ a → b ∈ N ∧ c ∈ b → c ∈ a

Proof

Step Hyp Ref Expression
1 dford3 ⊢ Ord ⁡ N ↔ Tr ⁡ N ∧ ∀ a ∈ N Tr ⁡ a
2 dftr2 ⊢ Tr ⁡ N ↔ ∀ b ∀ a b ∈ a ∧ a ∈ N → b ∈ N
3 19.3v ⊢ ∀ c a ∈ 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 ⊢ ∀ c a ∈ N ∧ b ∈ a → b ∈ N ↔ b ∈ a ∧ a ∈ N → b ∈ N
7 6 2albii ⊢ ∀ a ∀ b ∀ c a ∈ N ∧ b ∈ a → b ∈ N ↔ ∀ a ∀ b b ∈ a ∧ a ∈ N → b ∈ N
8 alcom ⊢ ∀ a ∀ b b ∈ a ∧ a ∈ N → b ∈ N ↔ ∀ b ∀ a b ∈ a ∧ a ∈ N → b ∈ N
9 7 8 bitri ⊢ ∀ a ∀ b ∀ c a ∈ N ∧ b ∈ a → b ∈ N ↔ ∀ b ∀ a b ∈ a ∧ a ∈ N → b ∈ N
10 2 9 bitr4i ⊢ Tr ⁡ N ↔ ∀ a ∀ b ∀ c a ∈ N ∧ b ∈ a → b ∈ N
11 df-ral ⊢ ∀ a ∈ N Tr ⁡ a ↔ ∀ a a ∈ N → Tr ⁡ a
12 dftr2 ⊢ Tr ⁡ a ↔ ∀ c ∀ b c ∈ b ∧ b ∈ a → c ∈ a
13 12 imbi2i ⊢ a ∈ N → Tr ⁡ a ↔ a ∈ N → ∀ c ∀ b c ∈ b ∧ b ∈ a → c ∈ a
14 nfv ⊢ Ⅎ c a ∈ N
15 nfv ⊢ Ⅎ b a ∈ N
16 14 15 19.21-2 ⊢ ∀ c ∀ b a ∈ N → c ∈ b ∧ b ∈ a → c ∈ a ↔ a ∈ N → ∀ c ∀ b c ∈ b ∧ b ∈ a → c ∈ a
17 13 16 bitr4i ⊢ a ∈ N → Tr ⁡ a ↔ ∀ c ∀ b a ∈ 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 ∀ b a ∈ N → c ∈ b ∧ b ∈ a → c ∈ a ↔ ∀ c ∀ b a ∈ N ∧ b ∈ a → c ∈ b → c ∈ a
28 alcom ⊢ ∀ c ∀ b a ∈ N ∧ b ∈ a → c ∈ b → c ∈ a ↔ ∀ b ∀ c a ∈ N ∧ b ∈ a → c ∈ b → c ∈ a
29 17 27 28 3bitri ⊢ a ∈ N → Tr ⁡ a ↔ ∀ b ∀ c a ∈ N ∧ b ∈ a → c ∈ b → c ∈ a
30 29 albii ⊢ ∀ a a ∈ N → Tr ⁡ a ↔ ∀ a ∀ b ∀ c a ∈ N ∧ b ∈ a → c ∈ b → c ∈ a
31 11 30 bitri ⊢ ∀ a ∈ N Tr ⁡ a ↔ ∀ a ∀ b ∀ c a ∈ N ∧ b ∈ a → c ∈ b → c ∈ a
32 10 31 anbi12i ⊢ Tr ⁡ N ∧ ∀ a ∈ N Tr ⁡ a ↔ ∀ a ∀ b ∀ c a ∈ N ∧ b ∈ a → b ∈ N ∧ ∀ a ∀ b ∀ c a ∈ N ∧ b ∈ a → c ∈ b → c ∈ a
33 19.26 ⊢ ∀ a ∀ b ∀ c a ∈ N ∧ b ∈ a → b ∈ N ∧ ∀ b ∀ c a ∈ N ∧ b ∈ a → c ∈ b → c ∈ a ↔ ∀ a ∀ b ∀ c a ∈ N ∧ b ∈ a → b ∈ N ∧ ∀ a ∀ b ∀ c a ∈ N ∧ b ∈ a → c ∈ b → c ∈ a
34 32 33 bitr4i ⊢ Tr ⁡ N ∧ ∀ a ∈ N Tr ⁡ a ↔ ∀ a ∀ b ∀ c a ∈ N ∧ b ∈ a → b ∈ N ∧ ∀ b ∀ c a ∈ N ∧ b ∈ a → c ∈ b → c ∈ a
35 19.26-2 ⊢ ∀ b ∀ c a ∈ N ∧ b ∈ a → b ∈ N ∧ a ∈ N ∧ b ∈ a → c ∈ b → c ∈ a ↔ ∀ b ∀ c a ∈ N ∧ b ∈ a → b ∈ N ∧ ∀ b ∀ c a ∈ 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 ∀ c a ∈ N ∧ b ∈ a → b ∈ N ∧ a ∈ N ∧ b ∈ a → c ∈ b → c ∈ a ↔ ∀ b ∀ c a ∈ N ∧ b ∈ a → b ∈ N ∧ c ∈ b → c ∈ a
38 35 37 bitr3i ⊢ ∀ b ∀ c a ∈ N ∧ b ∈ a → b ∈ N ∧ ∀ b ∀ c a ∈ N ∧ b ∈ a → c ∈ b → c ∈ a ↔ ∀ b ∀ c a ∈ N ∧ b ∈ a → b ∈ N ∧ c ∈ b → c ∈ a
39 38 albii ⊢ ∀ a ∀ b ∀ c a ∈ N ∧ b ∈ a → b ∈ N ∧ ∀ b ∀ c a ∈ N ∧ b ∈ a → c ∈ b → c ∈ a ↔ ∀ a ∀ b ∀ c a ∈ N ∧ b ∈ a → b ∈ N ∧ c ∈ b → c ∈ a
40 1 34 39 3bitri ⊢ Ord ⁡ N ↔ ∀ a ∀ b ∀ c a ∈ N ∧ b ∈ a → b ∈ N ∧ c ∈ b → c ∈ a