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. a A. b A. c ( ( a e. N /\ b e. a ) -> ( b e. N /\ ( c e. b -> c e. a ) ) ) )

Proof

Step Hyp Ref Expression
1 dford3 
 |-  ( Ord N <-> ( Tr N /\ A. a e. N Tr a ) )
2 dftr2 
 |-  ( Tr N <-> A. b A. a ( ( b e. a /\ a e. N ) -> b e. N ) )
3 19.3v 
 |-  ( A. c ( ( a e. N /\ b e. a ) -> b e. N ) <-> ( ( a e. N /\ b e. a ) -> b e. N ) )
4 ancom 
 |-  ( ( a e. N /\ b e. a ) <-> ( b e. a /\ a e. N ) )
5 4 imbi1i 
 |-  ( ( ( a e. N /\ b e. a ) -> b e. N ) <-> ( ( b e. a /\ a e. N ) -> b e. N ) )
6 3 5 bitri 
 |-  ( A. c ( ( a e. N /\ b e. a ) -> b e. N ) <-> ( ( b e. a /\ a e. N ) -> b e. N ) )
7 6 2albii 
 |-  ( A. a A. b A. c ( ( a e. N /\ b e. a ) -> b e. N ) <-> A. a A. b ( ( b e. a /\ a e. N ) -> b e. N ) )
8 alcom 
 |-  ( A. a A. b ( ( b e. a /\ a e. N ) -> b e. N ) <-> A. b A. a ( ( b e. a /\ a e. N ) -> b e. N ) )
9 7 8 bitri 
 |-  ( A. a A. b A. c ( ( a e. N /\ b e. a ) -> b e. N ) <-> A. b A. a ( ( b e. a /\ a e. N ) -> b e. N ) )
10 2 9 bitr4i 
 |-  ( Tr N <-> A. a A. b A. c ( ( a e. N /\ b e. a ) -> b e. N ) )
11 df-ral 
 |-  ( A. a e. N Tr a <-> A. a ( a e. N -> Tr a ) )
12 dftr2 
 |-  ( Tr a <-> A. c A. b ( ( c e. b /\ b e. a ) -> c e. a ) )
13 12 imbi2i 
 |-  ( ( a e. N -> Tr a ) <-> ( a e. N -> A. c A. b ( ( c e. b /\ b e. a ) -> c e. a ) ) )
14 nfv 
 |-  F/ c a e. N
15 nfv 
 |-  F/ b a e. N
16 14 15 19.21-2 
 |-  ( A. c A. b ( a e. N -> ( ( c e. b /\ b e. a ) -> c e. a ) ) <-> ( a e. N -> A. c A. b ( ( c e. b /\ b e. a ) -> c e. a ) ) )
17 13 16 bitr4i 
 |-  ( ( a e. N -> Tr a ) <-> A. c A. b ( a e. N -> ( ( c e. b /\ b e. a ) -> c e. a ) ) )
18 impexp 
 |-  ( ( ( a e. N /\ ( c e. b /\ b e. a ) ) -> c e. a ) <-> ( a e. N -> ( ( c e. b /\ b e. a ) -> c e. a ) ) )
19 ancom 
 |-  ( ( c e. b /\ b e. a ) <-> ( b e. a /\ c e. b ) )
20 19 anbi2i 
 |-  ( ( a e. N /\ ( c e. b /\ b e. a ) ) <-> ( a e. N /\ ( b e. a /\ c e. b ) ) )
21 anass 
 |-  ( ( ( a e. N /\ b e. a ) /\ c e. b ) <-> ( a e. N /\ ( b e. a /\ c e. b ) ) )
22 20 21 bitr4i 
 |-  ( ( a e. N /\ ( c e. b /\ b e. a ) ) <-> ( ( a e. N /\ b e. a ) /\ c e. b ) )
23 22 imbi1i 
 |-  ( ( ( a e. N /\ ( c e. b /\ b e. a ) ) -> c e. a ) <-> ( ( ( a e. N /\ b e. a ) /\ c e. b ) -> c e. a ) )
24 18 23 bitr3i 
 |-  ( ( a e. N -> ( ( c e. b /\ b e. a ) -> c e. a ) ) <-> ( ( ( a e. N /\ b e. a ) /\ c e. b ) -> c e. a ) )
25 impexp 
 |-  ( ( ( ( a e. N /\ b e. a ) /\ c e. b ) -> c e. a ) <-> ( ( a e. N /\ b e. a ) -> ( c e. b -> c e. a ) ) )
