Metamath Proof Explorer

Theorem zorn2lem2

Description: Lemma for zorn2 . (Contributed by NM, 3-Apr-1997) (Revised by Mario Carneiro, 9-May-2015)

Ref Expression
Hypotheses zorn2lem.3 
|- F = recs ( ( f e. _V |-> ( iota_ v e. C A. u e. C -. u w v ) ) )
zorn2lem.4 
|- C = { z e. A | A. g e. ran f g R z }
zorn2lem.5 
|- D = { z e. A | A. g e. ( F " x ) g R z }
Assertion zorn2lem2 
|- ( ( x e. On /\ ( w We A /\ D =/= (/) ) ) -> ( y e. x -> ( F ` y ) R ( F ` x ) ) )

Proof

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 ) ) )