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 𝑁 ↔ ∀ 𝑎 ∀ 𝑏 ∀ 𝑐 ( ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑎 ) → ( 𝑏 ∈ 𝑁 ∧ ( 𝑐 ∈ 𝑏 → 𝑐 ∈ 𝑎 ) ) ) )

Proof

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