Step |
Hyp |
Ref |
Expression |
1 |
|
simpll |
|- ( ( ( B e. ( ZZ>= ` A ) /\ D e. ( ZZ>= ` B ) ) /\ ( C e. ( ZZ>= ` B ) /\ D e. ( ZZ>= ` C ) ) ) -> B e. ( ZZ>= ` A ) ) |
2 |
|
simprl |
|- ( ( ( B e. ( ZZ>= ` A ) /\ D e. ( ZZ>= ` B ) ) /\ ( C e. ( ZZ>= ` B ) /\ D e. ( ZZ>= ` C ) ) ) -> C e. ( ZZ>= ` B ) ) |
3 |
1 2
|
jca |
|- ( ( ( B e. ( ZZ>= ` A ) /\ D e. ( ZZ>= ` B ) ) /\ ( C e. ( ZZ>= ` B ) /\ D e. ( ZZ>= ` C ) ) ) -> ( B e. ( ZZ>= ` A ) /\ C e. ( ZZ>= ` B ) ) ) |
4 |
|
uztrn |
|- ( ( C e. ( ZZ>= ` B ) /\ B e. ( ZZ>= ` A ) ) -> C e. ( ZZ>= ` A ) ) |
5 |
4
|
ancoms |
|- ( ( B e. ( ZZ>= ` A ) /\ C e. ( ZZ>= ` B ) ) -> C e. ( ZZ>= ` A ) ) |
6 |
5
|
ad2ant2r |
|- ( ( ( B e. ( ZZ>= ` A ) /\ D e. ( ZZ>= ` B ) ) /\ ( C e. ( ZZ>= ` B ) /\ D e. ( ZZ>= ` C ) ) ) -> C e. ( ZZ>= ` A ) ) |
7 |
|
simprr |
|- ( ( ( B e. ( ZZ>= ` A ) /\ D e. ( ZZ>= ` B ) ) /\ ( C e. ( ZZ>= ` B ) /\ D e. ( ZZ>= ` C ) ) ) -> D e. ( ZZ>= ` C ) ) |
8 |
3 6 7
|
jca32 |
|- ( ( ( B e. ( ZZ>= ` A ) /\ D e. ( ZZ>= ` B ) ) /\ ( C e. ( ZZ>= ` B ) /\ D e. ( ZZ>= ` C ) ) ) -> ( ( B e. ( ZZ>= ` A ) /\ C e. ( ZZ>= ` B ) ) /\ ( C e. ( ZZ>= ` A ) /\ D e. ( ZZ>= ` C ) ) ) ) |
9 |
|
simpll |
|- ( ( ( B e. ( ZZ>= ` A ) /\ C e. ( ZZ>= ` B ) ) /\ ( C e. ( ZZ>= ` A ) /\ D e. ( ZZ>= ` C ) ) ) -> B e. ( ZZ>= ` A ) ) |
10 |
|
uztrn |
|- ( ( D e. ( ZZ>= ` C ) /\ C e. ( ZZ>= ` B ) ) -> D e. ( ZZ>= ` B ) ) |
11 |
10
|
ancoms |
|- ( ( C e. ( ZZ>= ` B ) /\ D e. ( ZZ>= ` C ) ) -> D e. ( ZZ>= ` B ) ) |
12 |
11
|
ad2ant2l |
|- ( ( ( B e. ( ZZ>= ` A ) /\ C e. ( ZZ>= ` B ) ) /\ ( C e. ( ZZ>= ` A ) /\ D e. ( ZZ>= ` C ) ) ) -> D e. ( ZZ>= ` B ) ) |
13 |
9 12
|
jca |
|- ( ( ( B e. ( ZZ>= ` A ) /\ C e. ( ZZ>= ` B ) ) /\ ( C e. ( ZZ>= ` A ) /\ D e. ( ZZ>= ` C ) ) ) -> ( B e. ( ZZ>= ` A ) /\ D e. ( ZZ>= ` B ) ) ) |
14 |
|
simplr |
|- ( ( ( B e. ( ZZ>= ` A ) /\ C e. ( ZZ>= ` B ) ) /\ ( C e. ( ZZ>= ` A ) /\ D e. ( ZZ>= ` C ) ) ) -> C e. ( ZZ>= ` B ) ) |
15 |
|
simprr |
|- ( ( ( B e. ( ZZ>= ` A ) /\ C e. ( ZZ>= ` B ) ) /\ ( C e. ( ZZ>= ` A ) /\ D e. ( ZZ>= ` C ) ) ) -> D e. ( ZZ>= ` C ) ) |
16 |
13 14 15
|
jca32 |
|- ( ( ( B e. ( ZZ>= ` A ) /\ C e. ( ZZ>= ` B ) ) /\ ( C e. ( ZZ>= ` A ) /\ D e. ( ZZ>= ` C ) ) ) -> ( ( B e. ( ZZ>= ` A ) /\ D e. ( ZZ>= ` B ) ) /\ ( C e. ( ZZ>= ` B ) /\ D e. ( ZZ>= ` C ) ) ) ) |
17 |
8 16
|
impbii |
|- ( ( ( B e. ( ZZ>= ` A ) /\ D e. ( ZZ>= ` B ) ) /\ ( C e. ( ZZ>= ` B ) /\ D e. ( ZZ>= ` C ) ) ) <-> ( ( B e. ( ZZ>= ` A ) /\ C e. ( ZZ>= ` B ) ) /\ ( C e. ( ZZ>= ` A ) /\ D e. ( ZZ>= ` C ) ) ) ) |
18 |
|
elfzuzb |
|- ( B e. ( A ... D ) <-> ( B e. ( ZZ>= ` A ) /\ D e. ( ZZ>= ` B ) ) ) |
19 |
|
elfzuzb |
|- ( C e. ( B ... D ) <-> ( C e. ( ZZ>= ` B ) /\ D e. ( ZZ>= ` C ) ) ) |
20 |
18 19
|
anbi12i |
|- ( ( B e. ( A ... D ) /\ C e. ( B ... D ) ) <-> ( ( B e. ( ZZ>= ` A ) /\ D e. ( ZZ>= ` B ) ) /\ ( C e. ( ZZ>= ` B ) /\ D e. ( ZZ>= ` C ) ) ) ) |
21 |
|
elfzuzb |
|- ( B e. ( A ... C ) <-> ( B e. ( ZZ>= ` A ) /\ C e. ( ZZ>= ` B ) ) ) |
22 |
|
elfzuzb |
|- ( C e. ( A ... D ) <-> ( C e. ( ZZ>= ` A ) /\ D e. ( ZZ>= ` C ) ) ) |
23 |
21 22
|
anbi12i |
|- ( ( B e. ( A ... C ) /\ C e. ( A ... D ) ) <-> ( ( B e. ( ZZ>= ` A ) /\ C e. ( ZZ>= ` B ) ) /\ ( C e. ( ZZ>= ` A ) /\ D e. ( ZZ>= ` C ) ) ) ) |
24 |
17 20 23
|
3bitr4i |
|- ( ( B e. ( A ... D ) /\ C e. ( B ... D ) ) <-> ( B e. ( A ... C ) /\ C e. ( A ... D ) ) ) |