| 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
|
zorn2lem1 |
|- ( ( x e. On /\ ( w We A /\ D =/= (/) ) ) -> ( F ` x ) e. D ) |
| 5 |
|
breq2 |
|- ( z = ( F ` x ) -> ( g R z <-> g R ( F ` x ) ) ) |
| 6 |
5
|
ralbidv |
|- ( z = ( F ` x ) -> ( A. g e. ( F " x ) g R z <-> A. g e. ( F " x ) g R ( F ` x ) ) ) |
| 7 |
6 3
|
elrab2 |
|- ( ( F ` x ) e. D <-> ( ( F ` x ) e. A /\ A. g e. ( F " x ) g R ( F ` x ) ) ) |
| 8 |
7
|
simprbi |
|- ( ( F ` x ) e. D -> A. g e. ( F " x ) g R ( F ` x ) ) |
| 9 |
4 8
|
syl |
|- ( ( x e. On /\ ( w We A /\ D =/= (/) ) ) -> A. g e. ( F " x ) g R ( F ` x ) ) |
| 10 |
1
|
tfr1 |
|- F Fn On |
| 11 |
|
onss |
|- ( x e. On -> x C_ On ) |
| 12 |
|
fnfvima |
|- ( ( F Fn On /\ x C_ On /\ y e. x ) -> ( F ` y ) e. ( F " x ) ) |
| 13 |
12
|
3expia |
|- ( ( F Fn On /\ x C_ On ) -> ( y e. x -> ( F ` y ) e. ( F " x ) ) ) |
| 14 |
10 11 13
|
sylancr |
|- ( x e. On -> ( y e. x -> ( F ` y ) e. ( F " x ) ) ) |
| 15 |
14
|
adantr |
|- ( ( x e. On /\ ( w We A /\ D =/= (/) ) ) -> ( y e. x -> ( F ` y ) e. ( F " x ) ) ) |
| 16 |
|
breq1 |
|- ( g = ( F ` y ) -> ( g R ( F ` x ) <-> ( F ` y ) R ( F ` x ) ) ) |
| 17 |
16
|
rspccv |
|- ( A. g e. ( F " x ) g R ( F ` x ) -> ( ( F ` y ) e. ( F " x ) -> ( F ` y ) R ( F ` x ) ) ) |
| 18 |
9 15 17
|
sylsyld |
|- ( ( x e. On /\ ( w We A /\ D =/= (/) ) ) -> ( y e. x -> ( F ` y ) R ( F ` x ) ) ) |