Metamath Proof Explorer

Theorem zorn2lem1

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

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 tfr2 
 |-  ( x e. On -> ( F ` x ) = ( ( f e. _V |-> ( iota_ v e. C A. u e. C -. u w v ) ) ` ( F |` x ) ) )
5 4 adantr 
 |-  ( ( x e. On /\ ( w We A /\ D =/= (/) ) ) -> ( F ` x ) = ( ( f e. _V |-> ( iota_ v e. C A. u e. C -. u w v ) ) ` ( F |` x ) ) )
6 1 tfr1 
 |-  F Fn On
7 fnfun 
 |-  ( F Fn On -> Fun F )
8 6 7 ax-mp 
 |-  Fun F
9 vex 
 |-  x e. _V
10 resfunexg 
 |-  ( ( Fun F /\ x e. _V ) -> ( F |` x ) e. _V )
11 8 9 10 mp2an 
 |-  ( F |` x ) e. _V
12 rneq 
 |-  ( f = ( F |` x ) -> ran f = ran ( F |` x ) )
13 df-ima 
 |-  ( F " x ) = ran ( F |` x )
14 12 13 eqtr4di 
 |-  ( f = ( F |` x ) -> ran f = ( F " x ) )
15 14 eleq2d 
 |-  ( f = ( F |` x ) -> ( g e. ran f <-> g e. ( F " x ) ) )
16 15 imbi1d 
 |-  ( f = ( F |` x ) -> ( ( g e. ran f -> g R z ) <-> ( g e. ( F " x ) -> g R z ) ) )
17 16 ralbidv2 
 |-  ( f = ( F |` x ) -> ( A. g e. ran f g R z <-> A. g e. ( F " x ) g R z ) )
18 17 rabbidv 
 |-  ( f = ( F |` x ) -> { z e. A | A. g e. ran f g R z } = { z e. A | A. g e. ( F " x ) g R z } )
19 18 2 3 3eqtr4g 
 |-  ( f = ( F |` x ) -> C = D )
20 19 eleq2d 
 |-  ( f = ( F |` x ) -> ( u e. C <-> u e. D ) )
21 20 imbi1d 
 |-  ( f = ( F |` x ) -> ( ( u e. C -> -. u w v ) <-> ( u e. D -> -. u w v ) ) )
22 21 ralbidv2 
 |-  ( f = ( F |` x ) -> ( A. u e. C -. u w v <-> A. u e. D -. u w v ) )
23 19 22 riotaeqbidv 
 |-  ( f = ( F |` x ) -> ( iota_ v e. C A. u e. C -. u w v ) = ( iota_ v e. D A. u e. D -. u w v ) )
24 eqid 
 |-  ( f e. _V |-> ( iota_ v e. C A. u e. C -. u w v ) ) = ( f e. _V |-> ( iota_ v e. C A. u e. C -. u w v ) )
25 riotaex 
 |-  ( iota_ v e. D A. u e. D -. u w v ) e. _V
26 23 24 25 fvmpt 
 |-  ( ( F |` x ) e. _V -> ( ( f e. _V |-> ( iota_ v e. C A. u e. C -. u w v ) ) ` ( F |` x ) ) = ( iota_ v e. D A. u e. D -. u w v ) )
27 11 26 ax-mp 
 |-  ( ( f e. _V |-> ( iota_ v e. C A. u e. C -. u w v ) ) ` ( F |` x ) ) = ( iota_ v e. D A. u e. D -. u w v )
28 5 27 eqtrdi 
 |-  ( ( x e. On /\ ( w We A /\ D =/= (/) ) ) -> ( F ` x ) = ( iota_ v e. D A. u e. D -. u w v ) )
29 simprl 
 |-  ( ( x e. On /\ ( w We A /\ D =/= (/) ) ) -> w We A )
30 weso 
 |-  ( w We A -> w Or A )
31 30 ad2antrl 
 |-  ( ( x e. On /\ ( w We A /\ D =/= (/) ) ) -> w Or A )
32 vex 
 |-  w e. _V
33 soex 
 |-  ( ( w Or A /\ w e. _V ) -> A e. _V )
34 31 32 33 sylancl 
 |-  ( ( x e. On /\ ( w We A /\ D =/= (/) ) ) -> A e. _V )
35 3 34 rabexd 
 |-  ( ( x e. On /\ ( w We A /\ D =/= (/) ) ) -> D e. _V )
36 3 ssrab3 
 |-  D C_ A
37 36 a1i 
 |-  ( ( x e. On /\ ( w We A /\ D =/= (/) ) ) -> D C_ A )
38 simprr 
 |-  ( ( x e. On /\ ( w We A /\ D =/= (/) ) ) -> D =/= (/) )
39 wereu 
 |-  ( ( w We A /\ ( D e. _V /\ D C_ A /\ D =/= (/) ) ) -> E! v e. D A. u e. D -. u w v )
40 29 35 37 38 39 syl13anc 
 |-  ( ( x e. On /\ ( w We A /\ D =/= (/) ) ) -> E! v e. D A. u e. D -. u w v )
41 riotacl 
 |-  ( E! v e. D A. u e. D -. u w v -> ( iota_ v e. D A. u e. D -. u w v ) e. D )
42 40 41 syl 
 |-  ( ( x e. On /\ ( w We A /\ D =/= (/) ) ) -> ( iota_ v e. D A. u e. D -. u w v ) e. D )
43 28 42 eqeltrd 
 |-  ( ( x e. On /\ ( w We A /\ D =/= (/) ) ) -> ( F ` x ) e. D )