Step |
Hyp |
Ref |
Expression |
1 |
|
zorn2lem.3 |
|- F = recs ( ( f e. _V |-> ( iota_ v e. C A. u e. C -. u w v ) ) ) |
2 |
|
zorn2lem.4 |
|- C = { z e. A | A. g e. ran f g R z } |
3 |
|
zorn2lem.5 |
|- D = { z e. A | A. g e. ( F " x ) g R z } |
4 |
1 2 3
|
zorn2lem2 |
|- ( ( x e. On /\ ( w We A /\ D =/= (/) ) ) -> ( y e. x -> ( F ` y ) R ( F ` x ) ) ) |
5 |
4
|
adantl |
|- ( ( R Po A /\ ( x e. On /\ ( w We A /\ D =/= (/) ) ) ) -> ( y e. x -> ( F ` y ) R ( F ` x ) ) ) |
6 |
3
|
ssrab3 |
|- D C_ A |
7 |
1 2 3
|
zorn2lem1 |
|- ( ( x e. On /\ ( w We A /\ D =/= (/) ) ) -> ( F ` x ) e. D ) |
8 |
6 7
|
sselid |
|- ( ( x e. On /\ ( w We A /\ D =/= (/) ) ) -> ( F ` x ) e. A ) |
9 |
|
breq1 |
|- ( ( F ` x ) = ( F ` y ) -> ( ( F ` x ) R ( F ` x ) <-> ( F ` y ) R ( F ` x ) ) ) |
10 |
9
|
biimprcd |
|- ( ( F ` y ) R ( F ` x ) -> ( ( F ` x ) = ( F ` y ) -> ( F ` x ) R ( F ` x ) ) ) |
11 |
|
poirr |
|- ( ( R Po A /\ ( F ` x ) e. A ) -> -. ( F ` x ) R ( F ` x ) ) |
12 |
10 11
|
nsyli |
|- ( ( F ` y ) R ( F ` x ) -> ( ( R Po A /\ ( F ` x ) e. A ) -> -. ( F ` x ) = ( F ` y ) ) ) |
13 |
12
|
com12 |
|- ( ( R Po A /\ ( F ` x ) e. A ) -> ( ( F ` y ) R ( F ` x ) -> -. ( F ` x ) = ( F ` y ) ) ) |
14 |
8 13
|
sylan2 |
|- ( ( R Po A /\ ( x e. On /\ ( w We A /\ D =/= (/) ) ) ) -> ( ( F ` y ) R ( F ` x ) -> -. ( F ` x ) = ( F ` y ) ) ) |
15 |
5 14
|
syld |
|- ( ( R Po A /\ ( x e. On /\ ( w We A /\ D =/= (/) ) ) ) -> ( y e. x -> -. ( F ` x ) = ( F ` y ) ) ) |