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

Metamath Proof Explorer

Theorem zorn2lem5

Description: Lemma for zorn2 . (Contributed by NM, 4-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 }
zorn2lem.7 
|- H = { z e. A | A. g e. ( F " y ) g R z }
Assertion zorn2lem5 
|- ( ( ( w We A /\ x e. On ) /\ A. y e. x H =/= (/) ) -> ( F " x ) C_ A )

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 zorn2lem.7 
 |-  H = { z e. A | A. g e. ( F " y ) g R z }
5 1 tfr1 
 |-  F Fn On
6 fnfun 
 |-  ( F Fn On -> Fun F )
7 5 6 ax-mp 
 |-  Fun F
8 fvelima 
 |-  ( ( Fun F /\ s e. ( F " x ) ) -> E. y e. x ( F ` y ) = s )
9 7 8 mpan 
 |-  ( s e. ( F " x ) -> E. y e. x ( F ` y ) = s )
10 nfv 
 |-  F/ y ( w We A /\ x e. On )
11 nfra1 
 |-  F/ y A. y e. x H =/= (/)
12 10 11 nfan 
 |-  F/ y ( ( w We A /\ x e. On ) /\ A. y e. x H =/= (/) )
13 nfv 
 |-  F/ y s e. A
14 df-ral 
 |-  ( A. y e. x H =/= (/) <-> A. y ( y e. x -> H =/= (/) ) )
15 onelon 
 |-  ( ( x e. On /\ y e. x ) -> y e. On )
16 4 ssrab3 
 |-  H C_ A
17 1 2 4 zorn2lem1 
 |-  ( ( y e. On /\ ( w We A /\ H =/= (/) ) ) -> ( F ` y ) e. H )
18 16 17 sselid 
 |-  ( ( y e. On /\ ( w We A /\ H =/= (/) ) ) -> ( F ` y ) e. A )
19 eleq1 
 |-  ( ( F ` y ) = s -> ( ( F ` y ) e. A <-> s e. A ) )
20 18 19 imbitrid 
 |-  ( ( F ` y ) = s -> ( ( y e. On /\ ( w We A /\ H =/= (/) ) ) -> s e. A ) )
21 15 20 sylani 
 |-  ( ( F ` y ) = s -> ( ( ( x e. On /\ y e. x ) /\ ( w We A /\ H =/= (/) ) ) -> s e. A ) )
22 21 com12 
 |-  ( ( ( x e. On /\ y e. x ) /\ ( w We A /\ H =/= (/) ) ) -> ( ( F ` y ) = s -> s e. A ) )
23 22 exp43 
 |-  ( x e. On -> ( y e. x -> ( w We A -> ( H =/= (/) -> ( ( F ` y ) = s -> s e. A ) ) ) ) )
24 23 com3r 
 |-  ( w We A -> ( x e. On -> ( y e. x -> ( H =/= (/) -> ( ( F ` y ) = s -> s e. A ) ) ) ) )
25 24 imp 
 |-  ( ( w We A /\ x e. On ) -> ( y e. x -> ( H =/= (/) -> ( ( F ` y ) = s -> s e. A ) ) ) )
26 25 a2d 
 |-  ( ( w We A /\ x e. On ) -> ( ( y e. x -> H =/= (/) ) -> ( y e. x -> ( ( F ` y ) = s -> s e. A ) ) ) )
27 26 spsd 
 |-  ( ( w We A /\ x e. On ) -> ( A. y ( y e. x -> H =/= (/) ) -> ( y e. x -> ( ( F ` y ) = s -> s e. A ) ) ) )
28 14 27 biimtrid 
 |-  ( ( w We A /\ x e. On ) -> ( A. y e. x H =/= (/) -> ( y e. x -> ( ( F ` y ) = s -> s e. A ) ) ) )
29 28 imp 
 |-  ( ( ( w We A /\ x e. On ) /\ A. y e. x H =/= (/) ) -> ( y e. x -> ( ( F ` y ) = s -> s e. A ) ) )
30 12 13 29 rexlimd 
 |-  ( ( ( w We A /\ x e. On ) /\ A. y e. x H =/= (/) ) -> ( E. y e. x ( F ` y ) = s -> s e. A ) )
31 9 30 syl5 
 |-  ( ( ( w We A /\ x e. On ) /\ A. y e. x H =/= (/) ) -> ( s e. ( F " x ) -> s e. A ) )
32 31 ssrdv 
 |-  ( ( ( w We A /\ x e. On ) /\ A. y e. x H =/= (/) ) -> ( F " x ) C_ A )