Step |
Hyp |
Ref |
Expression |
1 |
|
fisupclrnmpt.x |
|- F/ x ph |
2 |
|
fisupclrnmpt.r |
|- ( ph -> R Or A ) |
3 |
|
fisupclrnmpt.b |
|- ( ph -> B e. Fin ) |
4 |
|
fisupclrnmpt.n |
|- ( ph -> B =/= (/) ) |
5 |
|
fisupclrnmpt.c |
|- ( ( ph /\ x e. B ) -> C e. A ) |
6 |
|
eqid |
|- ( x e. B |-> C ) = ( x e. B |-> C ) |
7 |
1 6 5
|
rnmptssd |
|- ( ph -> ran ( x e. B |-> C ) C_ A ) |
8 |
6
|
rnmptfi |
|- ( B e. Fin -> ran ( x e. B |-> C ) e. Fin ) |
9 |
3 8
|
syl |
|- ( ph -> ran ( x e. B |-> C ) e. Fin ) |
10 |
1 5 6 4
|
rnmptn0 |
|- ( ph -> ran ( x e. B |-> C ) =/= (/) ) |
11 |
|
fisupcl |
|- ( ( R Or A /\ ( ran ( x e. B |-> C ) e. Fin /\ ran ( x e. B |-> C ) =/= (/) /\ ran ( x e. B |-> C ) C_ A ) ) -> sup ( ran ( x e. B |-> C ) , A , R ) e. ran ( x e. B |-> C ) ) |
12 |
2 9 10 7 11
|
syl13anc |
|- ( ph -> sup ( ran ( x e. B |-> C ) , A , R ) e. ran ( x e. B |-> C ) ) |
13 |
7 12
|
sseldd |
|- ( ph -> sup ( ran ( x e. B |-> C ) , A , R ) e. A ) |