Metamath Proof Explorer

Theorem zorn2lem4

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 zorn2lem4 
|- ( ( R Po A /\ w We A ) -> E. x e. On 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 pm3.24 
 |-  -. ( ran F e. _V /\ -. ran F e. _V )
5 df-ne 
 |-  ( D =/= (/) <-> -. D = (/) )
6 5 ralbii 
 |-  ( A. x e. On D =/= (/) <-> A. x e. On -. D = (/) )
7 df-ral 
 |-  ( A. x e. On D =/= (/) <-> A. x ( x e. On -> D =/= (/) ) )
8 ralnex 
 |-  ( A. x e. On -. D = (/) <-> -. E. x e. On D = (/) )
9 6 7 8 3bitr3i 
 |-  ( A. x ( x e. On -> D =/= (/) ) <-> -. E. x e. On D = (/) )
10 weso 
 |-  ( w We A -> w Or A )
11 10 adantr 
 |-  ( ( w We A /\ A. x ( x e. On -> D =/= (/) ) ) -> w Or A )
12 vex 
 |-  w e. _V
13 soex 
 |-  ( ( w Or A /\ w e. _V ) -> A e. _V )
14 11 12 13 sylancl 
 |-  ( ( w We A /\ A. x ( x e. On -> D =/= (/) ) ) -> A e. _V )
15 1 tfr1 
 |-  F Fn On
16 fvelrnb 
 |-  ( F Fn On -> ( y e. ran F <-> E. x e. On ( F ` x ) = y ) )
17 15 16 ax-mp 
 |-  ( y e. ran F <-> E. x e. On ( F ` x ) = y )
18 nfv 
 |-  F/ x w We A
19 nfa1 
 |-  F/ x A. x ( x e. On -> D =/= (/) )
20 18 19 nfan 
 |-  F/ x ( w We A /\ A. x ( x e. On -> D =/= (/) ) )
21 nfv 
 |-  F/ x y e. A
22 3 ssrab3 
 |-  D C_ A
23 1 2 3 zorn2lem1 
 |-  ( ( x e. On /\ ( w We A /\ D =/= (/) ) ) -> ( F ` x ) e. D )
24 22 23 sselid 
 |-  ( ( x e. On /\ ( w We A /\ D =/= (/) ) ) -> ( F ` x ) e. A )
25 eleq1 
 |-  ( ( F ` x ) = y -> ( ( F ` x ) e. A <-> y e. A ) )
26 24 25 syl5ibcom 
 |-  ( ( x e. On /\ ( w We A /\ D =/= (/) ) ) -> ( ( F ` x ) = y -> y e. A ) )
27 26 exp32 
 |-  ( x e. On -> ( w We A -> ( D =/= (/) -> ( ( F ` x ) = y -> y e. A ) ) ) )
28 27 com12 
 |-  ( w We A -> ( x e. On -> ( D =/= (/) -> ( ( F ` x ) = y -> y e. A ) ) ) )
29 28 a2d 
 |-  ( w We A -> ( ( x e. On -> D =/= (/) ) -> ( x e. On -> ( ( F ` x ) = y -> y e. A ) ) ) )
