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