# 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}=\mathrm{recs}\left(\left({f}\in \mathrm{V}⟼\left(\iota {v}\in {C}|\forall {u}\in {C}\phantom{\rule{.4em}{0ex}}¬{u}{w}{v}\right)\right)\right)$
zorn2lem.4 ${⊢}{C}=\left\{{z}\in {A}|\forall {g}\in \mathrm{ran}{f}\phantom{\rule{.4em}{0ex}}{g}{R}{z}\right\}$
zorn2lem.5 ${⊢}{D}=\left\{{z}\in {A}|\forall {g}\in {F}\left[{x}\right]\phantom{\rule{.4em}{0ex}}{g}{R}{z}\right\}$
Assertion zorn2lem4 ${⊢}\left({R}\mathrm{Po}{A}\wedge {w}\mathrm{We}{A}\right)\to \exists {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{D}=\varnothing$

### Proof

Step Hyp Ref Expression
1 zorn2lem.3 ${⊢}{F}=\mathrm{recs}\left(\left({f}\in \mathrm{V}⟼\left(\iota {v}\in {C}|\forall {u}\in {C}\phantom{\rule{.4em}{0ex}}¬{u}{w}{v}\right)\right)\right)$
2 zorn2lem.4 ${⊢}{C}=\left\{{z}\in {A}|\forall {g}\in \mathrm{ran}{f}\phantom{\rule{.4em}{0ex}}{g}{R}{z}\right\}$
3 zorn2lem.5 ${⊢}{D}=\left\{{z}\in {A}|\forall {g}\in {F}\left[{x}\right]\phantom{\rule{.4em}{0ex}}{g}{R}{z}\right\}$
4 pm3.24 ${⊢}¬\left(\mathrm{ran}{F}\in \mathrm{V}\wedge ¬\mathrm{ran}{F}\in \mathrm{V}\right)$
5 df-ne ${⊢}{D}\ne \varnothing ↔¬{D}=\varnothing$
6 5 ralbii ${⊢}\forall {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{D}\ne \varnothing ↔\forall {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}¬{D}=\varnothing$
7 df-ral ${⊢}\forall {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{D}\ne \varnothing ↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in \mathrm{On}\to {D}\ne \varnothing \right)$
8 ralnex ${⊢}\forall {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}¬{D}=\varnothing ↔¬\exists {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{D}=\varnothing$
9 6 7 8 3bitr3i ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in \mathrm{On}\to {D}\ne \varnothing \right)↔¬\exists {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{D}=\varnothing$
10 weso ${⊢}{w}\mathrm{We}{A}\to {w}\mathrm{Or}{A}$
11 10 adantr ${⊢}\left({w}\mathrm{We}{A}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in \mathrm{On}\to {D}\ne \varnothing \right)\right)\to {w}\mathrm{Or}{A}$
12 vex ${⊢}{w}\in \mathrm{V}$
13 soex ${⊢}\left({w}\mathrm{Or}{A}\wedge {w}\in \mathrm{V}\right)\to {A}\in \mathrm{V}$
14 11 12 13 sylancl ${⊢}\left({w}\mathrm{We}{A}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in \mathrm{On}\to {D}\ne \varnothing \right)\right)\to {A}\in \mathrm{V}$
15 1 tfr1 ${⊢}{F}Fn\mathrm{On}$
16 fvelrnb ${⊢}{F}Fn\mathrm{On}\to \left({y}\in \mathrm{ran}{F}↔\exists {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)={y}\right)$
17 15 16 ax-mp ${⊢}{y}\in \mathrm{ran}{F}↔\exists {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)={y}$
18 nfv ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{w}\mathrm{We}{A}$
19 nfa1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in \mathrm{On}\to {D}\ne \varnothing \right)$
20 18 19 nfan ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({w}\mathrm{We}{A}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in \mathrm{On}\to {D}\ne \varnothing \right)\right)$
21 nfv ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{y}\in {A}$
22 3 ssrab3 ${⊢}{D}\subseteq {A}$
23 1 2 3 zorn2lem1 ${⊢}\left({x}\in \mathrm{On}\wedge \left({w}\mathrm{We}{A}\wedge {D}\ne \varnothing \right)\right)\to {F}\left({x}\right)\in {D}$
24 22 23 sseldi ${⊢}\left({x}\in \mathrm{On}\wedge \left({w}\mathrm{We}{A}\wedge {D}\ne \varnothing \right)\right)\to {F}\left({x}\right)\in {A}$
25 eleq1 ${⊢}{F}\left({x}\right)={y}\to \left({F}\left({x}\right)\in {A}↔{y}\in {A}\right)$
26 24 25 syl5ibcom ${⊢}\left({x}\in \mathrm{On}\wedge \left({w}\mathrm{We}{A}\wedge {D}\ne \varnothing \right)\right)\to \left({F}\left({x}\right)={y}\to {y}\in {A}\right)$
27 26 exp32 ${⊢}{x}\in \mathrm{On}\to \left({w}\mathrm{We}{A}\to \left({D}\ne \varnothing \to \left({F}\left({x}\right)={y}\to {y}\in {A}\right)\right)\right)$
28 27 com12 ${⊢}{w}\mathrm{We}{A}\to \left({x}\in \mathrm{On}\to \left({D}\ne \varnothing \to \left({F}\left({x}\right)={y}\to {y}\in {A}\right)\right)\right)$
29 28 a2d ${⊢}{w}\mathrm{We}{A}\to \left(\left({x}\in \mathrm{On}\to {D}\ne \varnothing \right)\to \left({x}\in \mathrm{On}\to \left({F}\left({x}\right)={y}\to {y}\in {A}\right)\right)\right)$
30 29 spsd ${⊢}{w}\mathrm{We}{A}\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in \mathrm{On}\to {D}\ne \varnothing \right)\to \left({x}\in \mathrm{On}\to \left({F}\left({x}\right)={y}\to {y}\in {A}\right)\right)\right)$
31 30 imp ${⊢}\left({w}\mathrm{We}{A}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in \mathrm{On}\to {D}\ne \varnothing \right)\right)\to \left({x}\in \mathrm{On}\to \left({F}\left({x}\right)={y}\to {y}\in {A}\right)\right)$
32 20 21 31 rexlimd ${⊢}\left({w}\mathrm{We}{A}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in \mathrm{On}\to {D}\ne \varnothing \right)\right)\to \left(\exists {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)={y}\to {y}\in {A}\right)$
33 17 32 syl5bi ${⊢}\left({w}\mathrm{We}{A}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in \mathrm{On}\to {D}\ne \varnothing \right)\right)\to \left({y}\in \mathrm{ran}{F}\to {y}\in {A}\right)$
34 33 ssrdv ${⊢}\left({w}\mathrm{We}{A}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in \mathrm{On}\to {D}\ne \varnothing \right)\right)\to \mathrm{ran}{F}\subseteq {A}$
35 14 34 ssexd ${⊢}\left({w}\mathrm{We}{A}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in \mathrm{On}\to {D}\ne \varnothing \right)\right)\to \mathrm{ran}{F}\in \mathrm{V}$
36 35 ex ${⊢}{w}\mathrm{We}{A}\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in \mathrm{On}\to {D}\ne \varnothing \right)\to \mathrm{ran}{F}\in \mathrm{V}\right)$
37 36 adantl ${⊢}\left({R}\mathrm{Po}{A}\wedge {w}\mathrm{We}{A}\right)\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in \mathrm{On}\to {D}\ne \varnothing \right)\to \mathrm{ran}{F}\in \mathrm{V}\right)$
38 1 2 3 zorn2lem3 ${⊢}\left({R}\mathrm{Po}{A}\wedge \left({x}\in \mathrm{On}\wedge \left({w}\mathrm{We}{A}\wedge {D}\ne \varnothing \right)\right)\right)\to \left({y}\in {x}\to ¬{F}\left({x}\right)={F}\left({y}\right)\right)$
39 38 exp45 ${⊢}{R}\mathrm{Po}{A}\to \left({x}\in \mathrm{On}\to \left({w}\mathrm{We}{A}\to \left({D}\ne \varnothing \to \left({y}\in {x}\to ¬{F}\left({x}\right)={F}\left({y}\right)\right)\right)\right)\right)$
40 39 com23 ${⊢}{R}\mathrm{Po}{A}\to \left({w}\mathrm{We}{A}\to \left({x}\in \mathrm{On}\to \left({D}\ne \varnothing \to \left({y}\in {x}\to ¬{F}\left({x}\right)={F}\left({y}\right)\right)\right)\right)\right)$
41 40 imp ${⊢}\left({R}\mathrm{Po}{A}\wedge {w}\mathrm{We}{A}\right)\to \left({x}\in \mathrm{On}\to \left({D}\ne \varnothing \to \left({y}\in {x}\to ¬{F}\left({x}\right)={F}\left({y}\right)\right)\right)\right)$
42 41 a2d ${⊢}\left({R}\mathrm{Po}{A}\wedge {w}\mathrm{We}{A}\right)\to \left(\left({x}\in \mathrm{On}\to {D}\ne \varnothing \right)\to \left({x}\in \mathrm{On}\to \left({y}\in {x}\to ¬{F}\left({x}\right)={F}\left({y}\right)\right)\right)\right)$
43 42 imp4a ${⊢}\left({R}\mathrm{Po}{A}\wedge {w}\mathrm{We}{A}\right)\to \left(\left({x}\in \mathrm{On}\to {D}\ne \varnothing \right)\to \left(\left({x}\in \mathrm{On}\wedge {y}\in {x}\right)\to ¬{F}\left({x}\right)={F}\left({y}\right)\right)\right)$
44 43 alrimdv ${⊢}\left({R}\mathrm{Po}{A}\wedge {w}\mathrm{We}{A}\right)\to \left(\left({x}\in \mathrm{On}\to {D}\ne \varnothing \right)\to \forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in \mathrm{On}\wedge {y}\in {x}\right)\to ¬{F}\left({x}\right)={F}\left({y}\right)\right)\right)$
45 44 alimdv ${⊢}\left({R}\mathrm{Po}{A}\wedge {w}\mathrm{We}{A}\right)\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in \mathrm{On}\to {D}\ne \varnothing \right)\to \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in \mathrm{On}\wedge {y}\in {x}\right)\to ¬{F}\left({x}\right)={F}\left({y}\right)\right)\right)$
46 r2al ${⊢}\forall {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}¬{F}\left({x}\right)={F}\left({y}\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in \mathrm{On}\wedge {y}\in {x}\right)\to ¬{F}\left({x}\right)={F}\left({y}\right)\right)$
47 45 46 syl6ibr ${⊢}\left({R}\mathrm{Po}{A}\wedge {w}\mathrm{We}{A}\right)\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in \mathrm{On}\to {D}\ne \varnothing \right)\to \forall {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}¬{F}\left({x}\right)={F}\left({y}\right)\right)$
48 ssid ${⊢}\mathrm{On}\subseteq \mathrm{On}$
49 15 tz7.48lem ${⊢}\left(\mathrm{On}\subseteq \mathrm{On}\wedge \forall {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}¬{F}\left({x}\right)={F}\left({y}\right)\right)\to \mathrm{Fun}{\left({{F}↾}_{\mathrm{On}}\right)}^{-1}$
50 48 49 mpan ${⊢}\forall {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}¬{F}\left({x}\right)={F}\left({y}\right)\to \mathrm{Fun}{\left({{F}↾}_{\mathrm{On}}\right)}^{-1}$
51 fnrel ${⊢}{F}Fn\mathrm{On}\to \mathrm{Rel}{F}$
52 15 51 ax-mp ${⊢}\mathrm{Rel}{F}$
53 fndm ${⊢}{F}Fn\mathrm{On}\to \mathrm{dom}{F}=\mathrm{On}$
54 15 53 ax-mp ${⊢}\mathrm{dom}{F}=\mathrm{On}$
55 54 eqimssi ${⊢}\mathrm{dom}{F}\subseteq \mathrm{On}$
56 relssres ${⊢}\left(\mathrm{Rel}{F}\wedge \mathrm{dom}{F}\subseteq \mathrm{On}\right)\to {{F}↾}_{\mathrm{On}}={F}$
57 52 55 56 mp2an ${⊢}{{F}↾}_{\mathrm{On}}={F}$
58 57 cnveqi ${⊢}{\left({{F}↾}_{\mathrm{On}}\right)}^{-1}={{F}}^{-1}$
59 58 funeqi ${⊢}\mathrm{Fun}{\left({{F}↾}_{\mathrm{On}}\right)}^{-1}↔\mathrm{Fun}{{F}}^{-1}$
60 50 59 sylib ${⊢}\forall {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}¬{F}\left({x}\right)={F}\left({y}\right)\to \mathrm{Fun}{{F}}^{-1}$
61 47 60 syl6 ${⊢}\left({R}\mathrm{Po}{A}\wedge {w}\mathrm{We}{A}\right)\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in \mathrm{On}\to {D}\ne \varnothing \right)\to \mathrm{Fun}{{F}}^{-1}\right)$
62 onprc ${⊢}¬\mathrm{On}\in \mathrm{V}$
63 funrnex ${⊢}\mathrm{dom}{{F}}^{-1}\in \mathrm{V}\to \left(\mathrm{Fun}{{F}}^{-1}\to \mathrm{ran}{{F}}^{-1}\in \mathrm{V}\right)$
64 63 com12 ${⊢}\mathrm{Fun}{{F}}^{-1}\to \left(\mathrm{dom}{{F}}^{-1}\in \mathrm{V}\to \mathrm{ran}{{F}}^{-1}\in \mathrm{V}\right)$
65 df-rn ${⊢}\mathrm{ran}{F}=\mathrm{dom}{{F}}^{-1}$
66 65 eleq1i ${⊢}\mathrm{ran}{F}\in \mathrm{V}↔\mathrm{dom}{{F}}^{-1}\in \mathrm{V}$
67 dfdm4 ${⊢}\mathrm{dom}{F}=\mathrm{ran}{{F}}^{-1}$
68 54 67 eqtr3i ${⊢}\mathrm{On}=\mathrm{ran}{{F}}^{-1}$
69 68 eleq1i ${⊢}\mathrm{On}\in \mathrm{V}↔\mathrm{ran}{{F}}^{-1}\in \mathrm{V}$
70 64 66 69 3imtr4g ${⊢}\mathrm{Fun}{{F}}^{-1}\to \left(\mathrm{ran}{F}\in \mathrm{V}\to \mathrm{On}\in \mathrm{V}\right)$
71 62 70 mtoi ${⊢}\mathrm{Fun}{{F}}^{-1}\to ¬\mathrm{ran}{F}\in \mathrm{V}$
72 61 71 syl6 ${⊢}\left({R}\mathrm{Po}{A}\wedge {w}\mathrm{We}{A}\right)\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in \mathrm{On}\to {D}\ne \varnothing \right)\to ¬\mathrm{ran}{F}\in \mathrm{V}\right)$
73 37 72 jcad ${⊢}\left({R}\mathrm{Po}{A}\wedge {w}\mathrm{We}{A}\right)\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in \mathrm{On}\to {D}\ne \varnothing \right)\to \left(\mathrm{ran}{F}\in \mathrm{V}\wedge ¬\mathrm{ran}{F}\in \mathrm{V}\right)\right)$
74 9 73 syl5bir ${⊢}\left({R}\mathrm{Po}{A}\wedge {w}\mathrm{We}{A}\right)\to \left(¬\exists {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{D}=\varnothing \to \left(\mathrm{ran}{F}\in \mathrm{V}\wedge ¬\mathrm{ran}{F}\in \mathrm{V}\right)\right)$
75 4 74 mt3i ${⊢}\left({R}\mathrm{Po}{A}\wedge {w}\mathrm{We}{A}\right)\to \exists {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{D}=\varnothing$