Step |
Hyp |
Ref |
Expression |
1 |
|
ordelord |
|- ( ( Ord C /\ B e. C ) -> Ord B ) |
2 |
1
|
ex |
|- ( Ord C -> ( B e. C -> Ord B ) ) |
3 |
2
|
ancld |
|- ( Ord C -> ( B e. C -> ( B e. C /\ Ord B ) ) ) |
4 |
3
|
anc2li |
|- ( Ord C -> ( B e. C -> ( Ord C /\ ( B e. C /\ Ord B ) ) ) ) |
5 |
|
ordelpss |
|- ( ( Ord B /\ Ord C ) -> ( B e. C <-> B C. C ) ) |
6 |
|
sspsstr |
|- ( ( A C_ B /\ B C. C ) -> A C. C ) |
7 |
6
|
expcom |
|- ( B C. C -> ( A C_ B -> A C. C ) ) |
8 |
5 7
|
syl6bi |
|- ( ( Ord B /\ Ord C ) -> ( B e. C -> ( A C_ B -> A C. C ) ) ) |
9 |
8
|
expcom |
|- ( Ord C -> ( Ord B -> ( B e. C -> ( A C_ B -> A C. C ) ) ) ) |
10 |
9
|
com23 |
|- ( Ord C -> ( B e. C -> ( Ord B -> ( A C_ B -> A C. C ) ) ) ) |
11 |
10
|
imp32 |
|- ( ( Ord C /\ ( B e. C /\ Ord B ) ) -> ( A C_ B -> A C. C ) ) |
12 |
11
|
com12 |
|- ( A C_ B -> ( ( Ord C /\ ( B e. C /\ Ord B ) ) -> A C. C ) ) |
13 |
4 12
|
syl9 |
|- ( Ord C -> ( A C_ B -> ( B e. C -> A C. C ) ) ) |
14 |
13
|
impd |
|- ( Ord C -> ( ( A C_ B /\ B e. C ) -> A C. C ) ) |
15 |
14
|
adantl |
|- ( ( Ord A /\ Ord C ) -> ( ( A C_ B /\ B e. C ) -> A C. C ) ) |
16 |
|
ordelpss |
|- ( ( Ord A /\ Ord C ) -> ( A e. C <-> A C. C ) ) |
17 |
15 16
|
sylibrd |
|- ( ( Ord A /\ Ord C ) -> ( ( A C_ B /\ B e. C ) -> A e. C ) ) |