Proof of Theorem zorn2lem7
| Step | Hyp | Ref
| Expression |
| 1 | | ween 10075 |
. . 3
⊢ (𝐴 ∈ dom card ↔
∃𝑤 𝑤 We 𝐴) |
| 2 | | zorn2lem.3 |
. . . . . . . . 9
⊢ 𝐹 = recs((𝑓 ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑤𝑣))) |
| 3 | | zorn2lem.4 |
. . . . . . . . 9
⊢ 𝐶 = {𝑧 ∈ 𝐴 ∣ ∀𝑔 ∈ ran 𝑓 𝑔𝑅𝑧} |
| 4 | | zorn2lem.5 |
. . . . . . . . 9
⊢ 𝐷 = {𝑧 ∈ 𝐴 ∣ ∀𝑔 ∈ (𝐹 “ 𝑥)𝑔𝑅𝑧} |
| 5 | 2, 3, 4 | zorn2lem4 10539 |
. . . . . . . 8
⊢ ((𝑅 Po 𝐴 ∧ 𝑤 We 𝐴) → ∃𝑥 ∈ On 𝐷 = ∅) |
| 6 | | imaeq2 6074 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → (𝐹 “ 𝑥) = (𝐹 “ 𝑦)) |
| 7 | 6 | raleqdv 3326 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (∀𝑔 ∈ (𝐹 “ 𝑥)𝑔𝑅𝑧 ↔ ∀𝑔 ∈ (𝐹 “ 𝑦)𝑔𝑅𝑧)) |
| 8 | 7 | rabbidv 3444 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → {𝑧 ∈ 𝐴 ∣ ∀𝑔 ∈ (𝐹 “ 𝑥)𝑔𝑅𝑧} = {𝑧 ∈ 𝐴 ∣ ∀𝑔 ∈ (𝐹 “ 𝑦)𝑔𝑅𝑧}) |
| 9 | | zorn2lem.7 |
. . . . . . . . . . . 12
⊢ 𝐻 = {𝑧 ∈ 𝐴 ∣ ∀𝑔 ∈ (𝐹 “ 𝑦)𝑔𝑅𝑧} |
| 10 | 8, 4, 9 | 3eqtr4g 2802 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → 𝐷 = 𝐻) |
| 11 | 10 | eqeq1d 2739 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝐷 = ∅ ↔ 𝐻 = ∅)) |
| 12 | 11 | onminex 7822 |
. . . . . . . . 9
⊢
(∃𝑥 ∈ On
𝐷 = ∅ →
∃𝑥 ∈ On (𝐷 = ∅ ∧ ∀𝑦 ∈ 𝑥 ¬ 𝐻 = ∅)) |
| 13 | | df-ne 2941 |
. . . . . . . . . . . 12
⊢ (𝐻 ≠ ∅ ↔ ¬ 𝐻 = ∅) |
| 14 | 13 | ralbii 3093 |
. . . . . . . . . . 11
⊢
(∀𝑦 ∈
𝑥 𝐻 ≠ ∅ ↔ ∀𝑦 ∈ 𝑥 ¬ 𝐻 = ∅) |
| 15 | 14 | anbi2i 623 |
. . . . . . . . . 10
⊢ ((𝐷 = ∅ ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅) ↔ (𝐷 = ∅ ∧ ∀𝑦 ∈ 𝑥 ¬ 𝐻 = ∅)) |
| 16 | 15 | rexbii 3094 |
. . . . . . . . 9
⊢
(∃𝑥 ∈ On
(𝐷 = ∅ ∧
∀𝑦 ∈ 𝑥 𝐻 ≠ ∅) ↔ ∃𝑥 ∈ On (𝐷 = ∅ ∧ ∀𝑦 ∈ 𝑥 ¬ 𝐻 = ∅)) |
| 17 | 12, 16 | sylibr 234 |
. . . . . . . 8
⊢
(∃𝑥 ∈ On
𝐷 = ∅ →
∃𝑥 ∈ On (𝐷 = ∅ ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅)) |
| 18 | 2, 3, 4, 9 | zorn2lem5 10540 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅) → (𝐹 “ 𝑥) ⊆ 𝐴) |
| 19 | 18 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑅 Po 𝐴 → (((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅) → (𝐹 “ 𝑥) ⊆ 𝐴)) |
| 20 | 2, 3, 4, 9 | zorn2lem6 10541 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑅 Po 𝐴 → (((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅) → 𝑅 Or (𝐹 “ 𝑥))) |
| 21 | 19, 20 | jcad 512 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑅 Po 𝐴 → (((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅) → ((𝐹 “ 𝑥) ⊆ 𝐴 ∧ 𝑅 Or (𝐹 “ 𝑥)))) |
| 22 | 2 | tfr1 8437 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝐹 Fn On |
| 23 | | fnfun 6668 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐹 Fn On → Fun 𝐹) |
| 24 | | vex 3484 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑥 ∈ V |
| 25 | 24 | funimaex 6655 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (Fun
𝐹 → (𝐹 “ 𝑥) ∈ V) |
| 26 | 22, 23, 25 | mp2b 10 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐹 “ 𝑥) ∈ V |
| 27 | | sseq1 4009 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑠 = (𝐹 “ 𝑥) → (𝑠 ⊆ 𝐴 ↔ (𝐹 “ 𝑥) ⊆ 𝐴)) |
| 28 | | soeq2 5614 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑠 = (𝐹 “ 𝑥) → (𝑅 Or 𝑠 ↔ 𝑅 Or (𝐹 “ 𝑥))) |
| 29 | 27, 28 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑠 = (𝐹 “ 𝑥) → ((𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠) ↔ ((𝐹 “ 𝑥) ⊆ 𝐴 ∧ 𝑅 Or (𝐹 “ 𝑥)))) |
| 30 | | raleq 3323 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑠 = (𝐹 “ 𝑥) → (∀𝑟 ∈ 𝑠 (𝑟𝑅𝑎 ∨ 𝑟 = 𝑎) ↔ ∀𝑟 ∈ (𝐹 “ 𝑥)(𝑟𝑅𝑎 ∨ 𝑟 = 𝑎))) |
| 31 | 30 | rexbidv 3179 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑠 = (𝐹 “ 𝑥) → (∃𝑎 ∈ 𝐴 ∀𝑟 ∈ 𝑠 (𝑟𝑅𝑎 ∨ 𝑟 = 𝑎) ↔ ∃𝑎 ∈ 𝐴 ∀𝑟 ∈ (𝐹 “ 𝑥)(𝑟𝑅𝑎 ∨ 𝑟 = 𝑎))) |
| 32 | 29, 31 | imbi12d 344 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑠 = (𝐹 “ 𝑥) → (((𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠) → ∃𝑎 ∈ 𝐴 ∀𝑟 ∈ 𝑠 (𝑟𝑅𝑎 ∨ 𝑟 = 𝑎)) ↔ (((𝐹 “ 𝑥) ⊆ 𝐴 ∧ 𝑅 Or (𝐹 “ 𝑥)) → ∃𝑎 ∈ 𝐴 ∀𝑟 ∈ (𝐹 “ 𝑥)(𝑟𝑅𝑎 ∨ 𝑟 = 𝑎)))) |
| 33 | 26, 32 | spcv 3605 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑠((𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠) → ∃𝑎 ∈ 𝐴 ∀𝑟 ∈ 𝑠 (𝑟𝑅𝑎 ∨ 𝑟 = 𝑎)) → (((𝐹 “ 𝑥) ⊆ 𝐴 ∧ 𝑅 Or (𝐹 “ 𝑥)) → ∃𝑎 ∈ 𝐴 ∀𝑟 ∈ (𝐹 “ 𝑥)(𝑟𝑅𝑎 ∨ 𝑟 = 𝑎))) |
| 34 | 21, 33 | sylan9 507 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 Po 𝐴 ∧ ∀𝑠((𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠) → ∃𝑎 ∈ 𝐴 ∀𝑟 ∈ 𝑠 (𝑟𝑅𝑎 ∨ 𝑟 = 𝑎))) → (((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅) → ∃𝑎 ∈ 𝐴 ∀𝑟 ∈ (𝐹 “ 𝑥)(𝑟𝑅𝑎 ∨ 𝑟 = 𝑎))) |
| 35 | 34 | adantld 490 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 Po 𝐴 ∧ ∀𝑠((𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠) → ∃𝑎 ∈ 𝐴 ∀𝑟 ∈ 𝑠 (𝑟𝑅𝑎 ∨ 𝑟 = 𝑎))) → ((𝐷 = ∅ ∧ ((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅)) → ∃𝑎 ∈ 𝐴 ∀𝑟 ∈ (𝐹 “ 𝑥)(𝑟𝑅𝑎 ∨ 𝑟 = 𝑎))) |
| 36 | 35 | imp 406 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 Po 𝐴 ∧ ∀𝑠((𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠) → ∃𝑎 ∈ 𝐴 ∀𝑟 ∈ 𝑠 (𝑟𝑅𝑎 ∨ 𝑟 = 𝑎))) ∧ (𝐷 = ∅ ∧ ((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅))) → ∃𝑎 ∈ 𝐴 ∀𝑟 ∈ (𝐹 “ 𝑥)(𝑟𝑅𝑎 ∨ 𝑟 = 𝑎)) |
| 37 | | noel 4338 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ¬
𝑏 ∈
∅ |
| 38 | 18 | sseld 3982 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅) → (𝑟 ∈ (𝐹 “ 𝑥) → 𝑟 ∈ 𝐴)) |
| 39 | | 3anass 1095 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ ((𝑟 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ↔ (𝑟 ∈ 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴))) |
| 40 | | potr 5605 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ ((𝑅 Po 𝐴 ∧ (𝑟 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((𝑟𝑅𝑎 ∧ 𝑎𝑅𝑏) → 𝑟𝑅𝑏)) |
| 41 | 39, 40 | sylan2br 595 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ ((𝑅 Po 𝐴 ∧ (𝑟 ∈ 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴))) → ((𝑟𝑅𝑎 ∧ 𝑎𝑅𝑏) → 𝑟𝑅𝑏)) |
| 42 | 41 | expcomd 416 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ ((𝑅 Po 𝐴 ∧ (𝑟 ∈ 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴))) → (𝑎𝑅𝑏 → (𝑟𝑅𝑎 → 𝑟𝑅𝑏))) |
| 43 | 42 | imp 406 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (((𝑅 Po 𝐴 ∧ (𝑟 ∈ 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴))) ∧ 𝑎𝑅𝑏) → (𝑟𝑅𝑎 → 𝑟𝑅𝑏)) |
| 44 | | breq1 5146 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ (𝑟 = 𝑎 → (𝑟𝑅𝑏 ↔ 𝑎𝑅𝑏)) |
| 45 | 44 | biimprcd 250 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ (𝑎𝑅𝑏 → (𝑟 = 𝑎 → 𝑟𝑅𝑏)) |
| 46 | 45 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (((𝑅 Po 𝐴 ∧ (𝑟 ∈ 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴))) ∧ 𝑎𝑅𝑏) → (𝑟 = 𝑎 → 𝑟𝑅𝑏)) |
| 47 | 43, 46 | jaod 860 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (((𝑅 Po 𝐴 ∧ (𝑟 ∈ 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴))) ∧ 𝑎𝑅𝑏) → ((𝑟𝑅𝑎 ∨ 𝑟 = 𝑎) → 𝑟𝑅𝑏)) |
| 48 | 47 | exp42 435 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝑅 Po 𝐴 → (𝑟 ∈ 𝐴 → ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → (𝑎𝑅𝑏 → ((𝑟𝑅𝑎 ∨ 𝑟 = 𝑎) → 𝑟𝑅𝑏))))) |
| 49 | 38, 48 | sylan9r 508 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅)) → (𝑟 ∈ (𝐹 “ 𝑥) → ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → (𝑎𝑅𝑏 → ((𝑟𝑅𝑎 ∨ 𝑟 = 𝑎) → 𝑟𝑅𝑏))))) |
| 50 | 49 | com24 95 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅)) → (𝑎𝑅𝑏 → ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → (𝑟 ∈ (𝐹 “ 𝑥) → ((𝑟𝑅𝑎 ∨ 𝑟 = 𝑎) → 𝑟𝑅𝑏))))) |
| 51 | 50 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅)) → ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → (𝑎𝑅𝑏 → (𝑟 ∈ (𝐹 “ 𝑥) → ((𝑟𝑅𝑎 ∨ 𝑟 = 𝑎) → 𝑟𝑅𝑏))))) |
| 52 | 51 | imp31 417 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((((𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅)) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) ∧ 𝑎𝑅𝑏) → (𝑟 ∈ (𝐹 “ 𝑥) → ((𝑟𝑅𝑎 ∨ 𝑟 = 𝑎) → 𝑟𝑅𝑏))) |
| 53 | 52 | a2d 29 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((((𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅)) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) ∧ 𝑎𝑅𝑏) → ((𝑟 ∈ (𝐹 “ 𝑥) → (𝑟𝑅𝑎 ∨ 𝑟 = 𝑎)) → (𝑟 ∈ (𝐹 “ 𝑥) → 𝑟𝑅𝑏))) |
| 54 | 53 | ralimdv2 3163 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((((𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅)) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) ∧ 𝑎𝑅𝑏) → (∀𝑟 ∈ (𝐹 “ 𝑥)(𝑟𝑅𝑎 ∨ 𝑟 = 𝑎) → ∀𝑟 ∈ (𝐹 “ 𝑥)𝑟𝑅𝑏)) |
| 55 | | breq1 5146 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑟 = 𝑔 → (𝑟𝑅𝑏 ↔ 𝑔𝑅𝑏)) |
| 56 | 55 | cbvralvw 3237 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
(∀𝑟 ∈
(𝐹 “ 𝑥)𝑟𝑅𝑏 ↔ ∀𝑔 ∈ (𝐹 “ 𝑥)𝑔𝑅𝑏) |
| 57 | | breq2 5147 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝑧 = 𝑏 → (𝑔𝑅𝑧 ↔ 𝑔𝑅𝑏)) |
| 58 | 57 | ralbidv 3178 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝑧 = 𝑏 → (∀𝑔 ∈ (𝐹 “ 𝑥)𝑔𝑅𝑧 ↔ ∀𝑔 ∈ (𝐹 “ 𝑥)𝑔𝑅𝑏)) |
| 59 | 58 | elrab 3692 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝑏 ∈ {𝑧 ∈ 𝐴 ∣ ∀𝑔 ∈ (𝐹 “ 𝑥)𝑔𝑅𝑧} ↔ (𝑏 ∈ 𝐴 ∧ ∀𝑔 ∈ (𝐹 “ 𝑥)𝑔𝑅𝑏)) |
| 60 | 4 | eqeq1i 2742 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝐷 = ∅ ↔ {𝑧 ∈ 𝐴 ∣ ∀𝑔 ∈ (𝐹 “ 𝑥)𝑔𝑅𝑧} = ∅) |
| 61 | | eleq2 2830 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ({𝑧 ∈ 𝐴 ∣ ∀𝑔 ∈ (𝐹 “ 𝑥)𝑔𝑅𝑧} = ∅ → (𝑏 ∈ {𝑧 ∈ 𝐴 ∣ ∀𝑔 ∈ (𝐹 “ 𝑥)𝑔𝑅𝑧} ↔ 𝑏 ∈ ∅)) |
| 62 | 60, 61 | sylbi 217 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝐷 = ∅ → (𝑏 ∈ {𝑧 ∈ 𝐴 ∣ ∀𝑔 ∈ (𝐹 “ 𝑥)𝑔𝑅𝑧} ↔ 𝑏 ∈ ∅)) |
| 63 | 59, 62 | bitr3id 285 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝐷 = ∅ → ((𝑏 ∈ 𝐴 ∧ ∀𝑔 ∈ (𝐹 “ 𝑥)𝑔𝑅𝑏) ↔ 𝑏 ∈ ∅)) |
| 64 | 63 | biimpd 229 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝐷 = ∅ → ((𝑏 ∈ 𝐴 ∧ ∀𝑔 ∈ (𝐹 “ 𝑥)𝑔𝑅𝑏) → 𝑏 ∈ ∅)) |
| 65 | 64 | expdimp 452 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝐷 = ∅ ∧ 𝑏 ∈ 𝐴) → (∀𝑔 ∈ (𝐹 “ 𝑥)𝑔𝑅𝑏 → 𝑏 ∈ ∅)) |
| 66 | 56, 65 | biimtrid 242 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝐷 = ∅ ∧ 𝑏 ∈ 𝐴) → (∀𝑟 ∈ (𝐹 “ 𝑥)𝑟𝑅𝑏 → 𝑏 ∈ ∅)) |
| 67 | 54, 66 | sylan9r 508 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝐷 = ∅ ∧ 𝑏 ∈ 𝐴) ∧ (((𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅)) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) ∧ 𝑎𝑅𝑏)) → (∀𝑟 ∈ (𝐹 “ 𝑥)(𝑟𝑅𝑎 ∨ 𝑟 = 𝑎) → 𝑏 ∈ ∅)) |
| 68 | 67 | exp32 420 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝐷 = ∅ ∧ 𝑏 ∈ 𝐴) → (((𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅)) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝑎𝑅𝑏 → (∀𝑟 ∈ (𝐹 “ 𝑥)(𝑟𝑅𝑎 ∨ 𝑟 = 𝑎) → 𝑏 ∈ ∅)))) |
| 69 | 68 | com34 91 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝐷 = ∅ ∧ 𝑏 ∈ 𝐴) → (((𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅)) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (∀𝑟 ∈ (𝐹 “ 𝑥)(𝑟𝑅𝑎 ∨ 𝑟 = 𝑎) → (𝑎𝑅𝑏 → 𝑏 ∈ ∅)))) |
| 70 | 69 | imp31 417 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((((𝐷 = ∅ ∧ 𝑏 ∈ 𝐴) ∧ ((𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅)) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴))) ∧ ∀𝑟 ∈ (𝐹 “ 𝑥)(𝑟𝑅𝑎 ∨ 𝑟 = 𝑎)) → (𝑎𝑅𝑏 → 𝑏 ∈ ∅)) |
| 71 | 37, 70 | mtoi 199 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝐷 = ∅ ∧ 𝑏 ∈ 𝐴) ∧ ((𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅)) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴))) ∧ ∀𝑟 ∈ (𝐹 “ 𝑥)(𝑟𝑅𝑎 ∨ 𝑟 = 𝑎)) → ¬ 𝑎𝑅𝑏) |
| 72 | 71 | exp42 435 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝐷 = ∅ ∧ 𝑏 ∈ 𝐴) → ((𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅)) → ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → (∀𝑟 ∈ (𝐹 “ 𝑥)(𝑟𝑅𝑎 ∨ 𝑟 = 𝑎) → ¬ 𝑎𝑅𝑏)))) |
| 73 | 72 | exp4a 431 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐷 = ∅ ∧ 𝑏 ∈ 𝐴) → ((𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅)) → (𝑎 ∈ 𝐴 → (𝑏 ∈ 𝐴 → (∀𝑟 ∈ (𝐹 “ 𝑥)(𝑟𝑅𝑎 ∨ 𝑟 = 𝑎) → ¬ 𝑎𝑅𝑏))))) |
| 74 | 73 | com34 91 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐷 = ∅ ∧ 𝑏 ∈ 𝐴) → ((𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅)) → (𝑏 ∈ 𝐴 → (𝑎 ∈ 𝐴 → (∀𝑟 ∈ (𝐹 “ 𝑥)(𝑟𝑅𝑎 ∨ 𝑟 = 𝑎) → ¬ 𝑎𝑅𝑏))))) |
| 75 | 74 | ex 412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐷 = ∅ → (𝑏 ∈ 𝐴 → ((𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅)) → (𝑏 ∈ 𝐴 → (𝑎 ∈ 𝐴 → (∀𝑟 ∈ (𝐹 “ 𝑥)(𝑟𝑅𝑎 ∨ 𝑟 = 𝑎) → ¬ 𝑎𝑅𝑏)))))) |
| 76 | 75 | com4r 94 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑏 ∈ 𝐴 → (𝐷 = ∅ → (𝑏 ∈ 𝐴 → ((𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅)) → (𝑎 ∈ 𝐴 → (∀𝑟 ∈ (𝐹 “ 𝑥)(𝑟𝑅𝑎 ∨ 𝑟 = 𝑎) → ¬ 𝑎𝑅𝑏)))))) |
| 77 | 76 | pm2.43a 54 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑏 ∈ 𝐴 → (𝐷 = ∅ → ((𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅)) → (𝑎 ∈ 𝐴 → (∀𝑟 ∈ (𝐹 “ 𝑥)(𝑟𝑅𝑎 ∨ 𝑟 = 𝑎) → ¬ 𝑎𝑅𝑏))))) |
| 78 | 77 | impd 410 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑏 ∈ 𝐴 → ((𝐷 = ∅ ∧ (𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅))) → (𝑎 ∈ 𝐴 → (∀𝑟 ∈ (𝐹 “ 𝑥)(𝑟𝑅𝑎 ∨ 𝑟 = 𝑎) → ¬ 𝑎𝑅𝑏)))) |
| 79 | 78 | com4l 92 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐷 = ∅ ∧ (𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅))) → (𝑎 ∈ 𝐴 → (∀𝑟 ∈ (𝐹 “ 𝑥)(𝑟𝑅𝑎 ∨ 𝑟 = 𝑎) → (𝑏 ∈ 𝐴 → ¬ 𝑎𝑅𝑏)))) |
| 80 | 79 | impd 410 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐷 = ∅ ∧ (𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅))) → ((𝑎 ∈ 𝐴 ∧ ∀𝑟 ∈ (𝐹 “ 𝑥)(𝑟𝑅𝑎 ∨ 𝑟 = 𝑎)) → (𝑏 ∈ 𝐴 → ¬ 𝑎𝑅𝑏))) |
| 81 | 80 | ralrimdv 3152 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐷 = ∅ ∧ (𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅))) → ((𝑎 ∈ 𝐴 ∧ ∀𝑟 ∈ (𝐹 “ 𝑥)(𝑟𝑅𝑎 ∨ 𝑟 = 𝑎)) → ∀𝑏 ∈ 𝐴 ¬ 𝑎𝑅𝑏)) |
| 82 | 81 | expd 415 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐷 = ∅ ∧ (𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅))) → (𝑎 ∈ 𝐴 → (∀𝑟 ∈ (𝐹 “ 𝑥)(𝑟𝑅𝑎 ∨ 𝑟 = 𝑎) → ∀𝑏 ∈ 𝐴 ¬ 𝑎𝑅𝑏))) |
| 83 | 82 | reximdvai 3165 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐷 = ∅ ∧ (𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅))) → (∃𝑎 ∈ 𝐴 ∀𝑟 ∈ (𝐹 “ 𝑥)(𝑟𝑅𝑎 ∨ 𝑟 = 𝑎) → ∃𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 ¬ 𝑎𝑅𝑏)) |
| 84 | 83 | exp32 420 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐷 = ∅ → (𝑅 Po 𝐴 → (((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅) → (∃𝑎 ∈ 𝐴 ∀𝑟 ∈ (𝐹 “ 𝑥)(𝑟𝑅𝑎 ∨ 𝑟 = 𝑎) → ∃𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 ¬ 𝑎𝑅𝑏)))) |
| 85 | 84 | com12 32 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑅 Po 𝐴 → (𝐷 = ∅ → (((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅) → (∃𝑎 ∈ 𝐴 ∀𝑟 ∈ (𝐹 “ 𝑥)(𝑟𝑅𝑎 ∨ 𝑟 = 𝑎) → ∃𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 ¬ 𝑎𝑅𝑏)))) |
| 86 | 85 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 Po 𝐴 ∧ ∀𝑠((𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠) → ∃𝑎 ∈ 𝐴 ∀𝑟 ∈ 𝑠 (𝑟𝑅𝑎 ∨ 𝑟 = 𝑎))) → (𝐷 = ∅ → (((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅) → (∃𝑎 ∈ 𝐴 ∀𝑟 ∈ (𝐹 “ 𝑥)(𝑟𝑅𝑎 ∨ 𝑟 = 𝑎) → ∃𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 ¬ 𝑎𝑅𝑏)))) |
| 87 | 86 | imp32 418 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 Po 𝐴 ∧ ∀𝑠((𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠) → ∃𝑎 ∈ 𝐴 ∀𝑟 ∈ 𝑠 (𝑟𝑅𝑎 ∨ 𝑟 = 𝑎))) ∧ (𝐷 = ∅ ∧ ((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅))) → (∃𝑎 ∈ 𝐴 ∀𝑟 ∈ (𝐹 “ 𝑥)(𝑟𝑅𝑎 ∨ 𝑟 = 𝑎) → ∃𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 ¬ 𝑎𝑅𝑏)) |
| 88 | 36, 87 | mpd 15 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 Po 𝐴 ∧ ∀𝑠((𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠) → ∃𝑎 ∈ 𝐴 ∀𝑟 ∈ 𝑠 (𝑟𝑅𝑎 ∨ 𝑟 = 𝑎))) ∧ (𝐷 = ∅ ∧ ((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅))) → ∃𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 ¬ 𝑎𝑅𝑏) |
| 89 | 88 | exp45 438 |
. . . . . . . . . . . . 13
⊢ ((𝑅 Po 𝐴 ∧ ∀𝑠((𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠) → ∃𝑎 ∈ 𝐴 ∀𝑟 ∈ 𝑠 (𝑟𝑅𝑎 ∨ 𝑟 = 𝑎))) → (𝐷 = ∅ → ((𝑤 We 𝐴 ∧ 𝑥 ∈ On) → (∀𝑦 ∈ 𝑥 𝐻 ≠ ∅ → ∃𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 ¬ 𝑎𝑅𝑏)))) |
| 90 | 89 | com23 86 |
. . . . . . . . . . . 12
⊢ ((𝑅 Po 𝐴 ∧ ∀𝑠((𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠) → ∃𝑎 ∈ 𝐴 ∀𝑟 ∈ 𝑠 (𝑟𝑅𝑎 ∨ 𝑟 = 𝑎))) → ((𝑤 We 𝐴 ∧ 𝑥 ∈ On) → (𝐷 = ∅ → (∀𝑦 ∈ 𝑥 𝐻 ≠ ∅ → ∃𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 ¬ 𝑎𝑅𝑏)))) |
| 91 | 90 | expdimp 452 |
. . . . . . . . . . 11
⊢ (((𝑅 Po 𝐴 ∧ ∀𝑠((𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠) → ∃𝑎 ∈ 𝐴 ∀𝑟 ∈ 𝑠 (𝑟𝑅𝑎 ∨ 𝑟 = 𝑎))) ∧ 𝑤 We 𝐴) → (𝑥 ∈ On → (𝐷 = ∅ → (∀𝑦 ∈ 𝑥 𝐻 ≠ ∅ → ∃𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 ¬ 𝑎𝑅𝑏)))) |
| 92 | 91 | imp4a 422 |
. . . . . . . . . 10
⊢ (((𝑅 Po 𝐴 ∧ ∀𝑠((𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠) → ∃𝑎 ∈ 𝐴 ∀𝑟 ∈ 𝑠 (𝑟𝑅𝑎 ∨ 𝑟 = 𝑎))) ∧ 𝑤 We 𝐴) → (𝑥 ∈ On → ((𝐷 = ∅ ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅) → ∃𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 ¬ 𝑎𝑅𝑏))) |
| 93 | 92 | com3l 89 |
. . . . . . . . 9
⊢ (𝑥 ∈ On → ((𝐷 = ∅ ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅) → (((𝑅 Po 𝐴 ∧ ∀𝑠((𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠) → ∃𝑎 ∈ 𝐴 ∀𝑟 ∈ 𝑠 (𝑟𝑅𝑎 ∨ 𝑟 = 𝑎))) ∧ 𝑤 We 𝐴) → ∃𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 ¬ 𝑎𝑅𝑏))) |
| 94 | 93 | rexlimiv 3148 |
. . . . . . . 8
⊢
(∃𝑥 ∈ On
(𝐷 = ∅ ∧
∀𝑦 ∈ 𝑥 𝐻 ≠ ∅) → (((𝑅 Po 𝐴 ∧ ∀𝑠((𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠) → ∃𝑎 ∈ 𝐴 ∀𝑟 ∈ 𝑠 (𝑟𝑅𝑎 ∨ 𝑟 = 𝑎))) ∧ 𝑤 We 𝐴) → ∃𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 ¬ 𝑎𝑅𝑏)) |
| 95 | 5, 17, 94 | 3syl 18 |
. . . . . . 7
⊢ ((𝑅 Po 𝐴 ∧ 𝑤 We 𝐴) → (((𝑅 Po 𝐴 ∧ ∀𝑠((𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠) → ∃𝑎 ∈ 𝐴 ∀𝑟 ∈ 𝑠 (𝑟𝑅𝑎 ∨ 𝑟 = 𝑎))) ∧ 𝑤 We 𝐴) → ∃𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 ¬ 𝑎𝑅𝑏)) |
| 96 | 95 | adantlr 715 |
. . . . . 6
⊢ (((𝑅 Po 𝐴 ∧ ∀𝑠((𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠) → ∃𝑎 ∈ 𝐴 ∀𝑟 ∈ 𝑠 (𝑟𝑅𝑎 ∨ 𝑟 = 𝑎))) ∧ 𝑤 We 𝐴) → (((𝑅 Po 𝐴 ∧ ∀𝑠((𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠) → ∃𝑎 ∈ 𝐴 ∀𝑟 ∈ 𝑠 (𝑟𝑅𝑎 ∨ 𝑟 = 𝑎))) ∧ 𝑤 We 𝐴) → ∃𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 ¬ 𝑎𝑅𝑏)) |
| 97 | 96 | pm2.43i 52 |
. . . . 5
⊢ (((𝑅 Po 𝐴 ∧ ∀𝑠((𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠) → ∃𝑎 ∈ 𝐴 ∀𝑟 ∈ 𝑠 (𝑟𝑅𝑎 ∨ 𝑟 = 𝑎))) ∧ 𝑤 We 𝐴) → ∃𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 ¬ 𝑎𝑅𝑏) |
| 98 | 97 | expcom 413 |
. . . 4
⊢ (𝑤 We 𝐴 → ((𝑅 Po 𝐴 ∧ ∀𝑠((𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠) → ∃𝑎 ∈ 𝐴 ∀𝑟 ∈ 𝑠 (𝑟𝑅𝑎 ∨ 𝑟 = 𝑎))) → ∃𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 ¬ 𝑎𝑅𝑏)) |
| 99 | 98 | exlimiv 1930 |
. . 3
⊢
(∃𝑤 𝑤 We 𝐴 → ((𝑅 Po 𝐴 ∧ ∀𝑠((𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠) → ∃𝑎 ∈ 𝐴 ∀𝑟 ∈ 𝑠 (𝑟𝑅𝑎 ∨ 𝑟 = 𝑎))) → ∃𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 ¬ 𝑎𝑅𝑏)) |
| 100 | 1, 99 | sylbi 217 |
. 2
⊢ (𝐴 ∈ dom card → ((𝑅 Po 𝐴 ∧ ∀𝑠((𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠) → ∃𝑎 ∈ 𝐴 ∀𝑟 ∈ 𝑠 (𝑟𝑅𝑎 ∨ 𝑟 = 𝑎))) → ∃𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 ¬ 𝑎𝑅𝑏)) |
| 101 | 100 | 3impib 1117 |
1
⊢ ((𝐴 ∈ dom card ∧ 𝑅 Po 𝐴 ∧ ∀𝑠((𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠) → ∃𝑎 ∈ 𝐴 ∀𝑟 ∈ 𝑠 (𝑟𝑅𝑎 ∨ 𝑟 = 𝑎))) → ∃𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 ¬ 𝑎𝑅𝑏) |