Step |
Hyp |
Ref |
Expression |
1 |
|
aomclem2.b |
|- B = { <. a , b >. | E. c e. ( R1 ` U. dom z ) ( ( c e. b /\ -. c e. a ) /\ A. d e. ( R1 ` U. dom z ) ( d ( z ` U. dom z ) c -> ( d e. a <-> d e. b ) ) ) } |
2 |
|
aomclem2.c |
|- C = ( a e. _V |-> sup ( ( y ` a ) , ( R1 ` dom z ) , B ) ) |
3 |
|
aomclem2.on |
|- ( ph -> dom z e. On ) |
4 |
|
aomclem2.su |
|- ( ph -> dom z = suc U. dom z ) |
5 |
|
aomclem2.we |
|- ( ph -> A. a e. dom z ( z ` a ) We ( R1 ` a ) ) |
6 |
|
aomclem2.a |
|- ( ph -> A e. On ) |
7 |
|
aomclem2.za |
|- ( ph -> dom z C_ A ) |
8 |
|
aomclem2.y |
|- ( ph -> A. a e. ~P ( R1 ` A ) ( a =/= (/) -> ( y ` a ) e. ( ( ~P a i^i Fin ) \ { (/) } ) ) ) |
9 |
|
vex |
|- a e. _V |
10 |
3 6
|
jca |
|- ( ph -> ( dom z e. On /\ A e. On ) ) |
11 |
|
r1ord3 |
|- ( ( dom z e. On /\ A e. On ) -> ( dom z C_ A -> ( R1 ` dom z ) C_ ( R1 ` A ) ) ) |
12 |
10 7 11
|
sylc |
|- ( ph -> ( R1 ` dom z ) C_ ( R1 ` A ) ) |
13 |
12
|
sspwd |
|- ( ph -> ~P ( R1 ` dom z ) C_ ~P ( R1 ` A ) ) |
14 |
13
|
sseld |
|- ( ph -> ( a e. ~P ( R1 ` dom z ) -> a e. ~P ( R1 ` A ) ) ) |
15 |
|
rsp |
|- ( A. a e. ~P ( R1 ` A ) ( a =/= (/) -> ( y ` a ) e. ( ( ~P a i^i Fin ) \ { (/) } ) ) -> ( a e. ~P ( R1 ` A ) -> ( a =/= (/) -> ( y ` a ) e. ( ( ~P a i^i Fin ) \ { (/) } ) ) ) ) |
16 |
8 14 15
|
sylsyld |
|- ( ph -> ( a e. ~P ( R1 ` dom z ) -> ( a =/= (/) -> ( y ` a ) e. ( ( ~P a i^i Fin ) \ { (/) } ) ) ) ) |
17 |
16
|
3imp |
|- ( ( ph /\ a e. ~P ( R1 ` dom z ) /\ a =/= (/) ) -> ( y ` a ) e. ( ( ~P a i^i Fin ) \ { (/) } ) ) |
18 |
17
|
eldifad |
|- ( ( ph /\ a e. ~P ( R1 ` dom z ) /\ a =/= (/) ) -> ( y ` a ) e. ( ~P a i^i Fin ) ) |
19 |
|
inss1 |
|- ( ~P a i^i Fin ) C_ ~P a |
20 |
19
|
sseli |
|- ( ( y ` a ) e. ( ~P a i^i Fin ) -> ( y ` a ) e. ~P a ) |
21 |
20
|
elpwid |
|- ( ( y ` a ) e. ( ~P a i^i Fin ) -> ( y ` a ) C_ a ) |
22 |
18 21
|
syl |
|- ( ( ph /\ a e. ~P ( R1 ` dom z ) /\ a =/= (/) ) -> ( y ` a ) C_ a ) |
23 |
1 3 4 5
|
aomclem1 |
|- ( ph -> B Or ( R1 ` dom z ) ) |
24 |
23
|
3ad2ant1 |
|- ( ( ph /\ a e. ~P ( R1 ` dom z ) /\ a =/= (/) ) -> B Or ( R1 ` dom z ) ) |
25 |
|
inss2 |
|- ( ~P a i^i Fin ) C_ Fin |
26 |
25 18
|
sseldi |
|- ( ( ph /\ a e. ~P ( R1 ` dom z ) /\ a =/= (/) ) -> ( y ` a ) e. Fin ) |
27 |
|
eldifsni |
|- ( ( y ` a ) e. ( ( ~P a i^i Fin ) \ { (/) } ) -> ( y ` a ) =/= (/) ) |
28 |
17 27
|
syl |
|- ( ( ph /\ a e. ~P ( R1 ` dom z ) /\ a =/= (/) ) -> ( y ` a ) =/= (/) ) |
29 |
|
elpwi |
|- ( a e. ~P ( R1 ` dom z ) -> a C_ ( R1 ` dom z ) ) |
30 |
29
|
3ad2ant2 |
|- ( ( ph /\ a e. ~P ( R1 ` dom z ) /\ a =/= (/) ) -> a C_ ( R1 ` dom z ) ) |
31 |
22 30
|
sstrd |
|- ( ( ph /\ a e. ~P ( R1 ` dom z ) /\ a =/= (/) ) -> ( y ` a ) C_ ( R1 ` dom z ) ) |
32 |
|
fisupcl |
|- ( ( B Or ( R1 ` dom z ) /\ ( ( y ` a ) e. Fin /\ ( y ` a ) =/= (/) /\ ( y ` a ) C_ ( R1 ` dom z ) ) ) -> sup ( ( y ` a ) , ( R1 ` dom z ) , B ) e. ( y ` a ) ) |
33 |
24 26 28 31 32
|
syl13anc |
|- ( ( ph /\ a e. ~P ( R1 ` dom z ) /\ a =/= (/) ) -> sup ( ( y ` a ) , ( R1 ` dom z ) , B ) e. ( y ` a ) ) |
34 |
22 33
|
sseldd |
|- ( ( ph /\ a e. ~P ( R1 ` dom z ) /\ a =/= (/) ) -> sup ( ( y ` a ) , ( R1 ` dom z ) , B ) e. a ) |
35 |
2
|
fvmpt2 |
|- ( ( a e. _V /\ sup ( ( y ` a ) , ( R1 ` dom z ) , B ) e. a ) -> ( C ` a ) = sup ( ( y ` a ) , ( R1 ` dom z ) , B ) ) |
36 |
9 34 35
|
sylancr |
|- ( ( ph /\ a e. ~P ( R1 ` dom z ) /\ a =/= (/) ) -> ( C ` a ) = sup ( ( y ` a ) , ( R1 ` dom z ) , B ) ) |
37 |
36 34
|
eqeltrd |
|- ( ( ph /\ a e. ~P ( R1 ` dom z ) /\ a =/= (/) ) -> ( C ` a ) e. a ) |
38 |
37
|
3exp |
|- ( ph -> ( a e. ~P ( R1 ` dom z ) -> ( a =/= (/) -> ( C ` a ) e. a ) ) ) |
39 |
38
|
ralrimiv |
|- ( ph -> A. a e. ~P ( R1 ` dom z ) ( a =/= (/) -> ( C ` a ) e. a ) ) |