Metamath Proof Explorer


Theorem zorn2lem3

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 zorn2lem3
|- ( ( R Po A /\ ( x e. On /\ ( w We A /\ D =/= (/) ) ) ) -> ( y e. x -> -. ( F ` x ) = ( F ` y ) ) )

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