Step |
Hyp |
Ref |
Expression |
1 |
|
supgtoreq.1 |
|- ( ph -> R Or A ) |
2 |
|
supgtoreq.2 |
|- ( ph -> B C_ A ) |
3 |
|
supgtoreq.3 |
|- ( ph -> B e. Fin ) |
4 |
|
supgtoreq.4 |
|- ( ph -> C e. B ) |
5 |
|
supgtoreq.5 |
|- ( ph -> S = sup ( B , A , R ) ) |
6 |
4
|
ne0d |
|- ( ph -> B =/= (/) ) |
7 |
|
fisup2g |
|- ( ( R Or A /\ ( B e. Fin /\ B =/= (/) /\ B C_ A ) ) -> E. x e. B ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) ) |
8 |
1 3 6 2 7
|
syl13anc |
|- ( ph -> E. x e. B ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) ) |
9 |
|
ssrexv |
|- ( B C_ A -> ( E. x e. B ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) -> E. x e. A ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) ) ) |
10 |
2 8 9
|
sylc |
|- ( ph -> E. x e. A ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) ) |
11 |
1 10
|
supub |
|- ( ph -> ( C e. B -> -. sup ( B , A , R ) R C ) ) |
12 |
4 11
|
mpd |
|- ( ph -> -. sup ( B , A , R ) R C ) |
13 |
5 12
|
eqnbrtrd |
|- ( ph -> -. S R C ) |
14 |
|
fisupcl |
|- ( ( R Or A /\ ( B e. Fin /\ B =/= (/) /\ B C_ A ) ) -> sup ( B , A , R ) e. B ) |
15 |
1 3 6 2 14
|
syl13anc |
|- ( ph -> sup ( B , A , R ) e. B ) |
16 |
2 15
|
sseldd |
|- ( ph -> sup ( B , A , R ) e. A ) |
17 |
5 16
|
eqeltrd |
|- ( ph -> S e. A ) |
18 |
2 4
|
sseldd |
|- ( ph -> C e. A ) |
19 |
|
sotric |
|- ( ( R Or A /\ ( S e. A /\ C e. A ) ) -> ( S R C <-> -. ( S = C \/ C R S ) ) ) |
20 |
1 17 18 19
|
syl12anc |
|- ( ph -> ( S R C <-> -. ( S = C \/ C R S ) ) ) |
21 |
|
orcom |
|- ( ( S = C \/ C R S ) <-> ( C R S \/ S = C ) ) |
22 |
|
eqcom |
|- ( S = C <-> C = S ) |
23 |
22
|
orbi2i |
|- ( ( C R S \/ S = C ) <-> ( C R S \/ C = S ) ) |
24 |
21 23
|
bitri |
|- ( ( S = C \/ C R S ) <-> ( C R S \/ C = S ) ) |
25 |
24
|
notbii |
|- ( -. ( S = C \/ C R S ) <-> -. ( C R S \/ C = S ) ) |
26 |
20 25
|
bitr2di |
|- ( ph -> ( -. ( C R S \/ C = S ) <-> S R C ) ) |
27 |
13 26
|
mtbird |
|- ( ph -> -. -. ( C R S \/ C = S ) ) |
28 |
27
|
notnotrd |
|- ( ph -> ( C R S \/ C = S ) ) |