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 ⊢ 𝐹 = recs ( ( 𝑓 ∈ V ↦ ( ℩ 𝑣 ∈ 𝐶 ∀ 𝑢 ∈ 𝐶 ¬ 𝑢 𝑤 𝑣 ) ) )
zorn2lem.4 ⊢ 𝐶 = { 𝑧 ∈ 𝐴 ∣ ∀ 𝑔 ∈ ran 𝑓 𝑔 𝑅 𝑧 }
zorn2lem.5 ⊢ 𝐷 = { 𝑧 ∈ 𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹 “ 𝑥 ) 𝑔 𝑅 𝑧 }
zorn2lem.7 ⊢ 𝐻 = { 𝑧 ∈ 𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹 “ 𝑦 ) 𝑔 𝑅 𝑧 }
Assertion zorn2lem7 ( ( 𝐴 ∈ dom card ∧ 𝑅 Po 𝐴 ∧ ∀ 𝑠 ( ( 𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠 ) → ∃ 𝑎 ∈ 𝐴 ∀ 𝑟 ∈ 𝑠 ( 𝑟 𝑅 𝑎 ∨ 𝑟 = 𝑎 ) ) ) → ∃ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ¬ 𝑎 𝑅 𝑏 )

Proof

Step Hyp Ref Expression
1 zorn2lem.3 ⊢ 𝐹 = recs ( ( 𝑓 ∈ V ↦ ( ℩ 𝑣 ∈ 𝐶 ∀ 𝑢 ∈ 𝐶 ¬ 𝑢 𝑤 𝑣 ) ) )
2 zorn2lem.4 ⊢ 𝐶 = { 𝑧 ∈ 𝐴 ∣ ∀ 𝑔 ∈ ran 𝑓 𝑔 𝑅 𝑧 }
3 zorn2lem.5 ⊢ 𝐷 = { 𝑧 ∈ 𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹 “ 𝑥 ) 𝑔 𝑅 𝑧 }
4 zorn2lem.7 ⊢ 𝐻 = { 𝑧 ∈ 𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹 “ 𝑦 ) 𝑔 𝑅 𝑧 }
5 ween ⊢ ( 𝐴 ∈ dom card ↔ ∃ 𝑤 𝑤 We 𝐴 )
6 1 2 3 zorn2lem4 ⊢ ( ( 𝑅 Po 𝐴 ∧ 𝑤 We 𝐴 ) → ∃ 𝑥 ∈ On 𝐷 = ∅ )
7 imaeq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐹 “ 𝑥 ) = ( 𝐹 “ 𝑦 ) )
8 7 raleqdv ⊢ ( 𝑥 = 𝑦 → ( ∀ 𝑔 ∈ ( 𝐹 “ 𝑥 ) 𝑔 𝑅 𝑧 ↔ ∀ 𝑔 ∈ ( 𝐹 “ 𝑦 ) 𝑔 𝑅 𝑧 ) )
9 8 rabbidv ⊢ ( 𝑥 = 𝑦 → { 𝑧 ∈ 𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹 “ 𝑥 ) 𝑔 𝑅 𝑧 } = { 𝑧 ∈ 𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹 “ 𝑦 ) 𝑔 𝑅 𝑧 } )
10 9 3 4 3eqtr4g ⊢ ( 𝑥 = 𝑦 → 𝐷 = 𝐻 )
11 10 eqeq1d ⊢ ( 𝑥 = 𝑦 → ( 𝐷 = ∅ ↔ 𝐻 = ∅ ) )
12 11 onminex ⊢ ( ∃ 𝑥 ∈ On 𝐷 = ∅ → ∃ 𝑥 ∈ On ( 𝐷 = ∅ ∧ ∀ 𝑦 ∈ 𝑥 ¬ 𝐻 = ∅ ) )
13 df-ne ⊢ ( 𝐻 ≠ ∅ ↔ ¬ 𝐻 = ∅ )
14 13 ralbii ⊢ ( ∀ 𝑦 ∈ 𝑥 𝐻 ≠ ∅ ↔ ∀ 𝑦 ∈ 𝑥 ¬ 𝐻 = ∅ )
15 14 anbi2i ⊢ ( ( 𝐷 = ∅ ∧ ∀ 𝑦 ∈ 𝑥 𝐻 ≠ ∅ ) ↔ ( 𝐷 = ∅ ∧ ∀ 𝑦 ∈ 𝑥 ¬ 𝐻 = ∅ ) )
16 15 rexbii ⊢ ( ∃ 𝑥 ∈ On ( 𝐷 = ∅ ∧ ∀ 𝑦 ∈ 𝑥 𝐻 ≠ ∅ ) ↔ ∃ 𝑥 ∈ On ( 𝐷 = ∅ ∧ ∀ 𝑦 ∈ 𝑥 ¬ 𝐻 = ∅ ) )
17 12 16 sylibr ⊢ ( ∃ 𝑥 ∈ On 𝐷 = ∅ → ∃ 𝑥 ∈ On ( 𝐷 = ∅ ∧ ∀ 𝑦 ∈ 𝑥 𝐻 ≠ ∅ ) )
18 1 2 3 4 zorn2lem5 ⊢ ( ( ( 𝑤 We 𝐴 ∧ 𝑥 ∈ On ) ∧ ∀ 𝑦 ∈ 𝑥 𝐻 ≠ ∅ ) → ( 𝐹 “ 𝑥 ) ⊆ 𝐴 )
19 18 a1i ⊢ ( 𝑅 Po 𝐴 → ( ( ( 𝑤 We 𝐴 ∧ 𝑥 ∈ On ) ∧ ∀ 𝑦 ∈ 𝑥 𝐻 ≠ ∅ ) → ( 𝐹 “ 𝑥 ) ⊆ 𝐴 ) )
20 1 2 3 4 zorn2lem6 ⊢ ( 𝑅 Po 𝐴 → ( ( ( 𝑤 We 𝐴 ∧ 𝑥 ∈ On ) ∧ ∀ 𝑦 ∈ 𝑥 𝐻 ≠ ∅ ) → 𝑅 Or ( 𝐹 “ 𝑥 ) ) )
21 19 20 jcad ⊢ ( 𝑅 Po 𝐴 → ( ( ( 𝑤 We 𝐴 ∧ 𝑥 ∈ On ) ∧ ∀ 𝑦 ∈ 𝑥 𝐻 ≠ ∅ ) → ( ( 𝐹 “ 𝑥 ) ⊆ 𝐴 ∧ 𝑅 Or ( 𝐹 “ 𝑥 ) ) ) )
22 1 tfr1 ⊢ 𝐹 Fn On
23 fnfun ⊢ ( 𝐹 Fn On → Fun 𝐹 )
24 vex ⊢ 𝑥 ∈ V
25 24 funimaex ⊢ ( Fun 𝐹 → ( 𝐹 “ 𝑥 ) ∈ V )
26 22 23 25 mp2b ⊢ ( 𝐹 “ 𝑥 ) ∈ V
27 sseq1 ⊢ ( 𝑠 = ( 𝐹 “ 𝑥 ) → ( 𝑠 ⊆ 𝐴 ↔ ( 𝐹 “ 𝑥 ) ⊆ 𝐴 ) )
28 soeq2 ⊢ ( 𝑠 = ( 𝐹 “ 𝑥 ) → ( 𝑅 Or 𝑠 ↔ 𝑅 Or ( 𝐹 “ 𝑥 ) ) )
29 27 28 anbi12d ⊢ ( 𝑠 = ( 𝐹 “ 𝑥 ) → ( ( 𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠 ) ↔ ( ( 𝐹 “ 𝑥 ) ⊆ 𝐴 ∧ 𝑅 Or ( 𝐹 “ 𝑥 ) ) ) )
30 raleq ⊢ ( 𝑠 = ( 𝐹 “ 𝑥 ) → ( ∀ 𝑟 ∈ 𝑠 ( 𝑟 𝑅 𝑎 ∨ 𝑟 = 𝑎 ) ↔ ∀ 𝑟 ∈ ( 𝐹 “ 𝑥 ) ( 𝑟 𝑅 𝑎 ∨ 𝑟 = 𝑎 ) ) )
31 30 rexbidv ⊢ ( 𝑠 = ( 𝐹 “ 𝑥 ) → ( ∃ 𝑎 ∈ 𝐴 ∀ 𝑟 ∈ 𝑠 ( 𝑟 𝑅 𝑎 ∨ 𝑟 = 𝑎 ) ↔ ∃ 𝑎 ∈ 𝐴 ∀ 𝑟 ∈ ( 𝐹 “ 𝑥 ) ( 𝑟 𝑅 𝑎 ∨ 𝑟 = 𝑎 ) ) )
32 29 31 imbi12d ⊢ ( 𝑠 = ( 𝐹 “ 𝑥 ) → ( ( ( 𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠 ) → ∃ 𝑎 ∈ 𝐴 ∀ 𝑟 ∈ 𝑠 ( 𝑟 𝑅 𝑎 ∨ 𝑟 = 𝑎 ) ) ↔ ( ( ( 𝐹 “ 𝑥 ) ⊆ 𝐴 ∧ 𝑅 Or ( 𝐹 “ 𝑥 ) ) → ∃ 𝑎 ∈ 𝐴 ∀ 𝑟 ∈ ( 𝐹 “ 𝑥 ) ( 𝑟 𝑅 𝑎 ∨ 𝑟 = 𝑎 ) ) ) )
33 26 32 spcv ⊢ ( ∀ 𝑠 ( ( 𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠 ) → ∃ 𝑎 ∈ 𝐴 ∀ 𝑟 ∈ 𝑠 ( 𝑟 𝑅 𝑎 ∨ 𝑟 = 𝑎 ) ) → ( ( ( 𝐹 “ 𝑥 ) ⊆ 𝐴 ∧ 𝑅 Or ( 𝐹 “ 𝑥 ) ) → ∃ 𝑎 ∈ 𝐴 ∀ 𝑟 ∈ ( 𝐹 “ 𝑥 ) ( 𝑟 𝑅 𝑎 ∨ 𝑟 = 𝑎 ) ) )
34 21 33 sylan9 ⊢ ( ( 𝑅 Po 𝐴 ∧ ∀ 𝑠 ( ( 𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠 ) → ∃ 𝑎 ∈ 𝐴 ∀ 𝑟 ∈ 𝑠 ( 𝑟 𝑅 𝑎 ∨ 𝑟 = 𝑎 ) ) ) → ( ( ( 𝑤 We 𝐴 ∧ 𝑥 ∈ On ) ∧ ∀ 𝑦 ∈ 𝑥 𝐻 ≠ ∅ ) → ∃ 𝑎 ∈ 𝐴 ∀ 𝑟 ∈ ( 𝐹 “ 𝑥 ) ( 𝑟 𝑅 𝑎 ∨ 𝑟 = 𝑎 ) ) )
35 34 adantld ⊢ ( ( 𝑅 Po 𝐴 ∧ ∀ 𝑠 ( ( 𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠 ) → ∃ 𝑎 ∈ 𝐴 ∀ 𝑟 ∈ 𝑠 ( 𝑟 𝑅 𝑎 ∨ 𝑟 = 𝑎 ) ) ) → ( ( 𝐷 = ∅ ∧ ( ( 𝑤 We 𝐴 ∧ 𝑥 ∈ On ) ∧ ∀ 𝑦 ∈ 𝑥 𝐻 ≠ ∅ ) ) → ∃ 𝑎 ∈ 𝐴 ∀ 𝑟 ∈ ( 𝐹 “ 𝑥 ) ( 𝑟 𝑅 𝑎 ∨ 𝑟 = 𝑎 ) ) )
36 35 imp ⊢ ( ( ( 𝑅 Po 𝐴 ∧ ∀ 𝑠 ( ( 𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠 ) → ∃ 𝑎 ∈ 𝐴 ∀ 𝑟 ∈ 𝑠 ( 𝑟 𝑅 𝑎 ∨ 𝑟 = 𝑎 ) ) ) ∧ ( 𝐷 = ∅ ∧ ( ( 𝑤 We 𝐴 ∧ 𝑥 ∈ On ) ∧ ∀ 𝑦 ∈ 𝑥 𝐻 ≠ ∅ ) ) ) → ∃ 𝑎 ∈ 𝐴 ∀ 𝑟 ∈ ( 𝐹 “ 𝑥 ) ( 𝑟 𝑅 𝑎 ∨ 𝑟 = 𝑎 ) )
37 noel ⊢ ¬ 𝑏 ∈ ∅
38 18 sseld ⊢ ( ( ( 𝑤 We 𝐴 ∧ 𝑥 ∈ On ) ∧ ∀ 𝑦 ∈ 𝑥 𝐻 ≠ ∅ ) → ( 𝑟 ∈ ( 𝐹 “ 𝑥 ) → 𝑟 ∈ 𝐴 ) )
39 3anass ⊢ ( ( 𝑟 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ↔ ( 𝑟 ∈ 𝐴 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) )
40 potr ⊢ ( ( 𝑅 Po 𝐴 ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) → ( ( 𝑟 𝑅 𝑎 ∧ 𝑎 𝑅 𝑏 ) → 𝑟 𝑅 𝑏 ) )
41 39 40 sylan2br ⊢ ( ( 𝑅 Po 𝐴 ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) ) → ( ( 𝑟 𝑅 𝑎 ∧ 𝑎 𝑅 𝑏 ) → 𝑟 𝑅 𝑏 ) )
42 41 expcomd ⊢ ( ( 𝑅 Po 𝐴 ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) ) → ( 𝑎 𝑅 𝑏 → ( 𝑟 𝑅 𝑎 → 𝑟 𝑅 𝑏 ) ) )
43 42 imp ⊢ ( ( ( 𝑅 Po 𝐴 ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) ) ∧ 𝑎 𝑅 𝑏 ) → ( 𝑟 𝑅 𝑎 → 𝑟 𝑅 𝑏 ) )
44 breq1 ⊢ ( 𝑟 = 𝑎 → ( 𝑟 𝑅 𝑏 ↔ 𝑎 𝑅 𝑏 ) )
45 44 biimprcd ⊢ ( 𝑎 𝑅 𝑏 → ( 𝑟 = 𝑎 → 𝑟 𝑅 𝑏 ) )
46 45 adantl ⊢ ( ( ( 𝑅 Po 𝐴 ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) ) ∧ 𝑎 𝑅 𝑏 ) → ( 𝑟 = 𝑎 → 𝑟 𝑅 𝑏 ) )
47 43 46 jaod ⊢ ( ( ( 𝑅 Po 𝐴 ∧ ( 𝑟 ∈ 𝐴 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) ) ∧ 𝑎 𝑅 𝑏 ) → ( ( 𝑟 𝑅 𝑎 ∨ 𝑟 = 𝑎 ) → 𝑟 𝑅 𝑏 ) )
48 47 exp42 ⊢ ( 𝑅 Po 𝐴 → ( 𝑟 ∈ 𝐴 → ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) → ( 𝑎 𝑅 𝑏 → ( ( 𝑟 𝑅 𝑎 ∨ 𝑟 = 𝑎 ) → 𝑟 𝑅 𝑏 ) ) ) ) )
49 38 48 sylan9r ⊢ ( ( 𝑅 Po 𝐴 ∧ ( ( 𝑤 We 𝐴 ∧ 𝑥 ∈ On ) ∧ ∀ 𝑦 ∈ 𝑥 𝐻 ≠ ∅ ) ) → ( 𝑟 ∈ ( 𝐹 “ 𝑥 ) → ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) → ( 𝑎 𝑅 𝑏 → ( ( 𝑟 𝑅 𝑎 ∨ 𝑟 = 𝑎 ) → 𝑟 𝑅 𝑏 ) ) ) ) )
50 49 com24 ⊢ ( ( 𝑅 Po 𝐴 ∧ ( ( 𝑤 We 𝐴 ∧ 𝑥 ∈ On ) ∧ ∀ 𝑦 ∈ 𝑥 𝐻 ≠ ∅ ) ) → ( 𝑎 𝑅 𝑏 → ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) → ( 𝑟 ∈ ( 𝐹 “ 𝑥 ) → ( ( 𝑟 𝑅 𝑎 ∨ 𝑟 = 𝑎 ) → 𝑟 𝑅 𝑏 ) ) ) ) )
51 50 com23 ⊢ ( ( 𝑅 Po 𝐴 ∧ ( ( 𝑤 We 𝐴 ∧ 𝑥 ∈ On ) ∧ ∀ 𝑦 ∈ 𝑥 𝐻 ≠ ∅ ) ) → ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) → ( 𝑎 𝑅 𝑏 → ( 𝑟 ∈ ( 𝐹 “ 𝑥 ) → ( ( 𝑟 𝑅 𝑎 ∨ 𝑟 = 𝑎 ) → 𝑟 𝑅 𝑏 ) ) ) ) )
52 51 imp31 ⊢ ( ( ( ( 𝑅 Po 𝐴 ∧ ( ( 𝑤 We 𝐴 ∧ 𝑥 ∈ On ) ∧ ∀ 𝑦 ∈ 𝑥 𝐻 ≠ ∅ ) ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) ∧ 𝑎 𝑅 𝑏 ) → ( 𝑟 ∈ ( 𝐹 “ 𝑥 ) → ( ( 𝑟 𝑅 𝑎 ∨ 𝑟 = 𝑎 ) → 𝑟 𝑅 𝑏 ) ) )
53 52 a2d ⊢ ( ( ( ( 𝑅 Po 𝐴 ∧ ( ( 𝑤 We 𝐴 ∧ 𝑥 ∈ On ) ∧ ∀ 𝑦 ∈ 𝑥 𝐻 ≠ ∅ ) ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) ∧ 𝑎 𝑅 𝑏 ) → ( ( 𝑟 ∈ ( 𝐹 “ 𝑥 ) → ( 𝑟 𝑅 𝑎 ∨ 𝑟 = 𝑎 ) ) → ( 𝑟 ∈ ( 𝐹 “ 𝑥 ) → 𝑟 𝑅 𝑏 ) ) )
54 53 ralimdv2 ⊢ ( ( ( ( 𝑅 Po 𝐴 ∧ ( ( 𝑤 We 𝐴 ∧ 𝑥 ∈ On ) ∧ ∀ 𝑦 ∈ 𝑥 𝐻 ≠ ∅ ) ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) ∧ 𝑎 𝑅 𝑏 ) → ( ∀ 𝑟 ∈ ( 𝐹 “ 𝑥 ) ( 𝑟 𝑅 𝑎 ∨ 𝑟 = 𝑎 ) → ∀ 𝑟 ∈ ( 𝐹 “ 𝑥 ) 𝑟 𝑅 𝑏 ) )
55 breq1 ⊢ ( 𝑟 = 𝑔 → ( 𝑟 𝑅 𝑏 ↔ 𝑔 𝑅 𝑏 ) )
56 55 cbvralvw ⊢ ( ∀ 𝑟 ∈ ( 𝐹 “ 𝑥 ) 𝑟 𝑅 𝑏 ↔ ∀ 𝑔 ∈ ( 𝐹 “ 𝑥 ) 𝑔 𝑅 𝑏 )
57 breq2 ⊢ ( 𝑧 = 𝑏 → ( 𝑔 𝑅 𝑧 ↔ 𝑔 𝑅 𝑏 ) )
58 57 ralbidv ⊢ ( 𝑧 = 𝑏 → ( ∀ 𝑔 ∈ ( 𝐹 “ 𝑥 ) 𝑔 𝑅 𝑧 ↔ ∀ 𝑔 ∈ ( 𝐹 “ 𝑥 ) 𝑔 𝑅 𝑏 ) )
59 58 elrab ⊢ ( 𝑏 ∈ { 𝑧 ∈ 𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹 “ 𝑥 ) 𝑔 𝑅 𝑧 } ↔ ( 𝑏 ∈ 𝐴 ∧ ∀ 𝑔 ∈ ( 𝐹 “ 𝑥 ) 𝑔 𝑅 𝑏 ) )
60 3 eqeq1i ⊢ ( 𝐷 = ∅ ↔ { 𝑧 ∈ 𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹 “ 𝑥 ) 𝑔 𝑅 𝑧 } = ∅ )
61 eleq2 ⊢ ( { 𝑧 ∈ 𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹 “ 𝑥 ) 𝑔 𝑅 𝑧 } = ∅ → ( 𝑏 ∈ { 𝑧 ∈ 𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹 “ 𝑥 ) 𝑔 𝑅 𝑧 } ↔ 𝑏 ∈ ∅ ) )
62 60 61 sylbi ⊢ ( 𝐷 = ∅ → ( 𝑏 ∈ { 𝑧 ∈ 𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹 “ 𝑥 ) 𝑔 𝑅 𝑧 } ↔ 𝑏 ∈ ∅ ) )
63 59 62 bitr3id ⊢ ( 𝐷 = ∅ → ( ( 𝑏 ∈ 𝐴 ∧ ∀ 𝑔 ∈ ( 𝐹 “ 𝑥 ) 𝑔 𝑅 𝑏 ) ↔ 𝑏 ∈ ∅ ) )
64 63 biimpd ⊢ ( 𝐷 = ∅ → ( ( 𝑏 ∈ 𝐴 ∧ ∀ 𝑔 ∈ ( 𝐹 “ 𝑥 ) 𝑔 𝑅 𝑏 ) → 𝑏 ∈ ∅ ) )
65 64 expdimp ⊢ ( ( 𝐷 = ∅ ∧ 𝑏 ∈ 𝐴 ) → ( ∀ 𝑔 ∈ ( 𝐹 “ 𝑥 ) 𝑔 𝑅 𝑏 → 𝑏 ∈ ∅ ) )
66 56 65 biimtrid ⊢ ( ( 𝐷 = ∅ ∧ 𝑏 ∈ 𝐴 ) → ( ∀ 𝑟 ∈ ( 𝐹 “ 𝑥 ) 𝑟 𝑅 𝑏 → 𝑏 ∈ ∅ ) )
67 54 66 sylan9r ⊢ ( ( ( 𝐷 = ∅ ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( ( 𝑅 Po 𝐴 ∧ ( ( 𝑤 We 𝐴 ∧ 𝑥 ∈ On ) ∧ ∀ 𝑦 ∈ 𝑥 𝐻 ≠ ∅ ) ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) ∧ 𝑎 𝑅 𝑏 ) ) → ( ∀ 𝑟 ∈ ( 𝐹 “ 𝑥 ) ( 𝑟 𝑅 𝑎 ∨ 𝑟 = 𝑎 ) → 𝑏 ∈ ∅ ) )
68 67 exp32 ⊢ ( ( 𝐷 = ∅ ∧ 𝑏 ∈ 𝐴 ) → ( ( ( 𝑅 Po 𝐴 ∧ ( ( 𝑤 We 𝐴 ∧ 𝑥 ∈ On ) ∧ ∀ 𝑦 ∈ 𝑥 𝐻 ≠ ∅ ) ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) → ( 𝑎 𝑅 𝑏 → ( ∀ 𝑟 ∈ ( 𝐹 “ 𝑥 ) ( 𝑟 𝑅 𝑎 ∨ 𝑟 = 𝑎 ) → 𝑏 ∈ ∅ ) ) ) )
69 68 com34 ⊢ ( ( 𝐷 = ∅ ∧ 𝑏 ∈ 𝐴 ) → ( ( ( 𝑅 Po 𝐴 ∧ ( ( 𝑤 We 𝐴 ∧ 𝑥 ∈ On ) ∧ ∀ 𝑦 ∈ 𝑥 𝐻 ≠ ∅ ) ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) → ( ∀ 𝑟 ∈ ( 𝐹 “ 𝑥 ) ( 𝑟 𝑅 𝑎 ∨ 𝑟 = 𝑎 ) → ( 𝑎 𝑅 𝑏 → 𝑏 ∈ ∅ ) ) ) )
70 69 imp31 ⊢ ( ( ( ( 𝐷 = ∅ ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( 𝑅 Po 𝐴 ∧ ( ( 𝑤 We 𝐴 ∧ 𝑥 ∈ On ) ∧ ∀ 𝑦 ∈ 𝑥 𝐻 ≠ ∅ ) ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) ) ∧ ∀ 𝑟 ∈ ( 𝐹 “ 𝑥 ) ( 𝑟 𝑅 𝑎 ∨ 𝑟 = 𝑎 ) ) → ( 𝑎 𝑅 𝑏 → 𝑏 ∈ ∅ ) )
71 37 70 mtoi ⊢ ( ( ( ( 𝐷 = ∅ ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( 𝑅 Po 𝐴 ∧ ( ( 𝑤 We 𝐴 ∧ 𝑥 ∈ On ) ∧ ∀ 𝑦 ∈ 𝑥 𝐻 ≠ ∅ ) ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) ) ∧ ∀ 𝑟 ∈ ( 𝐹 “ 𝑥 ) ( 𝑟 𝑅 𝑎 ∨ 𝑟 = 𝑎 ) ) → ¬ 𝑎 𝑅 𝑏 )
72 71 exp42 ⊢ ( ( 𝐷 = ∅ ∧ 𝑏 ∈ 𝐴 ) → ( ( 𝑅 Po 𝐴 ∧ ( ( 𝑤 We 𝐴 ∧ 𝑥 ∈ On ) ∧ ∀ 𝑦 ∈ 𝑥 𝐻 ≠ ∅ ) ) → ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) → ( ∀ 𝑟 ∈ ( 𝐹 “ 𝑥 ) ( 𝑟 𝑅 𝑎 ∨ 𝑟 = 𝑎 ) → ¬ 𝑎 𝑅 𝑏 ) ) ) )
73 72 exp4a ⊢ ( ( 𝐷 = ∅ ∧ 𝑏 ∈ 𝐴 ) → ( ( 𝑅 Po 𝐴 ∧ ( ( 𝑤 We 𝐴 ∧ 𝑥 ∈ On ) ∧ ∀ 𝑦 ∈ 𝑥 𝐻 ≠ ∅ ) ) → ( 𝑎 ∈ 𝐴 → ( 𝑏 ∈ 𝐴 → ( ∀ 𝑟 ∈ ( 𝐹 “ 𝑥 ) ( 𝑟 𝑅 𝑎 ∨ 𝑟 = 𝑎 ) → ¬ 𝑎 𝑅 𝑏 ) ) ) ) )
74 73 com34 ⊢ ( ( 𝐷 = ∅ ∧ 𝑏 ∈ 𝐴 ) → ( ( 𝑅 Po 𝐴 ∧ ( ( 𝑤 We 𝐴 ∧ 𝑥 ∈ On ) ∧ ∀ 𝑦 ∈ 𝑥 𝐻 ≠ ∅ ) ) → ( 𝑏 ∈ 𝐴 → ( 𝑎 ∈ 𝐴 → ( ∀ 𝑟 ∈ ( 𝐹 “ 𝑥 ) ( 𝑟 𝑅 𝑎 ∨ 𝑟 = 𝑎 ) → ¬ 𝑎 𝑅 𝑏 ) ) ) ) )
75 74 ex ⊢ ( 𝐷 = ∅ → ( 𝑏 ∈ 𝐴 → ( ( 𝑅 Po 𝐴 ∧ ( ( 𝑤 We 𝐴 ∧ 𝑥 ∈ On ) ∧ ∀ 𝑦 ∈ 𝑥 𝐻 ≠ ∅ ) ) → ( 𝑏 ∈ 𝐴 → ( 𝑎 ∈ 𝐴 → ( ∀ 𝑟 ∈ ( 𝐹 “ 𝑥 ) ( 𝑟 𝑅 𝑎 ∨ 𝑟 = 𝑎 ) → ¬ 𝑎 𝑅 𝑏 ) ) ) ) ) )
76 75 com4r ⊢ ( 𝑏 ∈ 𝐴 → ( 𝐷 = ∅ → ( 𝑏 ∈ 𝐴 → ( ( 𝑅 Po 𝐴 ∧ ( ( 𝑤 We 𝐴 ∧ 𝑥 ∈ On ) ∧ ∀ 𝑦 ∈ 𝑥 𝐻 ≠ ∅ ) ) → ( 𝑎 ∈ 𝐴 → ( ∀ 𝑟 ∈ ( 𝐹 “ 𝑥 ) ( 𝑟 𝑅 𝑎 ∨ 𝑟 = 𝑎 ) → ¬ 𝑎 𝑅 𝑏 ) ) ) ) ) )
77 76 pm2.43a ⊢ ( 𝑏 ∈ 𝐴 → ( 𝐷 = ∅ → ( ( 𝑅 Po 𝐴 ∧ ( ( 𝑤 We 𝐴 ∧ 𝑥 ∈ On ) ∧ ∀ 𝑦 ∈ 𝑥 𝐻 ≠ ∅ ) ) → ( 𝑎 ∈ 𝐴 → ( ∀ 𝑟 ∈ ( 𝐹 “ 𝑥 ) ( 𝑟 𝑅 𝑎 ∨ 𝑟 = 𝑎 ) → ¬ 𝑎 𝑅 𝑏 ) ) ) ) )
78 77 impd ⊢ ( 𝑏 ∈ 𝐴 → ( ( 𝐷 = ∅ ∧ ( 𝑅 Po 𝐴 ∧ ( ( 𝑤 We 𝐴 ∧ 𝑥 ∈ On ) ∧ ∀ 𝑦 ∈ 𝑥 𝐻 ≠ ∅ ) ) ) → ( 𝑎 ∈ 𝐴 → ( ∀ 𝑟 ∈ ( 𝐹 “ 𝑥 ) ( 𝑟 𝑅 𝑎 ∨ 𝑟 = 𝑎 ) → ¬ 𝑎 𝑅 𝑏 ) ) ) )
79 78 com4l ⊢ ( ( 𝐷 = ∅ ∧ ( 𝑅 Po 𝐴 ∧ ( ( 𝑤 We 𝐴 ∧ 𝑥 ∈ On ) ∧ ∀ 𝑦 ∈ 𝑥 𝐻 ≠ ∅ ) ) ) → ( 𝑎 ∈ 𝐴 → ( ∀ 𝑟 ∈ ( 𝐹 “ 𝑥 ) ( 𝑟 𝑅 𝑎 ∨ 𝑟 = 𝑎 ) → ( 𝑏 ∈ 𝐴 → ¬ 𝑎 𝑅 𝑏 ) ) ) )
80 79 impd ⊢ ( ( 𝐷 = ∅ ∧ ( 𝑅 Po 𝐴 ∧ ( ( 𝑤 We 𝐴 ∧ 𝑥 ∈ On ) ∧ ∀ 𝑦 ∈ 𝑥 𝐻 ≠ ∅ ) ) ) → ( ( 𝑎 ∈ 𝐴 ∧ ∀ 𝑟 ∈ ( 𝐹 “ 𝑥 ) ( 𝑟 𝑅 𝑎 ∨ 𝑟 = 𝑎 ) ) → ( 𝑏 ∈ 𝐴 → ¬ 𝑎 𝑅 𝑏 ) ) )
81 80 ralrimdv ⊢ ( ( 𝐷 = ∅ ∧ ( 𝑅 Po 𝐴 ∧ ( ( 𝑤 We 𝐴 ∧ 𝑥 ∈ On ) ∧ ∀ 𝑦 ∈ 𝑥 𝐻 ≠ ∅ ) ) ) → ( ( 𝑎 ∈ 𝐴 ∧ ∀ 𝑟 ∈ ( 𝐹 “ 𝑥 ) ( 𝑟 𝑅 𝑎 ∨ 𝑟 = 𝑎 ) ) → ∀ 𝑏 ∈ 𝐴 ¬ 𝑎 𝑅 𝑏 ) )
82 81 expd ⊢ ( ( 𝐷 = ∅ ∧ ( 𝑅 Po 𝐴 ∧ ( ( 𝑤 We 𝐴 ∧ 𝑥 ∈ On ) ∧ ∀ 𝑦 ∈ 𝑥 𝐻 ≠ ∅ ) ) ) → ( 𝑎 ∈ 𝐴 → ( ∀ 𝑟 ∈ ( 𝐹 “ 𝑥 ) ( 𝑟 𝑅 𝑎 ∨ 𝑟 = 𝑎 ) → ∀ 𝑏 ∈ 𝐴 ¬ 𝑎 𝑅 𝑏 ) ) )
83 82 reximdvai ⊢ ( ( 𝐷 = ∅ ∧ ( 𝑅 Po 𝐴 ∧ ( ( 𝑤 We 𝐴 ∧ 𝑥 ∈ On ) ∧ ∀ 𝑦 ∈ 𝑥 𝐻 ≠ ∅ ) ) ) → ( ∃ 𝑎 ∈ 𝐴 ∀ 𝑟 ∈ ( 𝐹 “ 𝑥 ) ( 𝑟 𝑅 𝑎 ∨ 𝑟 = 𝑎 ) → ∃ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ¬ 𝑎 𝑅 𝑏 ) )
84 83 exp32 ⊢ ( 𝐷 = ∅ → ( 𝑅 Po 𝐴 → ( ( ( 𝑤 We 𝐴 ∧ 𝑥 ∈ On ) ∧ ∀ 𝑦 ∈ 𝑥 𝐻 ≠ ∅ ) → ( ∃ 𝑎 ∈ 𝐴 ∀ 𝑟 ∈ ( 𝐹 “ 𝑥 ) ( 𝑟 𝑅 𝑎 ∨ 𝑟 = 𝑎 ) → ∃ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ¬ 𝑎 𝑅 𝑏 ) ) ) )
85 84 com12 ⊢ ( 𝑅 Po 𝐴 → ( 𝐷 = ∅ → ( ( ( 𝑤 We 𝐴 ∧ 𝑥 ∈ On ) ∧ ∀ 𝑦 ∈ 𝑥 𝐻 ≠ ∅ ) → ( ∃ 𝑎 ∈ 𝐴 ∀ 𝑟 ∈ ( 𝐹 “ 𝑥 ) ( 𝑟 𝑅 𝑎 ∨ 𝑟 = 𝑎 ) → ∃ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ¬ 𝑎 𝑅 𝑏 ) ) ) )
86 85 adantr ⊢ ( ( 𝑅 Po 𝐴 ∧ ∀ 𝑠 ( ( 𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠 ) → ∃ 𝑎 ∈ 𝐴 ∀ 𝑟 ∈ 𝑠 ( 𝑟 𝑅 𝑎 ∨ 𝑟 = 𝑎 ) ) ) → ( 𝐷 = ∅ → ( ( ( 𝑤 We 𝐴 ∧ 𝑥 ∈ On ) ∧ ∀ 𝑦 ∈ 𝑥 𝐻 ≠ ∅ ) → ( ∃ 𝑎 ∈ 𝐴 ∀ 𝑟 ∈ ( 𝐹 “ 𝑥 ) ( 𝑟 𝑅 𝑎 ∨ 𝑟 = 𝑎 ) → ∃ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ¬ 𝑎 𝑅 𝑏 ) ) ) )
87 86 imp32 ⊢ ( ( ( 𝑅 Po 𝐴 ∧ ∀ 𝑠 ( ( 𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠 ) → ∃ 𝑎 ∈ 𝐴 ∀ 𝑟 ∈ 𝑠 ( 𝑟 𝑅 𝑎 ∨ 𝑟 = 𝑎 ) ) ) ∧ ( 𝐷 = ∅ ∧ ( ( 𝑤 We 𝐴 ∧ 𝑥 ∈ On ) ∧ ∀ 𝑦 ∈ 𝑥 𝐻 ≠ ∅ ) ) ) → ( ∃ 𝑎 ∈ 𝐴 ∀ 𝑟 ∈ ( 𝐹 “ 𝑥 ) ( 𝑟 𝑅 𝑎 ∨ 𝑟 = 𝑎 ) → ∃ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ¬ 𝑎 𝑅 𝑏 ) )
88 36 87 mpd ⊢ ( ( ( 𝑅 Po 𝐴 ∧ ∀ 𝑠 ( ( 𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠 ) → ∃ 𝑎 ∈ 𝐴 ∀ 𝑟 ∈ 𝑠 ( 𝑟 𝑅 𝑎 ∨ 𝑟 = 𝑎 ) ) ) ∧ ( 𝐷 = ∅ ∧ ( ( 𝑤 We 𝐴 ∧ 𝑥 ∈ On ) ∧ ∀ 𝑦 ∈ 𝑥 𝐻 ≠ ∅ ) ) ) → ∃ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ¬ 𝑎 𝑅 𝑏 )
89 88 exp45 ⊢ ( ( 𝑅 Po 𝐴 ∧ ∀ 𝑠 ( ( 𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠 ) → ∃ 𝑎 ∈ 𝐴 ∀ 𝑟 ∈ 𝑠 ( 𝑟 𝑅 𝑎 ∨ 𝑟 = 𝑎 ) ) ) → ( 𝐷 = ∅ → ( ( 𝑤 We 𝐴 ∧ 𝑥 ∈ On ) → ( ∀ 𝑦 ∈ 𝑥 𝐻 ≠ ∅ → ∃ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ¬ 𝑎 𝑅 𝑏 ) ) ) )
90 89 com23 ⊢ ( ( 𝑅 Po 𝐴 ∧ ∀ 𝑠 ( ( 𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠 ) → ∃ 𝑎 ∈ 𝐴 ∀ 𝑟 ∈ 𝑠 ( 𝑟 𝑅 𝑎 ∨ 𝑟 = 𝑎 ) ) ) → ( ( 𝑤 We 𝐴 ∧ 𝑥 ∈ On ) → ( 𝐷 = ∅ → ( ∀ 𝑦 ∈ 𝑥 𝐻 ≠ ∅ → ∃ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ¬ 𝑎 𝑅 𝑏 ) ) ) )
91 90 expdimp ⊢ ( ( ( 𝑅 Po 𝐴 ∧ ∀ 𝑠 ( ( 𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠 ) → ∃ 𝑎 ∈ 𝐴 ∀ 𝑟 ∈ 𝑠 ( 𝑟 𝑅 𝑎 ∨ 𝑟 = 𝑎 ) ) ) ∧ 𝑤 We 𝐴 ) → ( 𝑥 ∈ On → ( 𝐷 = ∅ → ( ∀ 𝑦 ∈ 𝑥 𝐻 ≠ ∅ → ∃ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ¬ 𝑎 𝑅 𝑏 ) ) ) )
92 91 imp4a ⊢ ( ( ( 𝑅 Po 𝐴 ∧ ∀ 𝑠 ( ( 𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠 ) → ∃ 𝑎 ∈ 𝐴 ∀ 𝑟 ∈ 𝑠 ( 𝑟 𝑅 𝑎 ∨ 𝑟 = 𝑎 ) ) ) ∧ 𝑤 We 𝐴 ) → ( 𝑥 ∈ On → ( ( 𝐷 = ∅ ∧ ∀ 𝑦 ∈ 𝑥 𝐻 ≠ ∅ ) → ∃ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ¬ 𝑎 𝑅 𝑏 ) ) )
93 92 com3l ⊢ ( 𝑥 ∈ On → ( ( 𝐷 = ∅ ∧ ∀ 𝑦 ∈ 𝑥 𝐻 ≠ ∅ ) → ( ( ( 𝑅 Po 𝐴 ∧ ∀ 𝑠 ( ( 𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠 ) → ∃ 𝑎 ∈ 𝐴 ∀ 𝑟 ∈ 𝑠 ( 𝑟 𝑅 𝑎 ∨ 𝑟 = 𝑎 ) ) ) ∧ 𝑤 We 𝐴 ) → ∃ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ¬ 𝑎 𝑅 𝑏 ) ) )
94 93 rexlimiv ⊢ ( ∃ 𝑥 ∈ On ( 𝐷 = ∅ ∧ ∀ 𝑦 ∈ 𝑥 𝐻 ≠ ∅ ) → ( ( ( 𝑅 Po 𝐴 ∧ ∀ 𝑠 ( ( 𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠 ) → ∃ 𝑎 ∈ 𝐴 ∀ 𝑟 ∈ 𝑠 ( 𝑟 𝑅 𝑎 ∨ 𝑟 = 𝑎 ) ) ) ∧ 𝑤 We 𝐴 ) → ∃ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ¬ 𝑎 𝑅 𝑏 ) )
95 6 17 94 3syl ⊢ ( ( 𝑅 Po 𝐴 ∧ 𝑤 We 𝐴 ) → ( ( ( 𝑅 Po 𝐴 ∧ ∀ 𝑠 ( ( 𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠 ) → ∃ 𝑎 ∈ 𝐴 ∀ 𝑟 ∈ 𝑠 ( 𝑟 𝑅 𝑎 ∨ 𝑟 = 𝑎 ) ) ) ∧ 𝑤 We 𝐴 ) → ∃ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ¬ 𝑎 𝑅 𝑏 ) )
96 95 adantlr ⊢ ( ( ( 𝑅 Po 𝐴 ∧ ∀ 𝑠 ( ( 𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠 ) → ∃ 𝑎 ∈ 𝐴 ∀ 𝑟 ∈ 𝑠 ( 𝑟 𝑅 𝑎 ∨ 𝑟 = 𝑎 ) ) ) ∧ 𝑤 We 𝐴 ) → ( ( ( 𝑅 Po 𝐴 ∧ ∀ 𝑠 ( ( 𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠 ) → ∃ 𝑎 ∈ 𝐴 ∀ 𝑟 ∈ 𝑠 ( 𝑟 𝑅 𝑎 ∨ 𝑟 = 𝑎 ) ) ) ∧ 𝑤 We 𝐴 ) → ∃ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ¬ 𝑎 𝑅 𝑏 ) )
97 96 pm2.43i ⊢ ( ( ( 𝑅 Po 𝐴 ∧ ∀ 𝑠 ( ( 𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠 ) → ∃ 𝑎 ∈ 𝐴 ∀ 𝑟 ∈ 𝑠 ( 𝑟 𝑅 𝑎 ∨ 𝑟 = 𝑎 ) ) ) ∧ 𝑤 We 𝐴 ) → ∃ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ¬ 𝑎 𝑅 𝑏 )
98 97 expcom ⊢ ( 𝑤 We 𝐴 → ( ( 𝑅 Po 𝐴 ∧ ∀ 𝑠 ( ( 𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠 ) → ∃ 𝑎 ∈ 𝐴 ∀ 𝑟 ∈ 𝑠 ( 𝑟 𝑅 𝑎 ∨ 𝑟 = 𝑎 ) ) ) → ∃ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ¬ 𝑎 𝑅 𝑏 ) )
99 98 exlimiv ⊢ ( ∃ 𝑤 𝑤 We 𝐴 → ( ( 𝑅 Po 𝐴 ∧ ∀ 𝑠 ( ( 𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠 ) → ∃ 𝑎 ∈ 𝐴 ∀ 𝑟 ∈ 𝑠 ( 𝑟 𝑅 𝑎 ∨ 𝑟 = 𝑎 ) ) ) → ∃ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ¬ 𝑎 𝑅 𝑏 ) )
100 5 99 sylbi ⊢ ( 𝐴 ∈ dom card → ( ( 𝑅 Po 𝐴 ∧ ∀ 𝑠 ( ( 𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠 ) → ∃ 𝑎 ∈ 𝐴 ∀ 𝑟 ∈ 𝑠 ( 𝑟 𝑅 𝑎 ∨ 𝑟 = 𝑎 ) ) ) → ∃ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ¬ 𝑎 𝑅 𝑏 ) )
101 100 3impib ⊢ ( ( 𝐴 ∈ dom card ∧ 𝑅 Po 𝐴 ∧ ∀ 𝑠 ( ( 𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠 ) → ∃ 𝑎 ∈ 𝐴 ∀ 𝑟 ∈ 𝑠 ( 𝑟 𝑅 𝑎 ∨ 𝑟 = 𝑎 ) ) ) → ∃ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ¬ 𝑎 𝑅 𝑏 )