Step | Hyp | Ref
| Expression |
1 | | simpll1 1093 |
. . . . . 6
⊢ ((((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐴𝑅𝐵 ∧ 𝐴 ≠ 𝐵)) ∧ {𝑥 ∈ 𝑋 ∣ (¬ 𝐵𝑅𝑥 ∧ ¬ 𝑥𝑅𝐴)} = ∅) → 𝑅 ∈ TosetRel ) |
2 | | simpll3 1095 |
. . . . . 6
⊢ ((((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐴𝑅𝐵 ∧ 𝐴 ≠ 𝐵)) ∧ {𝑥 ∈ 𝑋 ∣ (¬ 𝐵𝑅𝑥 ∧ ¬ 𝑥𝑅𝐴)} = ∅) → 𝐵 ∈ 𝑋) |
3 | | ordthauslem.1 |
. . . . . . 7
⊢ 𝑋 = dom 𝑅 |
4 | 3 | ordtopn2 20809 |
. . . . . 6
⊢ ((𝑅 ∈ TosetRel ∧ 𝐵 ∈ 𝑋) → {𝑥 ∈ 𝑋 ∣ ¬ 𝐵𝑅𝑥} ∈ (ordTop‘𝑅)) |
5 | 1, 2, 4 | syl2anc 691 |
. . . . 5
⊢ ((((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐴𝑅𝐵 ∧ 𝐴 ≠ 𝐵)) ∧ {𝑥 ∈ 𝑋 ∣ (¬ 𝐵𝑅𝑥 ∧ ¬ 𝑥𝑅𝐴)} = ∅) → {𝑥 ∈ 𝑋 ∣ ¬ 𝐵𝑅𝑥} ∈ (ordTop‘𝑅)) |
6 | | simpll2 1094 |
. . . . . 6
⊢ ((((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐴𝑅𝐵 ∧ 𝐴 ≠ 𝐵)) ∧ {𝑥 ∈ 𝑋 ∣ (¬ 𝐵𝑅𝑥 ∧ ¬ 𝑥𝑅𝐴)} = ∅) → 𝐴 ∈ 𝑋) |
7 | 3 | ordtopn1 20808 |
. . . . . 6
⊢ ((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋) → {𝑥 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝐴} ∈ (ordTop‘𝑅)) |
8 | 1, 6, 7 | syl2anc 691 |
. . . . 5
⊢ ((((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐴𝑅𝐵 ∧ 𝐴 ≠ 𝐵)) ∧ {𝑥 ∈ 𝑋 ∣ (¬ 𝐵𝑅𝑥 ∧ ¬ 𝑥𝑅𝐴)} = ∅) → {𝑥 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝐴} ∈ (ordTop‘𝑅)) |
9 | | simprr 792 |
. . . . . . . 8
⊢ (((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐴𝑅𝐵 ∧ 𝐴 ≠ 𝐵)) → 𝐴 ≠ 𝐵) |
10 | | simpl1 1057 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐴𝑅𝐵 ∧ 𝐴 ≠ 𝐵)) → 𝑅 ∈ TosetRel ) |
11 | | tsrps 17044 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ TosetRel → 𝑅 ∈
PosetRel) |
12 | 10, 11 | syl 17 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐴𝑅𝐵 ∧ 𝐴 ≠ 𝐵)) → 𝑅 ∈ PosetRel) |
13 | | simprl 790 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐴𝑅𝐵 ∧ 𝐴 ≠ 𝐵)) → 𝐴𝑅𝐵) |
14 | | psasym 17033 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ PosetRel ∧ 𝐴𝑅𝐵 ∧ 𝐵𝑅𝐴) → 𝐴 = 𝐵) |
15 | 14 | 3expia 1259 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ PosetRel ∧ 𝐴𝑅𝐵) → (𝐵𝑅𝐴 → 𝐴 = 𝐵)) |
16 | 12, 13, 15 | syl2anc 691 |
. . . . . . . . 9
⊢ (((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐴𝑅𝐵 ∧ 𝐴 ≠ 𝐵)) → (𝐵𝑅𝐴 → 𝐴 = 𝐵)) |
17 | 16 | necon3ad 2795 |
. . . . . . . 8
⊢ (((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐴𝑅𝐵 ∧ 𝐴 ≠ 𝐵)) → (𝐴 ≠ 𝐵 → ¬ 𝐵𝑅𝐴)) |
18 | 9, 17 | mpd 15 |
. . . . . . 7
⊢ (((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐴𝑅𝐵 ∧ 𝐴 ≠ 𝐵)) → ¬ 𝐵𝑅𝐴) |
19 | 18 | adantr 480 |
. . . . . 6
⊢ ((((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐴𝑅𝐵 ∧ 𝐴 ≠ 𝐵)) ∧ {𝑥 ∈ 𝑋 ∣ (¬ 𝐵𝑅𝑥 ∧ ¬ 𝑥𝑅𝐴)} = ∅) → ¬ 𝐵𝑅𝐴) |
20 | | breq2 4587 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → (𝐵𝑅𝑥 ↔ 𝐵𝑅𝐴)) |
21 | 20 | notbid 307 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (¬ 𝐵𝑅𝑥 ↔ ¬ 𝐵𝑅𝐴)) |
22 | 21 | elrab 3331 |
. . . . . 6
⊢ (𝐴 ∈ {𝑥 ∈ 𝑋 ∣ ¬ 𝐵𝑅𝑥} ↔ (𝐴 ∈ 𝑋 ∧ ¬ 𝐵𝑅𝐴)) |
23 | 6, 19, 22 | sylanbrc 695 |
. . . . 5
⊢ ((((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐴𝑅𝐵 ∧ 𝐴 ≠ 𝐵)) ∧ {𝑥 ∈ 𝑋 ∣ (¬ 𝐵𝑅𝑥 ∧ ¬ 𝑥𝑅𝐴)} = ∅) → 𝐴 ∈ {𝑥 ∈ 𝑋 ∣ ¬ 𝐵𝑅𝑥}) |
24 | | breq1 4586 |
. . . . . . . 8
⊢ (𝑥 = 𝐵 → (𝑥𝑅𝐴 ↔ 𝐵𝑅𝐴)) |
25 | 24 | notbid 307 |
. . . . . . 7
⊢ (𝑥 = 𝐵 → (¬ 𝑥𝑅𝐴 ↔ ¬ 𝐵𝑅𝐴)) |
26 | 25 | elrab 3331 |
. . . . . 6
⊢ (𝐵 ∈ {𝑥 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝐴} ↔ (𝐵 ∈ 𝑋 ∧ ¬ 𝐵𝑅𝐴)) |
27 | 2, 19, 26 | sylanbrc 695 |
. . . . 5
⊢ ((((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐴𝑅𝐵 ∧ 𝐴 ≠ 𝐵)) ∧ {𝑥 ∈ 𝑋 ∣ (¬ 𝐵𝑅𝑥 ∧ ¬ 𝑥𝑅𝐴)} = ∅) → 𝐵 ∈ {𝑥 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝐴}) |
28 | | simpr 476 |
. . . . 5
⊢ ((((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐴𝑅𝐵 ∧ 𝐴 ≠ 𝐵)) ∧ {𝑥 ∈ 𝑋 ∣ (¬ 𝐵𝑅𝑥 ∧ ¬ 𝑥𝑅𝐴)} = ∅) → {𝑥 ∈ 𝑋 ∣ (¬ 𝐵𝑅𝑥 ∧ ¬ 𝑥𝑅𝐴)} = ∅) |
29 | | eleq2 2677 |
. . . . . . 7
⊢ (𝑚 = {𝑥 ∈ 𝑋 ∣ ¬ 𝐵𝑅𝑥} → (𝐴 ∈ 𝑚 ↔ 𝐴 ∈ {𝑥 ∈ 𝑋 ∣ ¬ 𝐵𝑅𝑥})) |
30 | | ineq1 3769 |
. . . . . . . 8
⊢ (𝑚 = {𝑥 ∈ 𝑋 ∣ ¬ 𝐵𝑅𝑥} → (𝑚 ∩ 𝑛) = ({𝑥 ∈ 𝑋 ∣ ¬ 𝐵𝑅𝑥} ∩ 𝑛)) |
31 | 30 | eqeq1d 2612 |
. . . . . . 7
⊢ (𝑚 = {𝑥 ∈ 𝑋 ∣ ¬ 𝐵𝑅𝑥} → ((𝑚 ∩ 𝑛) = ∅ ↔ ({𝑥 ∈ 𝑋 ∣ ¬ 𝐵𝑅𝑥} ∩ 𝑛) = ∅)) |
32 | 29, 31 | 3anbi13d 1393 |
. . . . . 6
⊢ (𝑚 = {𝑥 ∈ 𝑋 ∣ ¬ 𝐵𝑅𝑥} → ((𝐴 ∈ 𝑚 ∧ 𝐵 ∈ 𝑛 ∧ (𝑚 ∩ 𝑛) = ∅) ↔ (𝐴 ∈ {𝑥 ∈ 𝑋 ∣ ¬ 𝐵𝑅𝑥} ∧ 𝐵 ∈ 𝑛 ∧ ({𝑥 ∈ 𝑋 ∣ ¬ 𝐵𝑅𝑥} ∩ 𝑛) = ∅))) |
33 | | eleq2 2677 |
. . . . . . 7
⊢ (𝑛 = {𝑥 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝐴} → (𝐵 ∈ 𝑛 ↔ 𝐵 ∈ {𝑥 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝐴})) |
34 | | ineq2 3770 |
. . . . . . . . 9
⊢ (𝑛 = {𝑥 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝐴} → ({𝑥 ∈ 𝑋 ∣ ¬ 𝐵𝑅𝑥} ∩ 𝑛) = ({𝑥 ∈ 𝑋 ∣ ¬ 𝐵𝑅𝑥} ∩ {𝑥 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝐴})) |
35 | | inrab 3858 |
. . . . . . . . 9
⊢ ({𝑥 ∈ 𝑋 ∣ ¬ 𝐵𝑅𝑥} ∩ {𝑥 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝐴}) = {𝑥 ∈ 𝑋 ∣ (¬ 𝐵𝑅𝑥 ∧ ¬ 𝑥𝑅𝐴)} |
36 | 34, 35 | syl6eq 2660 |
. . . . . . . 8
⊢ (𝑛 = {𝑥 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝐴} → ({𝑥 ∈ 𝑋 ∣ ¬ 𝐵𝑅𝑥} ∩ 𝑛) = {𝑥 ∈ 𝑋 ∣ (¬ 𝐵𝑅𝑥 ∧ ¬ 𝑥𝑅𝐴)}) |
37 | 36 | eqeq1d 2612 |
. . . . . . 7
⊢ (𝑛 = {𝑥 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝐴} → (({𝑥 ∈ 𝑋 ∣ ¬ 𝐵𝑅𝑥} ∩ 𝑛) = ∅ ↔ {𝑥 ∈ 𝑋 ∣ (¬ 𝐵𝑅𝑥 ∧ ¬ 𝑥𝑅𝐴)} = ∅)) |
38 | 33, 37 | 3anbi23d 1394 |
. . . . . 6
⊢ (𝑛 = {𝑥 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝐴} → ((𝐴 ∈ {𝑥 ∈ 𝑋 ∣ ¬ 𝐵𝑅𝑥} ∧ 𝐵 ∈ 𝑛 ∧ ({𝑥 ∈ 𝑋 ∣ ¬ 𝐵𝑅𝑥} ∩ 𝑛) = ∅) ↔ (𝐴 ∈ {𝑥 ∈ 𝑋 ∣ ¬ 𝐵𝑅𝑥} ∧ 𝐵 ∈ {𝑥 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝐴} ∧ {𝑥 ∈ 𝑋 ∣ (¬ 𝐵𝑅𝑥 ∧ ¬ 𝑥𝑅𝐴)} = ∅))) |
39 | 32, 38 | rspc2ev 3295 |
. . . . 5
⊢ (({𝑥 ∈ 𝑋 ∣ ¬ 𝐵𝑅𝑥} ∈ (ordTop‘𝑅) ∧ {𝑥 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝐴} ∈ (ordTop‘𝑅) ∧ (𝐴 ∈ {𝑥 ∈ 𝑋 ∣ ¬ 𝐵𝑅𝑥} ∧ 𝐵 ∈ {𝑥 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝐴} ∧ {𝑥 ∈ 𝑋 ∣ (¬ 𝐵𝑅𝑥 ∧ ¬ 𝑥𝑅𝐴)} = ∅)) → ∃𝑚 ∈ (ordTop‘𝑅)∃𝑛 ∈ (ordTop‘𝑅)(𝐴 ∈ 𝑚 ∧ 𝐵 ∈ 𝑛 ∧ (𝑚 ∩ 𝑛) = ∅)) |
40 | 5, 8, 23, 27, 28, 39 | syl113anc 1330 |
. . . 4
⊢ ((((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐴𝑅𝐵 ∧ 𝐴 ≠ 𝐵)) ∧ {𝑥 ∈ 𝑋 ∣ (¬ 𝐵𝑅𝑥 ∧ ¬ 𝑥𝑅𝐴)} = ∅) → ∃𝑚 ∈ (ordTop‘𝑅)∃𝑛 ∈ (ordTop‘𝑅)(𝐴 ∈ 𝑚 ∧ 𝐵 ∈ 𝑛 ∧ (𝑚 ∩ 𝑛) = ∅)) |
41 | 40 | ex 449 |
. . 3
⊢ (((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐴𝑅𝐵 ∧ 𝐴 ≠ 𝐵)) → ({𝑥 ∈ 𝑋 ∣ (¬ 𝐵𝑅𝑥 ∧ ¬ 𝑥𝑅𝐴)} = ∅ → ∃𝑚 ∈ (ordTop‘𝑅)∃𝑛 ∈ (ordTop‘𝑅)(𝐴 ∈ 𝑚 ∧ 𝐵 ∈ 𝑛 ∧ (𝑚 ∩ 𝑛) = ∅))) |
42 | | rabn0 3912 |
. . . 4
⊢ ({𝑥 ∈ 𝑋 ∣ (¬ 𝐵𝑅𝑥 ∧ ¬ 𝑥𝑅𝐴)} ≠ ∅ ↔ ∃𝑥 ∈ 𝑋 (¬ 𝐵𝑅𝑥 ∧ ¬ 𝑥𝑅𝐴)) |
43 | | simpll1 1093 |
. . . . . . 7
⊢ ((((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐴𝑅𝐵 ∧ 𝐴 ≠ 𝐵)) ∧ (𝑥 ∈ 𝑋 ∧ (¬ 𝐵𝑅𝑥 ∧ ¬ 𝑥𝑅𝐴))) → 𝑅 ∈ TosetRel ) |
44 | | simprl 790 |
. . . . . . 7
⊢ ((((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐴𝑅𝐵 ∧ 𝐴 ≠ 𝐵)) ∧ (𝑥 ∈ 𝑋 ∧ (¬ 𝐵𝑅𝑥 ∧ ¬ 𝑥𝑅𝐴))) → 𝑥 ∈ 𝑋) |
45 | 3 | ordtopn2 20809 |
. . . . . . 7
⊢ ((𝑅 ∈ TosetRel ∧ 𝑥 ∈ 𝑋) → {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦} ∈ (ordTop‘𝑅)) |
46 | 43, 44, 45 | syl2anc 691 |
. . . . . 6
⊢ ((((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐴𝑅𝐵 ∧ 𝐴 ≠ 𝐵)) ∧ (𝑥 ∈ 𝑋 ∧ (¬ 𝐵𝑅𝑥 ∧ ¬ 𝑥𝑅𝐴))) → {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦} ∈ (ordTop‘𝑅)) |
47 | 3 | ordtopn1 20808 |
. . . . . . 7
⊢ ((𝑅 ∈ TosetRel ∧ 𝑥 ∈ 𝑋) → {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥} ∈ (ordTop‘𝑅)) |
48 | 43, 44, 47 | syl2anc 691 |
. . . . . 6
⊢ ((((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐴𝑅𝐵 ∧ 𝐴 ≠ 𝐵)) ∧ (𝑥 ∈ 𝑋 ∧ (¬ 𝐵𝑅𝑥 ∧ ¬ 𝑥𝑅𝐴))) → {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥} ∈ (ordTop‘𝑅)) |
49 | | simpll2 1094 |
. . . . . . 7
⊢ ((((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐴𝑅𝐵 ∧ 𝐴 ≠ 𝐵)) ∧ (𝑥 ∈ 𝑋 ∧ (¬ 𝐵𝑅𝑥 ∧ ¬ 𝑥𝑅𝐴))) → 𝐴 ∈ 𝑋) |
50 | | simprrr 801 |
. . . . . . 7
⊢ ((((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐴𝑅𝐵 ∧ 𝐴 ≠ 𝐵)) ∧ (𝑥 ∈ 𝑋 ∧ (¬ 𝐵𝑅𝑥 ∧ ¬ 𝑥𝑅𝐴))) → ¬ 𝑥𝑅𝐴) |
51 | | breq2 4587 |
. . . . . . . . 9
⊢ (𝑦 = 𝐴 → (𝑥𝑅𝑦 ↔ 𝑥𝑅𝐴)) |
52 | 51 | notbid 307 |
. . . . . . . 8
⊢ (𝑦 = 𝐴 → (¬ 𝑥𝑅𝑦 ↔ ¬ 𝑥𝑅𝐴)) |
53 | 52 | elrab 3331 |
. . . . . . 7
⊢ (𝐴 ∈ {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦} ↔ (𝐴 ∈ 𝑋 ∧ ¬ 𝑥𝑅𝐴)) |
54 | 49, 50, 53 | sylanbrc 695 |
. . . . . 6
⊢ ((((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐴𝑅𝐵 ∧ 𝐴 ≠ 𝐵)) ∧ (𝑥 ∈ 𝑋 ∧ (¬ 𝐵𝑅𝑥 ∧ ¬ 𝑥𝑅𝐴))) → 𝐴 ∈ {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦}) |
55 | | simpll3 1095 |
. . . . . . 7
⊢ ((((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐴𝑅𝐵 ∧ 𝐴 ≠ 𝐵)) ∧ (𝑥 ∈ 𝑋 ∧ (¬ 𝐵𝑅𝑥 ∧ ¬ 𝑥𝑅𝐴))) → 𝐵 ∈ 𝑋) |
56 | | simprrl 800 |
. . . . . . 7
⊢ ((((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐴𝑅𝐵 ∧ 𝐴 ≠ 𝐵)) ∧ (𝑥 ∈ 𝑋 ∧ (¬ 𝐵𝑅𝑥 ∧ ¬ 𝑥𝑅𝐴))) → ¬ 𝐵𝑅𝑥) |
57 | | breq1 4586 |
. . . . . . . . 9
⊢ (𝑦 = 𝐵 → (𝑦𝑅𝑥 ↔ 𝐵𝑅𝑥)) |
58 | 57 | notbid 307 |
. . . . . . . 8
⊢ (𝑦 = 𝐵 → (¬ 𝑦𝑅𝑥 ↔ ¬ 𝐵𝑅𝑥)) |
59 | 58 | elrab 3331 |
. . . . . . 7
⊢ (𝐵 ∈ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥} ↔ (𝐵 ∈ 𝑋 ∧ ¬ 𝐵𝑅𝑥)) |
60 | 55, 56, 59 | sylanbrc 695 |
. . . . . 6
⊢ ((((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐴𝑅𝐵 ∧ 𝐴 ≠ 𝐵)) ∧ (𝑥 ∈ 𝑋 ∧ (¬ 𝐵𝑅𝑥 ∧ ¬ 𝑥𝑅𝐴))) → 𝐵 ∈ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥}) |
61 | 43, 44 | jca 553 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐴𝑅𝐵 ∧ 𝐴 ≠ 𝐵)) ∧ (𝑥 ∈ 𝑋 ∧ (¬ 𝐵𝑅𝑥 ∧ ¬ 𝑥𝑅𝐴))) → (𝑅 ∈ TosetRel ∧ 𝑥 ∈ 𝑋)) |
62 | 3 | tsrlin 17042 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ TosetRel ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥𝑅𝑦 ∨ 𝑦𝑅𝑥)) |
63 | 62 | 3expa 1257 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ TosetRel ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝑥𝑅𝑦 ∨ 𝑦𝑅𝑥)) |
64 | 61, 63 | sylan 487 |
. . . . . . . . 9
⊢
(((((𝑅 ∈
TosetRel ∧ 𝐴 ∈
𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐴𝑅𝐵 ∧ 𝐴 ≠ 𝐵)) ∧ (𝑥 ∈ 𝑋 ∧ (¬ 𝐵𝑅𝑥 ∧ ¬ 𝑥𝑅𝐴))) ∧ 𝑦 ∈ 𝑋) → (𝑥𝑅𝑦 ∨ 𝑦𝑅𝑥)) |
65 | | oran 516 |
. . . . . . . . 9
⊢ ((𝑥𝑅𝑦 ∨ 𝑦𝑅𝑥) ↔ ¬ (¬ 𝑥𝑅𝑦 ∧ ¬ 𝑦𝑅𝑥)) |
66 | 64, 65 | sylib 207 |
. . . . . . . 8
⊢
(((((𝑅 ∈
TosetRel ∧ 𝐴 ∈
𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐴𝑅𝐵 ∧ 𝐴 ≠ 𝐵)) ∧ (𝑥 ∈ 𝑋 ∧ (¬ 𝐵𝑅𝑥 ∧ ¬ 𝑥𝑅𝐴))) ∧ 𝑦 ∈ 𝑋) → ¬ (¬ 𝑥𝑅𝑦 ∧ ¬ 𝑦𝑅𝑥)) |
67 | 66 | ralrimiva 2949 |
. . . . . . 7
⊢ ((((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐴𝑅𝐵 ∧ 𝐴 ≠ 𝐵)) ∧ (𝑥 ∈ 𝑋 ∧ (¬ 𝐵𝑅𝑥 ∧ ¬ 𝑥𝑅𝐴))) → ∀𝑦 ∈ 𝑋 ¬ (¬ 𝑥𝑅𝑦 ∧ ¬ 𝑦𝑅𝑥)) |
68 | | rabeq0 3911 |
. . . . . . 7
⊢ ({𝑦 ∈ 𝑋 ∣ (¬ 𝑥𝑅𝑦 ∧ ¬ 𝑦𝑅𝑥)} = ∅ ↔ ∀𝑦 ∈ 𝑋 ¬ (¬ 𝑥𝑅𝑦 ∧ ¬ 𝑦𝑅𝑥)) |
69 | 67, 68 | sylibr 223 |
. . . . . 6
⊢ ((((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐴𝑅𝐵 ∧ 𝐴 ≠ 𝐵)) ∧ (𝑥 ∈ 𝑋 ∧ (¬ 𝐵𝑅𝑥 ∧ ¬ 𝑥𝑅𝐴))) → {𝑦 ∈ 𝑋 ∣ (¬ 𝑥𝑅𝑦 ∧ ¬ 𝑦𝑅𝑥)} = ∅) |
70 | | eleq2 2677 |
. . . . . . . 8
⊢ (𝑚 = {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦} → (𝐴 ∈ 𝑚 ↔ 𝐴 ∈ {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦})) |
71 | | ineq1 3769 |
. . . . . . . . 9
⊢ (𝑚 = {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦} → (𝑚 ∩ 𝑛) = ({𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦} ∩ 𝑛)) |
72 | 71 | eqeq1d 2612 |
. . . . . . . 8
⊢ (𝑚 = {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦} → ((𝑚 ∩ 𝑛) = ∅ ↔ ({𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦} ∩ 𝑛) = ∅)) |
73 | 70, 72 | 3anbi13d 1393 |
. . . . . . 7
⊢ (𝑚 = {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦} → ((𝐴 ∈ 𝑚 ∧ 𝐵 ∈ 𝑛 ∧ (𝑚 ∩ 𝑛) = ∅) ↔ (𝐴 ∈ {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦} ∧ 𝐵 ∈ 𝑛 ∧ ({𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦} ∩ 𝑛) = ∅))) |
74 | | eleq2 2677 |
. . . . . . . 8
⊢ (𝑛 = {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥} → (𝐵 ∈ 𝑛 ↔ 𝐵 ∈ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥})) |
75 | | ineq2 3770 |
. . . . . . . . . 10
⊢ (𝑛 = {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥} → ({𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦} ∩ 𝑛) = ({𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦} ∩ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥})) |
76 | | inrab 3858 |
. . . . . . . . . 10
⊢ ({𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦} ∩ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥}) = {𝑦 ∈ 𝑋 ∣ (¬ 𝑥𝑅𝑦 ∧ ¬ 𝑦𝑅𝑥)} |
77 | 75, 76 | syl6eq 2660 |
. . . . . . . . 9
⊢ (𝑛 = {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥} → ({𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦} ∩ 𝑛) = {𝑦 ∈ 𝑋 ∣ (¬ 𝑥𝑅𝑦 ∧ ¬ 𝑦𝑅𝑥)}) |
78 | 77 | eqeq1d 2612 |
. . . . . . . 8
⊢ (𝑛 = {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥} → (({𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦} ∩ 𝑛) = ∅ ↔ {𝑦 ∈ 𝑋 ∣ (¬ 𝑥𝑅𝑦 ∧ ¬ 𝑦𝑅𝑥)} = ∅)) |
79 | 74, 78 | 3anbi23d 1394 |
. . . . . . 7
⊢ (𝑛 = {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥} → ((𝐴 ∈ {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦} ∧ 𝐵 ∈ 𝑛 ∧ ({𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦} ∩ 𝑛) = ∅) ↔ (𝐴 ∈ {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦} ∧ 𝐵 ∈ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥} ∧ {𝑦 ∈ 𝑋 ∣ (¬ 𝑥𝑅𝑦 ∧ ¬ 𝑦𝑅𝑥)} = ∅))) |
80 | 73, 79 | rspc2ev 3295 |
. . . . . 6
⊢ (({𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦} ∈ (ordTop‘𝑅) ∧ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥} ∈ (ordTop‘𝑅) ∧ (𝐴 ∈ {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦} ∧ 𝐵 ∈ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥} ∧ {𝑦 ∈ 𝑋 ∣ (¬ 𝑥𝑅𝑦 ∧ ¬ 𝑦𝑅𝑥)} = ∅)) → ∃𝑚 ∈ (ordTop‘𝑅)∃𝑛 ∈ (ordTop‘𝑅)(𝐴 ∈ 𝑚 ∧ 𝐵 ∈ 𝑛 ∧ (𝑚 ∩ 𝑛) = ∅)) |
81 | 46, 48, 54, 60, 69, 80 | syl113anc 1330 |
. . . . 5
⊢ ((((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐴𝑅𝐵 ∧ 𝐴 ≠ 𝐵)) ∧ (𝑥 ∈ 𝑋 ∧ (¬ 𝐵𝑅𝑥 ∧ ¬ 𝑥𝑅𝐴))) → ∃𝑚 ∈ (ordTop‘𝑅)∃𝑛 ∈ (ordTop‘𝑅)(𝐴 ∈ 𝑚 ∧ 𝐵 ∈ 𝑛 ∧ (𝑚 ∩ 𝑛) = ∅)) |
82 | 81 | rexlimdvaa 3014 |
. . . 4
⊢ (((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐴𝑅𝐵 ∧ 𝐴 ≠ 𝐵)) → (∃𝑥 ∈ 𝑋 (¬ 𝐵𝑅𝑥 ∧ ¬ 𝑥𝑅𝐴) → ∃𝑚 ∈ (ordTop‘𝑅)∃𝑛 ∈ (ordTop‘𝑅)(𝐴 ∈ 𝑚 ∧ 𝐵 ∈ 𝑛 ∧ (𝑚 ∩ 𝑛) = ∅))) |
83 | 42, 82 | syl5bi 231 |
. . 3
⊢ (((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐴𝑅𝐵 ∧ 𝐴 ≠ 𝐵)) → ({𝑥 ∈ 𝑋 ∣ (¬ 𝐵𝑅𝑥 ∧ ¬ 𝑥𝑅𝐴)} ≠ ∅ → ∃𝑚 ∈ (ordTop‘𝑅)∃𝑛 ∈ (ordTop‘𝑅)(𝐴 ∈ 𝑚 ∧ 𝐵 ∈ 𝑛 ∧ (𝑚 ∩ 𝑛) = ∅))) |
84 | 41, 83 | pm2.61dne 2868 |
. 2
⊢ (((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐴𝑅𝐵 ∧ 𝐴 ≠ 𝐵)) → ∃𝑚 ∈ (ordTop‘𝑅)∃𝑛 ∈ (ordTop‘𝑅)(𝐴 ∈ 𝑚 ∧ 𝐵 ∈ 𝑛 ∧ (𝑚 ∩ 𝑛) = ∅)) |
85 | 84 | exp32 629 |
1
⊢ ((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑅𝐵 → (𝐴 ≠ 𝐵 → ∃𝑚 ∈ (ordTop‘𝑅)∃𝑛 ∈ (ordTop‘𝑅)(𝐴 ∈ 𝑚 ∧ 𝐵 ∈ 𝑛 ∧ (𝑚 ∩ 𝑛) = ∅)))) |