30 29 spsd 
 |-  ( w We A -> ( A. x ( x e. On -> D =/= (/) ) -> ( x e. On -> ( ( F ` x ) = y -> y e. A ) ) ) )
31 30 imp 
 |-  ( ( w We A /\ A. x ( x e. On -> D =/= (/) ) ) -> ( x e. On -> ( ( F ` x ) = y -> y e. A ) ) )
32 20 21 31 rexlimd 
 |-  ( ( w We A /\ A. x ( x e. On -> D =/= (/) ) ) -> ( E. x e. On ( F ` x ) = y -> y e. A ) )
33 17 32 syl5bi 
 |-  ( ( w We A /\ A. x ( x e. On -> D =/= (/) ) ) -> ( y e. ran F -> y e. A ) )
34 33 ssrdv 
 |-  ( ( w We A /\ A. x ( x e. On -> D =/= (/) ) ) -> ran F C_ A )
35 14 34 ssexd 
 |-  ( ( w We A /\ A. x ( x e. On -> D =/= (/) ) ) -> ran F e. _V )
36 35 ex 
 |-  ( w We A -> ( A. x ( x e. On -> D =/= (/) ) -> ran F e. _V ) )
37 36 adantl 
 |-  ( ( R Po A /\ w We A ) -> ( A. x ( x e. On -> D =/= (/) ) -> ran F e. _V ) )
38 1 2 3 zorn2lem3 
 |-  ( ( R Po A /\ ( x e. On /\ ( w We A /\ D =/= (/) ) ) ) -> ( y e. x -> -. ( F ` x ) = ( F ` y ) ) )
39 38 exp45 
 |-  ( R Po A -> ( x e. On -> ( w We A -> ( D =/= (/) -> ( y e. x -> -. ( F ` x ) = ( F ` y ) ) ) ) ) )
40 39 com23 
 |-  ( R Po A -> ( w We A -> ( x e. On -> ( D =/= (/) -> ( y e. x -> -. ( F ` x ) = ( F ` y ) ) ) ) ) )
41 40 imp 
 |-  ( ( R Po A /\ w We A ) -> ( x e. On -> ( D =/= (/) -> ( y e. x -> -. ( F ` x ) = ( F ` y ) ) ) ) )
42 41 a2d 
 |-  ( ( R Po A /\ w We A ) -> ( ( x e. On -> D =/= (/) ) -> ( x e. On -> ( y e. x -> -. ( F ` x ) = ( F ` y ) ) ) ) )
43 42 imp4a 
 |-  ( ( R Po A /\ w We A ) -> ( ( x e. On -> D =/= (/) ) -> ( ( x e. On /\ y e. x ) -> -. ( F ` x ) = ( F ` y ) ) ) )
44 43 alrimdv 
 |-  ( ( R Po A /\ w We A ) -> ( ( x e. On -> D =/= (/) ) -> A. y ( ( x e. On /\ y e. x ) -> -. ( F ` x ) = ( F ` y ) ) ) )
45 44 alimdv 
 |-  ( ( R Po A /\ w We A ) -> ( A. x ( x e. On -> D =/= (/) ) -> A. x A. y ( ( x e. On /\ y e. x ) -> -. ( F ` x ) = ( F ` y ) ) ) )
46 r2al 
 |-  ( A. x e. On A. y e. x -. ( F ` x ) = ( F ` y ) <-> A. x A. y ( ( x e. On /\ y e. x ) -> -. ( F ` x ) = ( F ` y ) ) )
47 45 46 syl6ibr 
 |-  ( ( R Po A /\ w We A ) -> ( A. x ( x e. On -> D =/= (/) ) -> A. x e. On A. y e. x -. ( F ` x ) = ( F ` y ) ) )
48 ssid 
 |-  On C_ On
49 15 tz7.48lem 
 |-  ( ( On C_ On /\ A. x e. On A. y e. x -. ( F ` x ) = ( F ` y ) ) -> Fun `' ( F |` On ) )
50 48 49 mpan 
 |-  ( A. x e. On A. y e. x -. ( F ` x ) = ( F ` y ) -> Fun `' ( F |` On ) )
51 fnrel 
 |-  ( F Fn On -> Rel F )
52 15 51 ax-mp 
 |-  Rel F
53 15 fndmi 
 |-  dom F = On
54 53 eqimssi 
 |-  dom F C_ On
55 relssres 
 |-  ( ( Rel F /\ dom F C_ On ) -> ( F |` On ) = F )
56 52 54 55 mp2an 
 |-  ( F |` On ) = F
57 56 cnveqi 
 |-  `' ( F |` On ) = `' F
58 57 funeqi 
 |-  ( Fun `' ( F |` On ) <-> Fun `' F )
59 50 58 sylib 
 |-  ( A. x e. On A. y e. x -. ( F ` x ) = ( F ` y ) -> Fun `' F )
60 47 59 syl6 
 |-  ( ( R Po A /\ w We A ) -> ( A. x ( x e. On -> D =/= (/) ) -> Fun `' F ) )
61 onprc 
 |-  -. On e. _V
62 funrnex 
 |-  ( dom `' F e. _V -> ( Fun `' F -> ran `' F e. _V ) )
63 62 com12 
 |-  ( Fun `' F -> ( dom `' F e. _V -> ran `' F e. _V ) )
64 df-rn 
 |-  ran F = dom `' F
65 64 eleq1i 
 |-  ( ran F e. _V <-> dom `' F e. _V )
66 dfdm4 
 |-  dom F = ran `' F
67 53 66 eqtr3i 
 |-  On = ran `' F
68 67 eleq1i 
 |-  ( On e. _V <-> ran `' F e. _V )
69 63 65 68 3imtr4g 
 |-  ( Fun `' F -> ( ran F e. _V -> On e. _V ) )
70 61 69 mtoi 
 |-  ( Fun `' F -> -. ran F e. _V )
71 60 70 syl6 
 |-  ( ( R Po A /\ w We A ) -> ( A. x ( x e. On -> D =/= (/) ) -> -. ran F e. _V ) )
72 37 71 jcad 
 |-  ( ( R Po A /\ w We A ) -> ( A. x ( x e. On -> D =/= (/) ) -> ( ran F e. _V /\ -. ran F e. _V ) ) )
73 9 72 syl5bir 
 |-  ( ( R Po A /\ w We A ) -> ( -. E. x e. On D = (/) -> ( ran F e. _V /\ -. ran F e. _V ) ) )
74 4 73 mt3i 
 |-  ( ( R Po A /\ w We A ) -> E. x e. On D = (/) )