26 24 25 bitri 
 |-  ( ( a e. N -> ( ( c e. b /\ b e. a ) -> c e. a ) ) <-> ( ( a e. N /\ b e. a ) -> ( c e. b -> c e. a ) ) )
27 26 2albii 
 |-  ( A. c A. b ( a e. N -> ( ( c e. b /\ b e. a ) -> c e. a ) ) <-> A. c A. b ( ( a e. N /\ b e. a ) -> ( c e. b -> c e. a ) ) )
28 alcom 
 |-  ( A. c A. b ( ( a e. N /\ b e. a ) -> ( c e. b -> c e. a ) ) <-> A. b A. c ( ( a e. N /\ b e. a ) -> ( c e. b -> c e. a ) ) )
29 17 27 28 3bitri 
 |-  ( ( a e. N -> Tr a ) <-> A. b A. c ( ( a e. N /\ b e. a ) -> ( c e. b -> c e. a ) ) )
30 29 albii 
 |-  ( A. a ( a e. N -> Tr a ) <-> A. a A. b A. c ( ( a e. N /\ b e. a ) -> ( c e. b -> c e. a ) ) )
31 11 30 bitri 
 |-  ( A. a e. N Tr a <-> A. a A. b A. c ( ( a e. N /\ b e. a ) -> ( c e. b -> c e. a ) ) )
32 10 31 anbi12i 
 |-  ( ( Tr N /\ A. a e. N Tr a ) <-> ( A. a A. b A. c ( ( a e. N /\ b e. a ) -> b e. N ) /\ A. a A. b A. c ( ( a e. N /\ b e. a ) -> ( c e. b -> c e. a ) ) ) )
33 19.26 
 |-  ( A. a ( A. b A. c ( ( a e. N /\ b e. a ) -> b e. N ) /\ A. b A. c ( ( a e. N /\ b e. a ) -> ( c e. b -> c e. a ) ) ) <-> ( A. a A. b A. c ( ( a e. N /\ b e. a ) -> b e. N ) /\ A. a A. b A. c ( ( a e. N /\ b e. a ) -> ( c e. b -> c e. a ) ) ) )
34 32 33 bitr4i 
 |-  ( ( Tr N /\ A. a e. N Tr a ) <-> A. a ( A. b A. c ( ( a e. N /\ b e. a ) -> b e. N ) /\ A. b A. c ( ( a e. N /\ b e. a ) -> ( c e. b -> c e. a ) ) ) )
35 19.26-2 
 |-  ( A. b A. c ( ( ( a e. N /\ b e. a ) -> b e. N ) /\ ( ( a e. N /\ b e. a ) -> ( c e. b -> c e. a ) ) ) <-> ( A. b A. c ( ( a e. N /\ b e. a ) -> b e. N ) /\ A. b A. c ( ( a e. N /\ b e. a ) -> ( c e. b -> c e. a ) ) ) )
36 pm4.76 
 |-  ( ( ( ( a e. N /\ b e. a ) -> b e. N ) /\ ( ( a e. N /\ b e. a ) -> ( c e. b -> c e. a ) ) ) <-> ( ( a e. N /\ b e. a ) -> ( b e. N /\ ( c e. b -> c e. a ) ) ) )
37 36 2albii 
 |-  ( A. b A. c ( ( ( a e. N /\ b e. a ) -> b e. N ) /\ ( ( a e. N /\ b e. a ) -> ( c e. b -> c e. a ) ) ) <-> A. b A. c ( ( a e. N /\ b e. a ) -> ( b e. N /\ ( c e. b -> c e. a ) ) ) )
38 35 37 bitr3i 
 |-  ( ( A. b A. c ( ( a e. N /\ b e. a ) -> b e. N ) /\ A. b A. c ( ( a e. N /\ b e. a ) -> ( c e. b -> c e. a ) ) ) <-> A. b A. c ( ( a e. N /\ b e. a ) -> ( b e. N /\ ( c e. b -> c e. a ) ) ) )
39 38 albii 
 |-  ( A. a ( A. b A. c ( ( a e. N /\ b e. a ) -> b e. N ) /\ A. b A. c ( ( a e. N /\ b e. a ) -> ( c e. b -> c e. a ) ) ) <-> A. a A. b A. c ( ( a e. N /\ b e. a ) -> ( b e. N /\ ( c e. b -> c e. a ) ) ) )
40 1 34 39 3bitri 
 |-  ( Ord N <-> A. a A. b A. c ( ( a e. N /\ b e. a ) -> ( b e. N /\ ( c e. b -> c e. a ) ) ) )