# Metamath Proof Explorer

## Theorem zorn2lem7

Description: Lemma for zorn2 . (Contributed by NM, 6-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\}$
zorn2lem.7 ${⊢}{H}=\left\{{z}\in {A}|\forall {g}\in {F}\left[{y}\right]\phantom{\rule{.4em}{0ex}}{g}{R}{z}\right\}$
Assertion zorn2lem7 ${⊢}\left({A}\in \mathrm{dom}\mathrm{card}\wedge {R}\mathrm{Po}{A}\wedge \forall {s}\phantom{\rule{.4em}{0ex}}\left(\left({s}\subseteq {A}\wedge {R}\mathrm{Or}{s}\right)\to \exists {a}\in {A}\phantom{\rule{.4em}{0ex}}\forall {r}\in {s}\phantom{\rule{.4em}{0ex}}\left({r}{R}{a}\vee {r}={a}\right)\right)\right)\to \exists {a}\in {A}\phantom{\rule{.4em}{0ex}}\forall {b}\in {A}\phantom{\rule{.4em}{0ex}}¬{a}{R}{b}$

### 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 zorn2lem.7 ${⊢}{H}=\left\{{z}\in {A}|\forall {g}\in {F}\left[{y}\right]\phantom{\rule{.4em}{0ex}}{g}{R}{z}\right\}$
5 ween ${⊢}{A}\in \mathrm{dom}\mathrm{card}↔\exists {w}\phantom{\rule{.4em}{0ex}}{w}\mathrm{We}{A}$
6 1 2 3 zorn2lem4 ${⊢}\left({R}\mathrm{Po}{A}\wedge {w}\mathrm{We}{A}\right)\to \exists {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{D}=\varnothing$
7 imaeq2 ${⊢}{x}={y}\to {F}\left[{x}\right]={F}\left[{y}\right]$
8 7 raleqdv ${⊢}{x}={y}\to \left(\forall {g}\in {F}\left[{x}\right]\phantom{\rule{.4em}{0ex}}{g}{R}{z}↔\forall {g}\in {F}\left[{y}\right]\phantom{\rule{.4em}{0ex}}{g}{R}{z}\right)$
9 8 rabbidv ${⊢}{x}={y}\to \left\{{z}\in {A}|\forall {g}\in {F}\left[{x}\right]\phantom{\rule{.4em}{0ex}}{g}{R}{z}\right\}=\left\{{z}\in {A}|\forall {g}\in {F}\left[{y}\right]\phantom{\rule{.4em}{0ex}}{g}{R}{z}\right\}$
10 9 3 4 3eqtr4g ${⊢}{x}={y}\to {D}={H}$
11 10 eqeq1d ${⊢}{x}={y}\to \left({D}=\varnothing ↔{H}=\varnothing \right)$
12 11 onminex ${⊢}\exists {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{D}=\varnothing \to \exists {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\left({D}=\varnothing \wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}¬{H}=\varnothing \right)$
13 df-ne ${⊢}{H}\ne \varnothing ↔¬{H}=\varnothing$
14 13 ralbii ${⊢}\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{H}\ne \varnothing ↔\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}¬{H}=\varnothing$
15 14 anbi2i ${⊢}\left({D}=\varnothing \wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{H}\ne \varnothing \right)↔\left({D}=\varnothing \wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}¬{H}=\varnothing \right)$
16 15 rexbii ${⊢}\exists {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\left({D}=\varnothing \wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{H}\ne \varnothing \right)↔\exists {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\left({D}=\varnothing \wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}¬{H}=\varnothing \right)$
17 12 16 sylibr ${⊢}\exists {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{D}=\varnothing \to \exists {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\left({D}=\varnothing \wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{H}\ne \varnothing \right)$
18 1 2 3 4 zorn2lem5 ${⊢}\left(\left({w}\mathrm{We}{A}\wedge {x}\in \mathrm{On}\right)\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{H}\ne \varnothing \right)\to {F}\left[{x}\right]\subseteq {A}$
19 18 a1i ${⊢}{R}\mathrm{Po}{A}\to \left(\left(\left({w}\mathrm{We}{A}\wedge {x}\in \mathrm{On}\right)\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{H}\ne \varnothing \right)\to {F}\left[{x}\right]\subseteq {A}\right)$
20 1 2 3 4 zorn2lem6 ${⊢}{R}\mathrm{Po}{A}\to \left(\left(\left({w}\mathrm{We}{A}\wedge {x}\in \mathrm{On}\right)\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{H}\ne \varnothing \right)\to {R}\mathrm{Or}{F}\left[{x}\right]\right)$
21 19 20 jcad ${⊢}{R}\mathrm{Po}{A}\to \left(\left(\left({w}\mathrm{We}{A}\wedge {x}\in \mathrm{On}\right)\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{H}\ne \varnothing \right)\to \left({F}\left[{x}\right]\subseteq {A}\wedge {R}\mathrm{Or}{F}\left[{x}\right]\right)\right)$
22 1 tfr1 ${⊢}{F}Fn\mathrm{On}$
23 fnfun ${⊢}{F}Fn\mathrm{On}\to \mathrm{Fun}{F}$
24 vex ${⊢}{x}\in \mathrm{V}$
25 24 funimaex ${⊢}\mathrm{Fun}{F}\to {F}\left[{x}\right]\in \mathrm{V}$
26 22 23 25 mp2b ${⊢}{F}\left[{x}\right]\in \mathrm{V}$
27 sseq1 ${⊢}{s}={F}\left[{x}\right]\to \left({s}\subseteq {A}↔{F}\left[{x}\right]\subseteq {A}\right)$
28 soeq2 ${⊢}{s}={F}\left[{x}\right]\to \left({R}\mathrm{Or}{s}↔{R}\mathrm{Or}{F}\left[{x}\right]\right)$
29 27 28 anbi12d ${⊢}{s}={F}\left[{x}\right]\to \left(\left({s}\subseteq {A}\wedge {R}\mathrm{Or}{s}\right)↔\left({F}\left[{x}\right]\subseteq {A}\wedge {R}\mathrm{Or}{F}\left[{x}\right]\right)\right)$
30 raleq ${⊢}{s}={F}\left[{x}\right]\to \left(\forall {r}\in {s}\phantom{\rule{.4em}{0ex}}\left({r}{R}{a}\vee {r}={a}\right)↔\forall {r}\in {F}\left[{x}\right]\phantom{\rule{.4em}{0ex}}\left({r}{R}{a}\vee {r}={a}\right)\right)$
31 30 rexbidv ${⊢}{s}={F}\left[{x}\right]\to \left(\exists {a}\in {A}\phantom{\rule{.4em}{0ex}}\forall {r}\in {s}\phantom{\rule{.4em}{0ex}}\left({r}{R}{a}\vee {r}={a}\right)↔\exists {a}\in {A}\phantom{\rule{.4em}{0ex}}\forall {r}\in {F}\left[{x}\right]\phantom{\rule{.4em}{0ex}}\left({r}{R}{a}\vee {r}={a}\right)\right)$
32 29 31 imbi12d ${⊢}{s}={F}\left[{x}\right]\to \left(\left(\left({s}\subseteq {A}\wedge {R}\mathrm{Or}{s}\right)\to \exists {a}\in {A}\phantom{\rule{.4em}{0ex}}\forall {r}\in {s}\phantom{\rule{.4em}{0ex}}\left({r}{R}{a}\vee {r}={a}\right)\right)↔\left(\left({F}\left[{x}\right]\subseteq {A}\wedge {R}\mathrm{Or}{F}\left[{x}\right]\right)\to \exists {a}\in {A}\phantom{\rule{.4em}{0ex}}\forall {r}\in {F}\left[{x}\right]\phantom{\rule{.4em}{0ex}}\left({r}{R}{a}\vee {r}={a}\right)\right)\right)$
33 26 32 spcv ${⊢}\forall {s}\phantom{\rule{.4em}{0ex}}\left(\left({s}\subseteq {A}\wedge {R}\mathrm{Or}{s}\right)\to \exists {a}\in {A}\phantom{\rule{.4em}{0ex}}\forall {r}\in {s}\phantom{\rule{.4em}{0ex}}\left({r}{R}{a}\vee {r}={a}\right)\right)\to \left(\left({F}\left[{x}\right]\subseteq {A}\wedge {R}\mathrm{Or}{F}\left[{x}\right]\right)\to \exists {a}\in {A}\phantom{\rule{.4em}{0ex}}\forall {r}\in {F}\left[{x}\right]\phantom{\rule{.4em}{0ex}}\left({r}{R}{a}\vee {r}={a}\right)\right)$
34 21 33 sylan9 ${⊢}\left({R}\mathrm{Po}{A}\wedge \forall {s}\phantom{\rule{.4em}{0ex}}\left(\left({s}\subseteq {A}\wedge {R}\mathrm{Or}{s}\right)\to \exists {a}\in {A}\phantom{\rule{.4em}{0ex}}\forall {r}\in {s}\phantom{\rule{.4em}{0ex}}\left({r}{R}{a}\vee {r}={a}\right)\right)\right)\to \left(\left(\left({w}\mathrm{We}{A}\wedge {x}\in \mathrm{On}\right)\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{H}\ne \varnothing \right)\to \exists {a}\in {A}\phantom{\rule{.4em}{0ex}}\forall {r}\in {F}\left[{x}\right]\phantom{\rule{.4em}{0ex}}\left({r}{R}{a}\vee {r}={a}\right)\right)$
35 34 adantld ${⊢}\left({R}\mathrm{Po}{A}\wedge \forall {s}\phantom{\rule{.4em}{0ex}}\left(\left({s}\subseteq {A}\wedge {R}\mathrm{Or}{s}\right)\to \exists {a}\in {A}\phantom{\rule{.4em}{0ex}}\forall {r}\in {s}\phantom{\rule{.4em}{0ex}}\left({r}{R}{a}\vee {r}={a}\right)\right)\right)\to \left(\left({D}=\varnothing \wedge \left(\left({w}\mathrm{We}{A}\wedge {x}\in \mathrm{On}\right)\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{H}\ne \varnothing \right)\right)\to \exists {a}\in {A}\phantom{\rule{.4em}{0ex}}\forall {r}\in {F}\left[{x}\right]\phantom{\rule{.4em}{0ex}}\left({r}{R}{a}\vee {r}={a}\right)\right)$
36 35 imp ${⊢}\left(\left({R}\mathrm{Po}{A}\wedge \forall {s}\phantom{\rule{.4em}{0ex}}\left(\left({s}\subseteq {A}\wedge {R}\mathrm{Or}{s}\right)\to \exists {a}\in {A}\phantom{\rule{.4em}{0ex}}\forall {r}\in {s}\phantom{\rule{.4em}{0ex}}\left({r}{R}{a}\vee {r}={a}\right)\right)\right)\wedge \left({D}=\varnothing \wedge \left(\left({w}\mathrm{We}{A}\wedge {x}\in \mathrm{On}\right)\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{H}\ne \varnothing \right)\right)\right)\to \exists {a}\in {A}\phantom{\rule{.4em}{0ex}}\forall {r}\in {F}\left[{x}\right]\phantom{\rule{.4em}{0ex}}\left({r}{R}{a}\vee {r}={a}\right)$
37 noel ${⊢}¬{b}\in \varnothing$
38 18 sseld ${⊢}\left(\left({w}\mathrm{We}{A}\wedge {x}\in \mathrm{On}\right)\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{H}\ne \varnothing \right)\to \left({r}\in {F}\left[{x}\right]\to {r}\in {A}\right)$
39 3anass ${⊢}\left({r}\in {A}\wedge {a}\in {A}\wedge {b}\in {A}\right)↔\left({r}\in {A}\wedge \left({a}\in {A}\wedge {b}\in {A}\right)\right)$
40 potr ${⊢}\left({R}\mathrm{Po}{A}\wedge \left({r}\in {A}\wedge {a}\in {A}\wedge {b}\in {A}\right)\right)\to \left(\left({r}{R}{a}\wedge {a}{R}{b}\right)\to {r}{R}{b}\right)$
41 39 40 sylan2br ${⊢}\left({R}\mathrm{Po}{A}\wedge \left({r}\in {A}\wedge \left({a}\in {A}\wedge {b}\in {A}\right)\right)\right)\to \left(\left({r}{R}{a}\wedge {a}{R}{b}\right)\to {r}{R}{b}\right)$
42 41 expcomd ${⊢}\left({R}\mathrm{Po}{A}\wedge \left({r}\in {A}\wedge \left({a}\in {A}\wedge {b}\in {A}\right)\right)\right)\to \left({a}{R}{b}\to \left({r}{R}{a}\to {r}{R}{b}\right)\right)$
43 42 imp ${⊢}\left(\left({R}\mathrm{Po}{A}\wedge \left({r}\in {A}\wedge \left({a}\in {A}\wedge {b}\in {A}\right)\right)\right)\wedge {a}{R}{b}\right)\to \left({r}{R}{a}\to {r}{R}{b}\right)$
44 breq1 ${⊢}{r}={a}\to \left({r}{R}{b}↔{a}{R}{b}\right)$
45 44 biimprcd ${⊢}{a}{R}{b}\to \left({r}={a}\to {r}{R}{b}\right)$
46 45 adantl ${⊢}\left(\left({R}\mathrm{Po}{A}\wedge \left({r}\in {A}\wedge \left({a}\in {A}\wedge {b}\in {A}\right)\right)\right)\wedge {a}{R}{b}\right)\to \left({r}={a}\to {r}{R}{b}\right)$
47 43 46 jaod ${⊢}\left(\left({R}\mathrm{Po}{A}\wedge \left({r}\in {A}\wedge \left({a}\in {A}\wedge {b}\in {A}\right)\right)\right)\wedge {a}{R}{b}\right)\to \left(\left({r}{R}{a}\vee {r}={a}\right)\to {r}{R}{b}\right)$
48 47 exp42 ${⊢}{R}\mathrm{Po}{A}\to \left({r}\in {A}\to \left(\left({a}\in {A}\wedge {b}\in {A}\right)\to \left({a}{R}{b}\to \left(\left({r}{R}{a}\vee {r}={a}\right)\to {r}{R}{b}\right)\right)\right)\right)$
49 38 48 sylan9r ${⊢}\left({R}\mathrm{Po}{A}\wedge \left(\left({w}\mathrm{We}{A}\wedge {x}\in \mathrm{On}\right)\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{H}\ne \varnothing \right)\right)\to \left({r}\in {F}\left[{x}\right]\to \left(\left({a}\in {A}\wedge {b}\in {A}\right)\to \left({a}{R}{b}\to \left(\left({r}{R}{a}\vee {r}={a}\right)\to {r}{R}{b}\right)\right)\right)\right)$
50 49 com24 ${⊢}\left({R}\mathrm{Po}{A}\wedge \left(\left({w}\mathrm{We}{A}\wedge {x}\in \mathrm{On}\right)\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{H}\ne \varnothing \right)\right)\to \left({a}{R}{b}\to \left(\left({a}\in {A}\wedge {b}\in {A}\right)\to \left({r}\in {F}\left[{x}\right]\to \left(\left({r}{R}{a}\vee {r}={a}\right)\to {r}{R}{b}\right)\right)\right)\right)$
51 50 com23 ${⊢}\left({R}\mathrm{Po}{A}\wedge \left(\left({w}\mathrm{We}{A}\wedge {x}\in \mathrm{On}\right)\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{H}\ne \varnothing \right)\right)\to \left(\left({a}\in {A}\wedge {b}\in {A}\right)\to \left({a}{R}{b}\to \left({r}\in {F}\left[{x}\right]\to \left(\left({r}{R}{a}\vee {r}={a}\right)\to {r}{R}{b}\right)\right)\right)\right)$
52 51 imp31 ${⊢}\left(\left(\left({R}\mathrm{Po}{A}\wedge \left(\left({w}\mathrm{We}{A}\wedge {x}\in \mathrm{On}\right)\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{H}\ne \varnothing \right)\right)\wedge \left({a}\in {A}\wedge {b}\in {A}\right)\right)\wedge {a}{R}{b}\right)\to \left({r}\in {F}\left[{x}\right]\to \left(\left({r}{R}{a}\vee {r}={a}\right)\to {r}{R}{b}\right)\right)$
53 52 a2d ${⊢}\left(\left(\left({R}\mathrm{Po}{A}\wedge \left(\left({w}\mathrm{We}{A}\wedge {x}\in \mathrm{On}\right)\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{H}\ne \varnothing \right)\right)\wedge \left({a}\in {A}\wedge {b}\in {A}\right)\right)\wedge {a}{R}{b}\right)\to \left(\left({r}\in {F}\left[{x}\right]\to \left({r}{R}{a}\vee {r}={a}\right)\right)\to \left({r}\in {F}\left[{x}\right]\to {r}{R}{b}\right)\right)$
54 53 ralimdv2 ${⊢}\left(\left(\left({R}\mathrm{Po}{A}\wedge \left(\left({w}\mathrm{We}{A}\wedge {x}\in \mathrm{On}\right)\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{H}\ne \varnothing \right)\right)\wedge \left({a}\in {A}\wedge {b}\in {A}\right)\right)\wedge {a}{R}{b}\right)\to \left(\forall {r}\in {F}\left[{x}\right]\phantom{\rule{.4em}{0ex}}\left({r}{R}{a}\vee {r}={a}\right)\to \forall {r}\in {F}\left[{x}\right]\phantom{\rule{.4em}{0ex}}{r}{R}{b}\right)$
55 breq1 ${⊢}{r}={g}\to \left({r}{R}{b}↔{g}{R}{b}\right)$
56 55 cbvralvw ${⊢}\forall {r}\in {F}\left[{x}\right]\phantom{\rule{.4em}{0ex}}{r}{R}{b}↔\forall {g}\in {F}\left[{x}\right]\phantom{\rule{.4em}{0ex}}{g}{R}{b}$
57 breq2 ${⊢}{z}={b}\to \left({g}{R}{z}↔{g}{R}{b}\right)$
58 57 ralbidv ${⊢}{z}={b}\to \left(\forall {g}\in {F}\left[{x}\right]\phantom{\rule{.4em}{0ex}}{g}{R}{z}↔\forall {g}\in {F}\left[{x}\right]\phantom{\rule{.4em}{0ex}}{g}{R}{b}\right)$
59 58 elrab ${⊢}{b}\in \left\{{z}\in {A}|\forall {g}\in {F}\left[{x}\right]\phantom{\rule{.4em}{0ex}}{g}{R}{z}\right\}↔\left({b}\in {A}\wedge \forall {g}\in {F}\left[{x}\right]\phantom{\rule{.4em}{0ex}}{g}{R}{b}\right)$
60 3 eqeq1i ${⊢}{D}=\varnothing ↔\left\{{z}\in {A}|\forall {g}\in {F}\left[{x}\right]\phantom{\rule{.4em}{0ex}}{g}{R}{z}\right\}=\varnothing$
61 eleq2 ${⊢}\left\{{z}\in {A}|\forall {g}\in {F}\left[{x}\right]\phantom{\rule{.4em}{0ex}}{g}{R}{z}\right\}=\varnothing \to \left({b}\in \left\{{z}\in {A}|\forall {g}\in {F}\left[{x}\right]\phantom{\rule{.4em}{0ex}}{g}{R}{z}\right\}↔{b}\in \varnothing \right)$
62 60 61 sylbi ${⊢}{D}=\varnothing \to \left({b}\in \left\{{z}\in {A}|\forall {g}\in {F}\left[{x}\right]\phantom{\rule{.4em}{0ex}}{g}{R}{z}\right\}↔{b}\in \varnothing \right)$
63 59 62 syl5bbr ${⊢}{D}=\varnothing \to \left(\left({b}\in {A}\wedge \forall {g}\in {F}\left[{x}\right]\phantom{\rule{.4em}{0ex}}{g}{R}{b}\right)↔{b}\in \varnothing \right)$
64 63 biimpd ${⊢}{D}=\varnothing \to \left(\left({b}\in {A}\wedge \forall {g}\in {F}\left[{x}\right]\phantom{\rule{.4em}{0ex}}{g}{R}{b}\right)\to {b}\in \varnothing \right)$
65 64 expdimp ${⊢}\left({D}=\varnothing \wedge {b}\in {A}\right)\to \left(\forall {g}\in {F}\left[{x}\right]\phantom{\rule{.4em}{0ex}}{g}{R}{b}\to {b}\in \varnothing \right)$
66 56 65 syl5bi ${⊢}\left({D}=\varnothing \wedge {b}\in {A}\right)\to \left(\forall {r}\in {F}\left[{x}\right]\phantom{\rule{.4em}{0ex}}{r}{R}{b}\to {b}\in \varnothing \right)$
67 54 66 sylan9r ${⊢}\left(\left({D}=\varnothing \wedge {b}\in {A}\right)\wedge \left(\left(\left({R}\mathrm{Po}{A}\wedge \left(\left({w}\mathrm{We}{A}\wedge {x}\in \mathrm{On}\right)\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{H}\ne \varnothing \right)\right)\wedge \left({a}\in {A}\wedge {b}\in {A}\right)\right)\wedge {a}{R}{b}\right)\right)\to \left(\forall {r}\in {F}\left[{x}\right]\phantom{\rule{.4em}{0ex}}\left({r}{R}{a}\vee {r}={a}\right)\to {b}\in \varnothing \right)$
68 67 exp32 ${⊢}\left({D}=\varnothing \wedge {b}\in {A}\right)\to \left(\left(\left({R}\mathrm{Po}{A}\wedge \left(\left({w}\mathrm{We}{A}\wedge {x}\in \mathrm{On}\right)\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{H}\ne \varnothing \right)\right)\wedge \left({a}\in {A}\wedge {b}\in {A}\right)\right)\to \left({a}{R}{b}\to \left(\forall {r}\in {F}\left[{x}\right]\phantom{\rule{.4em}{0ex}}\left({r}{R}{a}\vee {r}={a}\right)\to {b}\in \varnothing \right)\right)\right)$
69 68 com34 ${⊢}\left({D}=\varnothing \wedge {b}\in {A}\right)\to \left(\left(\left({R}\mathrm{Po}{A}\wedge \left(\left({w}\mathrm{We}{A}\wedge {x}\in \mathrm{On}\right)\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{H}\ne \varnothing \right)\right)\wedge \left({a}\in {A}\wedge {b}\in {A}\right)\right)\to \left(\forall {r}\in {F}\left[{x}\right]\phantom{\rule{.4em}{0ex}}\left({r}{R}{a}\vee {r}={a}\right)\to \left({a}{R}{b}\to {b}\in \varnothing \right)\right)\right)$
70 69 imp31 ${⊢}\left(\left(\left({D}=\varnothing \wedge {b}\in {A}\right)\wedge \left(\left({R}\mathrm{Po}{A}\wedge \left(\left({w}\mathrm{We}{A}\wedge {x}\in \mathrm{On}\right)\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{H}\ne \varnothing \right)\right)\wedge \left({a}\in {A}\wedge {b}\in {A}\right)\right)\right)\wedge \forall {r}\in {F}\left[{x}\right]\phantom{\rule{.4em}{0ex}}\left({r}{R}{a}\vee {r}={a}\right)\right)\to \left({a}{R}{b}\to {b}\in \varnothing \right)$
71 37 70 mtoi ${⊢}\left(\left(\left({D}=\varnothing \wedge {b}\in {A}\right)\wedge \left(\left({R}\mathrm{Po}{A}\wedge \left(\left({w}\mathrm{We}{A}\wedge {x}\in \mathrm{On}\right)\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{H}\ne \varnothing \right)\right)\wedge \left({a}\in {A}\wedge {b}\in {A}\right)\right)\right)\wedge \forall {r}\in {F}\left[{x}\right]\phantom{\rule{.4em}{0ex}}\left({r}{R}{a}\vee {r}={a}\right)\right)\to ¬{a}{R}{b}$
72 71 exp42 ${⊢}\left({D}=\varnothing \wedge {b}\in {A}\right)\to \left(\left({R}\mathrm{Po}{A}\wedge \left(\left({w}\mathrm{We}{A}\wedge {x}\in \mathrm{On}\right)\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{H}\ne \varnothing \right)\right)\to \left(\left({a}\in {A}\wedge {b}\in {A}\right)\to \left(\forall {r}\in {F}\left[{x}\right]\phantom{\rule{.4em}{0ex}}\left({r}{R}{a}\vee {r}={a}\right)\to ¬{a}{R}{b}\right)\right)\right)$
73 72 exp4a ${⊢}\left({D}=\varnothing \wedge {b}\in {A}\right)\to \left(\left({R}\mathrm{Po}{A}\wedge \left(\left({w}\mathrm{We}{A}\wedge {x}\in \mathrm{On}\right)\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{H}\ne \varnothing \right)\right)\to \left({a}\in {A}\to \left({b}\in {A}\to \left(\forall {r}\in {F}\left[{x}\right]\phantom{\rule{.4em}{0ex}}\left({r}{R}{a}\vee {r}={a}\right)\to ¬{a}{R}{b}\right)\right)\right)\right)$
74 73 com34 ${⊢}\left({D}=\varnothing \wedge {b}\in {A}\right)\to \left(\left({R}\mathrm{Po}{A}\wedge \left(\left({w}\mathrm{We}{A}\wedge {x}\in \mathrm{On}\right)\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{H}\ne \varnothing \right)\right)\to \left({b}\in {A}\to \left({a}\in {A}\to \left(\forall {r}\in {F}\left[{x}\right]\phantom{\rule{.4em}{0ex}}\left({r}{R}{a}\vee {r}={a}\right)\to ¬{a}{R}{b}\right)\right)\right)\right)$
75 74 ex ${⊢}{D}=\varnothing \to \left({b}\in {A}\to \left(\left({R}\mathrm{Po}{A}\wedge \left(\left({w}\mathrm{We}{A}\wedge {x}\in \mathrm{On}\right)\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{H}\ne \varnothing \right)\right)\to \left({b}\in {A}\to \left({a}\in {A}\to \left(\forall {r}\in {F}\left[{x}\right]\phantom{\rule{.4em}{0ex}}\left({r}{R}{a}\vee {r}={a}\right)\to ¬{a}{R}{b}\right)\right)\right)\right)\right)$
76 75 com4r ${⊢}{b}\in {A}\to \left({D}=\varnothing \to \left({b}\in {A}\to \left(\left({R}\mathrm{Po}{A}\wedge \left(\left({w}\mathrm{We}{A}\wedge {x}\in \mathrm{On}\right)\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{H}\ne \varnothing \right)\right)\to \left({a}\in {A}\to \left(\forall {r}\in {F}\left[{x}\right]\phantom{\rule{.4em}{0ex}}\left({r}{R}{a}\vee {r}={a}\right)\to ¬{a}{R}{b}\right)\right)\right)\right)\right)$
77 76 pm2.43a ${⊢}{b}\in {A}\to \left({D}=\varnothing \to \left(\left({R}\mathrm{Po}{A}\wedge \left(\left({w}\mathrm{We}{A}\wedge {x}\in \mathrm{On}\right)\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{H}\ne \varnothing \right)\right)\to \left({a}\in {A}\to \left(\forall {r}\in {F}\left[{x}\right]\phantom{\rule{.4em}{0ex}}\left({r}{R}{a}\vee {r}={a}\right)\to ¬{a}{R}{b}\right)\right)\right)\right)$
78 77 impd ${⊢}{b}\in {A}\to \left(\left({D}=\varnothing \wedge \left({R}\mathrm{Po}{A}\wedge \left(\left({w}\mathrm{We}{A}\wedge {x}\in \mathrm{On}\right)\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{H}\ne \varnothing \right)\right)\right)\to \left({a}\in {A}\to \left(\forall {r}\in {F}\left[{x}\right]\phantom{\rule{.4em}{0ex}}\left({r}{R}{a}\vee {r}={a}\right)\to ¬{a}{R}{b}\right)\right)\right)$
79 78 com4l ${⊢}\left({D}=\varnothing \wedge \left({R}\mathrm{Po}{A}\wedge \left(\left({w}\mathrm{We}{A}\wedge {x}\in \mathrm{On}\right)\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{H}\ne \varnothing \right)\right)\right)\to \left({a}\in {A}\to \left(\forall {r}\in {F}\left[{x}\right]\phantom{\rule{.4em}{0ex}}\left({r}{R}{a}\vee {r}={a}\right)\to \left({b}\in {A}\to ¬{a}{R}{b}\right)\right)\right)$
80 79 impd ${⊢}\left({D}=\varnothing \wedge \left({R}\mathrm{Po}{A}\wedge \left(\left({w}\mathrm{We}{A}\wedge {x}\in \mathrm{On}\right)\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{H}\ne \varnothing \right)\right)\right)\to \left(\left({a}\in {A}\wedge \forall {r}\in {F}\left[{x}\right]\phantom{\rule{.4em}{0ex}}\left({r}{R}{a}\vee {r}={a}\right)\right)\to \left({b}\in {A}\to ¬{a}{R}{b}\right)\right)$
81 80 ralrimdv ${⊢}\left({D}=\varnothing \wedge \left({R}\mathrm{Po}{A}\wedge \left(\left({w}\mathrm{We}{A}\wedge {x}\in \mathrm{On}\right)\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{H}\ne \varnothing \right)\right)\right)\to \left(\left({a}\in {A}\wedge \forall {r}\in {F}\left[{x}\right]\phantom{\rule{.4em}{0ex}}\left({r}{R}{a}\vee {r}={a}\right)\right)\to \forall {b}\in {A}\phantom{\rule{.4em}{0ex}}¬{a}{R}{b}\right)$
82 81 expd ${⊢}\left({D}=\varnothing \wedge \left({R}\mathrm{Po}{A}\wedge \left(\left({w}\mathrm{We}{A}\wedge {x}\in \mathrm{On}\right)\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{H}\ne \varnothing \right)\right)\right)\to \left({a}\in {A}\to \left(\forall {r}\in {F}\left[{x}\right]\phantom{\rule{.4em}{0ex}}\left({r}{R}{a}\vee {r}={a}\right)\to \forall {b}\in {A}\phantom{\rule{.4em}{0ex}}¬{a}{R}{b}\right)\right)$
83 82 reximdvai ${⊢}\left({D}=\varnothing \wedge \left({R}\mathrm{Po}{A}\wedge \left(\left({w}\mathrm{We}{A}\wedge {x}\in \mathrm{On}\right)\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{H}\ne \varnothing \right)\right)\right)\to \left(\exists {a}\in {A}\phantom{\rule{.4em}{0ex}}\forall {r}\in {F}\left[{x}\right]\phantom{\rule{.4em}{0ex}}\left({r}{R}{a}\vee {r}={a}\right)\to \exists {a}\in {A}\phantom{\rule{.4em}{0ex}}\forall {b}\in {A}\phantom{\rule{.4em}{0ex}}¬{a}{R}{b}\right)$
84 83 exp32 ${⊢}{D}=\varnothing \to \left({R}\mathrm{Po}{A}\to \left(\left(\left({w}\mathrm{We}{A}\wedge {x}\in \mathrm{On}\right)\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{H}\ne \varnothing \right)\to \left(\exists {a}\in {A}\phantom{\rule{.4em}{0ex}}\forall {r}\in {F}\left[{x}\right]\phantom{\rule{.4em}{0ex}}\left({r}{R}{a}\vee {r}={a}\right)\to \exists {a}\in {A}\phantom{\rule{.4em}{0ex}}\forall {b}\in {A}\phantom{\rule{.4em}{0ex}}¬{a}{R}{b}\right)\right)\right)$
85 84 com12 ${⊢}{R}\mathrm{Po}{A}\to \left({D}=\varnothing \to \left(\left(\left({w}\mathrm{We}{A}\wedge {x}\in \mathrm{On}\right)\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{H}\ne \varnothing \right)\to \left(\exists {a}\in {A}\phantom{\rule{.4em}{0ex}}\forall {r}\in {F}\left[{x}\right]\phantom{\rule{.4em}{0ex}}\left({r}{R}{a}\vee {r}={a}\right)\to \exists {a}\in {A}\phantom{\rule{.4em}{0ex}}\forall {b}\in {A}\phantom{\rule{.4em}{0ex}}¬{a}{R}{b}\right)\right)\right)$
86 85 adantr ${⊢}\left({R}\mathrm{Po}{A}\wedge \forall {s}\phantom{\rule{.4em}{0ex}}\left(\left({s}\subseteq {A}\wedge {R}\mathrm{Or}{s}\right)\to \exists {a}\in {A}\phantom{\rule{.4em}{0ex}}\forall {r}\in {s}\phantom{\rule{.4em}{0ex}}\left({r}{R}{a}\vee {r}={a}\right)\right)\right)\to \left({D}=\varnothing \to \left(\left(\left({w}\mathrm{We}{A}\wedge {x}\in \mathrm{On}\right)\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{H}\ne \varnothing \right)\to \left(\exists {a}\in {A}\phantom{\rule{.4em}{0ex}}\forall {r}\in {F}\left[{x}\right]\phantom{\rule{.4em}{0ex}}\left({r}{R}{a}\vee {r}={a}\right)\to \exists {a}\in {A}\phantom{\rule{.4em}{0ex}}\forall {b}\in {A}\phantom{\rule{.4em}{0ex}}¬{a}{R}{b}\right)\right)\right)$
87 86 imp32 ${⊢}\left(\left({R}\mathrm{Po}{A}\wedge \forall {s}\phantom{\rule{.4em}{0ex}}\left(\left({s}\subseteq {A}\wedge {R}\mathrm{Or}{s}\right)\to \exists {a}\in {A}\phantom{\rule{.4em}{0ex}}\forall {r}\in {s}\phantom{\rule{.4em}{0ex}}\left({r}{R}{a}\vee {r}={a}\right)\right)\right)\wedge \left({D}=\varnothing \wedge \left(\left({w}\mathrm{We}{A}\wedge {x}\in \mathrm{On}\right)\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{H}\ne \varnothing \right)\right)\right)\to \left(\exists {a}\in {A}\phantom{\rule{.4em}{0ex}}\forall {r}\in {F}\left[{x}\right]\phantom{\rule{.4em}{0ex}}\left({r}{R}{a}\vee {r}={a}\right)\to \exists {a}\in {A}\phantom{\rule{.4em}{0ex}}\forall {b}\in {A}\phantom{\rule{.4em}{0ex}}¬{a}{R}{b}\right)$
88 36 87 mpd ${⊢}\left(\left({R}\mathrm{Po}{A}\wedge \forall {s}\phantom{\rule{.4em}{0ex}}\left(\left({s}\subseteq {A}\wedge {R}\mathrm{Or}{s}\right)\to \exists {a}\in {A}\phantom{\rule{.4em}{0ex}}\forall {r}\in {s}\phantom{\rule{.4em}{0ex}}\left({r}{R}{a}\vee {r}={a}\right)\right)\right)\wedge \left({D}=\varnothing \wedge \left(\left({w}\mathrm{We}{A}\wedge {x}\in \mathrm{On}\right)\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{H}\ne \varnothing \right)\right)\right)\to \exists {a}\in {A}\phantom{\rule{.4em}{0ex}}\forall {b}\in {A}\phantom{\rule{.4em}{0ex}}¬{a}{R}{b}$
89 88 exp45 ${⊢}\left({R}\mathrm{Po}{A}\wedge \forall {s}\phantom{\rule{.4em}{0ex}}\left(\left({s}\subseteq {A}\wedge {R}\mathrm{Or}{s}\right)\to \exists {a}\in {A}\phantom{\rule{.4em}{0ex}}\forall {r}\in {s}\phantom{\rule{.4em}{0ex}}\left({r}{R}{a}\vee {r}={a}\right)\right)\right)\to \left({D}=\varnothing \to \left(\left({w}\mathrm{We}{A}\wedge {x}\in \mathrm{On}\right)\to \left(\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{H}\ne \varnothing \to \exists {a}\in {A}\phantom{\rule{.4em}{0ex}}\forall {b}\in {A}\phantom{\rule{.4em}{0ex}}¬{a}{R}{b}\right)\right)\right)$
90 89 com23 ${⊢}\left({R}\mathrm{Po}{A}\wedge \forall {s}\phantom{\rule{.4em}{0ex}}\left(\left({s}\subseteq {A}\wedge {R}\mathrm{Or}{s}\right)\to \exists {a}\in {A}\phantom{\rule{.4em}{0ex}}\forall {r}\in {s}\phantom{\rule{.4em}{0ex}}\left({r}{R}{a}\vee {r}={a}\right)\right)\right)\to \left(\left({w}\mathrm{We}{A}\wedge {x}\in \mathrm{On}\right)\to \left({D}=\varnothing \to \left(\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{H}\ne \varnothing \to \exists {a}\in {A}\phantom{\rule{.4em}{0ex}}\forall {b}\in {A}\phantom{\rule{.4em}{0ex}}¬{a}{R}{b}\right)\right)\right)$
91 90 expdimp ${⊢}\left(\left({R}\mathrm{Po}{A}\wedge \forall {s}\phantom{\rule{.4em}{0ex}}\left(\left({s}\subseteq {A}\wedge {R}\mathrm{Or}{s}\right)\to \exists {a}\in {A}\phantom{\rule{.4em}{0ex}}\forall {r}\in {s}\phantom{\rule{.4em}{0ex}}\left({r}{R}{a}\vee {r}={a}\right)\right)\right)\wedge {w}\mathrm{We}{A}\right)\to \left({x}\in \mathrm{On}\to \left({D}=\varnothing \to \left(\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{H}\ne \varnothing \to \exists {a}\in {A}\phantom{\rule{.4em}{0ex}}\forall {b}\in {A}\phantom{\rule{.4em}{0ex}}¬{a}{R}{b}\right)\right)\right)$
92 91 imp4a ${⊢}\left(\left({R}\mathrm{Po}{A}\wedge \forall {s}\phantom{\rule{.4em}{0ex}}\left(\left({s}\subseteq {A}\wedge {R}\mathrm{Or}{s}\right)\to \exists {a}\in {A}\phantom{\rule{.4em}{0ex}}\forall {r}\in {s}\phantom{\rule{.4em}{0ex}}\left({r}{R}{a}\vee {r}={a}\right)\right)\right)\wedge {w}\mathrm{We}{A}\right)\to \left({x}\in \mathrm{On}\to \left(\left({D}=\varnothing \wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{H}\ne \varnothing \right)\to \exists {a}\in {A}\phantom{\rule{.4em}{0ex}}\forall {b}\in {A}\phantom{\rule{.4em}{0ex}}¬{a}{R}{b}\right)\right)$
93 92 com3l ${⊢}{x}\in \mathrm{On}\to \left(\left({D}=\varnothing \wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{H}\ne \varnothing \right)\to \left(\left(\left({R}\mathrm{Po}{A}\wedge \forall {s}\phantom{\rule{.4em}{0ex}}\left(\left({s}\subseteq {A}\wedge {R}\mathrm{Or}{s}\right)\to \exists {a}\in {A}\phantom{\rule{.4em}{0ex}}\forall {r}\in {s}\phantom{\rule{.4em}{0ex}}\left({r}{R}{a}\vee {r}={a}\right)\right)\right)\wedge {w}\mathrm{We}{A}\right)\to \exists {a}\in {A}\phantom{\rule{.4em}{0ex}}\forall {b}\in {A}\phantom{\rule{.4em}{0ex}}¬{a}{R}{b}\right)\right)$
94 93 rexlimiv ${⊢}\exists {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\left({D}=\varnothing \wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{H}\ne \varnothing \right)\to \left(\left(\left({R}\mathrm{Po}{A}\wedge \forall {s}\phantom{\rule{.4em}{0ex}}\left(\left({s}\subseteq {A}\wedge {R}\mathrm{Or}{s}\right)\to \exists {a}\in {A}\phantom{\rule{.4em}{0ex}}\forall {r}\in {s}\phantom{\rule{.4em}{0ex}}\left({r}{R}{a}\vee {r}={a}\right)\right)\right)\wedge {w}\mathrm{We}{A}\right)\to \exists {a}\in {A}\phantom{\rule{.4em}{0ex}}\forall {b}\in {A}\phantom{\rule{.4em}{0ex}}¬{a}{R}{b}\right)$
95 6 17 94 3syl ${⊢}\left({R}\mathrm{Po}{A}\wedge {w}\mathrm{We}{A}\right)\to \left(\left(\left({R}\mathrm{Po}{A}\wedge \forall {s}\phantom{\rule{.4em}{0ex}}\left(\left({s}\subseteq {A}\wedge {R}\mathrm{Or}{s}\right)\to \exists {a}\in {A}\phantom{\rule{.4em}{0ex}}\forall {r}\in {s}\phantom{\rule{.4em}{0ex}}\left({r}{R}{a}\vee {r}={a}\right)\right)\right)\wedge {w}\mathrm{We}{A}\right)\to \exists {a}\in {A}\phantom{\rule{.4em}{0ex}}\forall {b}\in {A}\phantom{\rule{.4em}{0ex}}¬{a}{R}{b}\right)$
96 95 adantlr ${⊢}\left(\left({R}\mathrm{Po}{A}\wedge \forall {s}\phantom{\rule{.4em}{0ex}}\left(\left({s}\subseteq {A}\wedge {R}\mathrm{Or}{s}\right)\to \exists {a}\in {A}\phantom{\rule{.4em}{0ex}}\forall {r}\in {s}\phantom{\rule{.4em}{0ex}}\left({r}{R}{a}\vee {r}={a}\right)\right)\right)\wedge {w}\mathrm{We}{A}\right)\to \left(\left(\left({R}\mathrm{Po}{A}\wedge \forall {s}\phantom{\rule{.4em}{0ex}}\left(\left({s}\subseteq {A}\wedge {R}\mathrm{Or}{s}\right)\to \exists {a}\in {A}\phantom{\rule{.4em}{0ex}}\forall {r}\in {s}\phantom{\rule{.4em}{0ex}}\left({r}{R}{a}\vee {r}={a}\right)\right)\right)\wedge {w}\mathrm{We}{A}\right)\to \exists {a}\in {A}\phantom{\rule{.4em}{0ex}}\forall {b}\in {A}\phantom{\rule{.4em}{0ex}}¬{a}{R}{b}\right)$
97 96 pm2.43i ${⊢}\left(\left({R}\mathrm{Po}{A}\wedge \forall {s}\phantom{\rule{.4em}{0ex}}\left(\left({s}\subseteq {A}\wedge {R}\mathrm{Or}{s}\right)\to \exists {a}\in {A}\phantom{\rule{.4em}{0ex}}\forall {r}\in {s}\phantom{\rule{.4em}{0ex}}\left({r}{R}{a}\vee {r}={a}\right)\right)\right)\wedge {w}\mathrm{We}{A}\right)\to \exists {a}\in {A}\phantom{\rule{.4em}{0ex}}\forall {b}\in {A}\phantom{\rule{.4em}{0ex}}¬{a}{R}{b}$
98 97 expcom ${⊢}{w}\mathrm{We}{A}\to \left(\left({R}\mathrm{Po}{A}\wedge \forall {s}\phantom{\rule{.4em}{0ex}}\left(\left({s}\subseteq {A}\wedge {R}\mathrm{Or}{s}\right)\to \exists {a}\in {A}\phantom{\rule{.4em}{0ex}}\forall {r}\in {s}\phantom{\rule{.4em}{0ex}}\left({r}{R}{a}\vee {r}={a}\right)\right)\right)\to \exists {a}\in {A}\phantom{\rule{.4em}{0ex}}\forall {b}\in {A}\phantom{\rule{.4em}{0ex}}¬{a}{R}{b}\right)$
99 98 exlimiv ${⊢}\exists {w}\phantom{\rule{.4em}{0ex}}{w}\mathrm{We}{A}\to \left(\left({R}\mathrm{Po}{A}\wedge \forall {s}\phantom{\rule{.4em}{0ex}}\left(\left({s}\subseteq {A}\wedge {R}\mathrm{Or}{s}\right)\to \exists {a}\in {A}\phantom{\rule{.4em}{0ex}}\forall {r}\in {s}\phantom{\rule{.4em}{0ex}}\left({r}{R}{a}\vee {r}={a}\right)\right)\right)\to \exists {a}\in {A}\phantom{\rule{.4em}{0ex}}\forall {b}\in {A}\phantom{\rule{.4em}{0ex}}¬{a}{R}{b}\right)$
100 5 99 sylbi ${⊢}{A}\in \mathrm{dom}\mathrm{card}\to \left(\left({R}\mathrm{Po}{A}\wedge \forall {s}\phantom{\rule{.4em}{0ex}}\left(\left({s}\subseteq {A}\wedge {R}\mathrm{Or}{s}\right)\to \exists {a}\in {A}\phantom{\rule{.4em}{0ex}}\forall {r}\in {s}\phantom{\rule{.4em}{0ex}}\left({r}{R}{a}\vee {r}={a}\right)\right)\right)\to \exists {a}\in {A}\phantom{\rule{.4em}{0ex}}\forall {b}\in {A}\phantom{\rule{.4em}{0ex}}¬{a}{R}{b}\right)$
101 100 3impib ${⊢}\left({A}\in \mathrm{dom}\mathrm{card}\wedge {R}\mathrm{Po}{A}\wedge \forall {s}\phantom{\rule{.4em}{0ex}}\left(\left({s}\subseteq {A}\wedge {R}\mathrm{Or}{s}\right)\to \exists {a}\in {A}\phantom{\rule{.4em}{0ex}}\forall {r}\in {s}\phantom{\rule{.4em}{0ex}}\left({r}{R}{a}\vee {r}={a}\right)\right)\right)\to \exists {a}\in {A}\phantom{\rule{.4em}{0ex}}\forall {b}\in {A}\phantom{\rule{.4em}{0ex}}¬{a}{R}{b}$