This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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