Step |
Hyp |
Ref |
Expression |
1 |
|
aomclem3.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 |
|
aomclem3.c |
|- C = ( a e. _V |-> sup ( ( y ` a ) , ( R1 ` dom z ) , B ) ) |
3 |
|
aomclem3.d |
|- D = recs ( ( a e. _V |-> ( C ` ( ( R1 ` dom z ) \ ran a ) ) ) ) |
4 |
|
aomclem3.e |
|- E = { <. a , b >. | |^| ( `' D " { a } ) e. |^| ( `' D " { b } ) } |
5 |
|
aomclem3.on |
|- ( ph -> dom z e. On ) |
6 |
|
aomclem3.su |
|- ( ph -> dom z = suc U. dom z ) |
7 |
|
aomclem3.we |
|- ( ph -> A. a e. dom z ( z ` a ) We ( R1 ` a ) ) |
8 |
|
aomclem3.a |
|- ( ph -> A e. On ) |
9 |
|
aomclem3.za |
|- ( ph -> dom z C_ A ) |
10 |
|
aomclem3.y |
|- ( ph -> A. a e. ~P ( R1 ` A ) ( a =/= (/) -> ( y ` a ) e. ( ( ~P a i^i Fin ) \ { (/) } ) ) ) |
11 |
|
rneq |
|- ( a = c -> ran a = ran c ) |
12 |
11
|
difeq2d |
|- ( a = c -> ( ( R1 ` dom z ) \ ran a ) = ( ( R1 ` dom z ) \ ran c ) ) |
13 |
12
|
fveq2d |
|- ( a = c -> ( C ` ( ( R1 ` dom z ) \ ran a ) ) = ( C ` ( ( R1 ` dom z ) \ ran c ) ) ) |
14 |
13
|
cbvmptv |
|- ( a e. _V |-> ( C ` ( ( R1 ` dom z ) \ ran a ) ) ) = ( c e. _V |-> ( C ` ( ( R1 ` dom z ) \ ran c ) ) ) |
15 |
|
recseq |
|- ( ( a e. _V |-> ( C ` ( ( R1 ` dom z ) \ ran a ) ) ) = ( c e. _V |-> ( C ` ( ( R1 ` dom z ) \ ran c ) ) ) -> recs ( ( a e. _V |-> ( C ` ( ( R1 ` dom z ) \ ran a ) ) ) ) = recs ( ( c e. _V |-> ( C ` ( ( R1 ` dom z ) \ ran c ) ) ) ) ) |
16 |
14 15
|
ax-mp |
|- recs ( ( a e. _V |-> ( C ` ( ( R1 ` dom z ) \ ran a ) ) ) ) = recs ( ( c e. _V |-> ( C ` ( ( R1 ` dom z ) \ ran c ) ) ) ) |
17 |
3 16
|
eqtri |
|- D = recs ( ( c e. _V |-> ( C ` ( ( R1 ` dom z ) \ ran c ) ) ) ) |
18 |
|
fvexd |
|- ( ph -> ( R1 ` dom z ) e. _V ) |
19 |
1 2 5 6 7 8 9 10
|
aomclem2 |
|- ( ph -> A. a e. ~P ( R1 ` dom z ) ( a =/= (/) -> ( C ` a ) e. a ) ) |
20 |
|
neeq1 |
|- ( a = d -> ( a =/= (/) <-> d =/= (/) ) ) |
21 |
|
fveq2 |
|- ( a = d -> ( C ` a ) = ( C ` d ) ) |
22 |
|
id |
|- ( a = d -> a = d ) |
23 |
21 22
|
eleq12d |
|- ( a = d -> ( ( C ` a ) e. a <-> ( C ` d ) e. d ) ) |
24 |
20 23
|
imbi12d |
|- ( a = d -> ( ( a =/= (/) -> ( C ` a ) e. a ) <-> ( d =/= (/) -> ( C ` d ) e. d ) ) ) |
25 |
24
|
cbvralvw |
|- ( A. a e. ~P ( R1 ` dom z ) ( a =/= (/) -> ( C ` a ) e. a ) <-> A. d e. ~P ( R1 ` dom z ) ( d =/= (/) -> ( C ` d ) e. d ) ) |
26 |
19 25
|
sylib |
|- ( ph -> A. d e. ~P ( R1 ` dom z ) ( d =/= (/) -> ( C ` d ) e. d ) ) |
27 |
17 18 26 4
|
dnwech |
|- ( ph -> E We ( R1 ` dom z ) ) |