Step | Hyp | Ref
| Expression |
1 | | swoer.1 |
. . . . 5
⊢ 𝑅 = ((𝑋 × 𝑋) ∖ ( < ∪ ◡ < )) |
2 | | difss 4022 |
. . . . 5
⊢ ((𝑋 × 𝑋) ∖ ( < ∪ ◡ < )) ⊆ (𝑋 × 𝑋) |
3 | 1, 2 | eqsstri 3911 |
. . . 4
⊢ 𝑅 ⊆ (𝑋 × 𝑋) |
4 | | relxp 5543 |
. . . 4
⊢ Rel
(𝑋 × 𝑋) |
5 | | relss 5627 |
. . . 4
⊢ (𝑅 ⊆ (𝑋 × 𝑋) → (Rel (𝑋 × 𝑋) → Rel 𝑅)) |
6 | 3, 4, 5 | mp2 9 |
. . 3
⊢ Rel 𝑅 |
7 | 6 | a1i 11 |
. 2
⊢ (𝜑 → Rel 𝑅) |
8 | | simpr 488 |
. . 3
⊢ ((𝜑 ∧ 𝑢𝑅𝑣) → 𝑢𝑅𝑣) |
9 | | orcom 869 |
. . . . . 6
⊢ ((𝑢 < 𝑣 ∨ 𝑣 < 𝑢) ↔ (𝑣 < 𝑢 ∨ 𝑢 < 𝑣)) |
10 | 9 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢𝑅𝑣) → ((𝑢 < 𝑣 ∨ 𝑣 < 𝑢) ↔ (𝑣 < 𝑢 ∨ 𝑢 < 𝑣))) |
11 | 10 | notbid 321 |
. . . 4
⊢ ((𝜑 ∧ 𝑢𝑅𝑣) → (¬ (𝑢 < 𝑣 ∨ 𝑣 < 𝑢) ↔ ¬ (𝑣 < 𝑢 ∨ 𝑢 < 𝑣))) |
12 | 3 | ssbri 5075 |
. . . . . . 7
⊢ (𝑢𝑅𝑣 → 𝑢(𝑋 × 𝑋)𝑣) |
13 | 12 | adantl 485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢𝑅𝑣) → 𝑢(𝑋 × 𝑋)𝑣) |
14 | | brxp 5572 |
. . . . . 6
⊢ (𝑢(𝑋 × 𝑋)𝑣 ↔ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) |
15 | 13, 14 | sylib 221 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢𝑅𝑣) → (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) |
16 | 1 | brdifun 8351 |
. . . . 5
⊢ ((𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋) → (𝑢𝑅𝑣 ↔ ¬ (𝑢 < 𝑣 ∨ 𝑣 < 𝑢))) |
17 | 15, 16 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑢𝑅𝑣) → (𝑢𝑅𝑣 ↔ ¬ (𝑢 < 𝑣 ∨ 𝑣 < 𝑢))) |
18 | 15 | simprd 499 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢𝑅𝑣) → 𝑣 ∈ 𝑋) |
19 | 15 | simpld 498 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢𝑅𝑣) → 𝑢 ∈ 𝑋) |
20 | 1 | brdifun 8351 |
. . . . 5
⊢ ((𝑣 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋) → (𝑣𝑅𝑢 ↔ ¬ (𝑣 < 𝑢 ∨ 𝑢 < 𝑣))) |
21 | 18, 19, 20 | syl2anc 587 |
. . . 4
⊢ ((𝜑 ∧ 𝑢𝑅𝑣) → (𝑣𝑅𝑢 ↔ ¬ (𝑣 < 𝑢 ∨ 𝑢 < 𝑣))) |
22 | 11, 17, 21 | 3bitr4d 314 |
. . 3
⊢ ((𝜑 ∧ 𝑢𝑅𝑣) → (𝑢𝑅𝑣 ↔ 𝑣𝑅𝑢)) |
23 | 8, 22 | mpbid 235 |
. 2
⊢ ((𝜑 ∧ 𝑢𝑅𝑣) → 𝑣𝑅𝑢) |
24 | | simprl 771 |
. . . . 5
⊢ ((𝜑 ∧ (𝑢𝑅𝑣 ∧ 𝑣𝑅𝑤)) → 𝑢𝑅𝑣) |
25 | 12 | ad2antrl 728 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑢𝑅𝑣 ∧ 𝑣𝑅𝑤)) → 𝑢(𝑋 × 𝑋)𝑣) |
26 | 14 | simplbi 501 |
. . . . . . 7
⊢ (𝑢(𝑋 × 𝑋)𝑣 → 𝑢 ∈ 𝑋) |
27 | 25, 26 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑢𝑅𝑣 ∧ 𝑣𝑅𝑤)) → 𝑢 ∈ 𝑋) |
28 | 14 | simprbi 500 |
. . . . . . 7
⊢ (𝑢(𝑋 × 𝑋)𝑣 → 𝑣 ∈ 𝑋) |
29 | 25, 28 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑢𝑅𝑣 ∧ 𝑣𝑅𝑤)) → 𝑣 ∈ 𝑋) |
30 | 27, 29, 16 | syl2anc 587 |
. . . . 5
⊢ ((𝜑 ∧ (𝑢𝑅𝑣 ∧ 𝑣𝑅𝑤)) → (𝑢𝑅𝑣 ↔ ¬ (𝑢 < 𝑣 ∨ 𝑣 < 𝑢))) |
31 | 24, 30 | mpbid 235 |
. . . 4
⊢ ((𝜑 ∧ (𝑢𝑅𝑣 ∧ 𝑣𝑅𝑤)) → ¬ (𝑢 < 𝑣 ∨ 𝑣 < 𝑢)) |
32 | | simprr 773 |
. . . . 5
⊢ ((𝜑 ∧ (𝑢𝑅𝑣 ∧ 𝑣𝑅𝑤)) → 𝑣𝑅𝑤) |
33 | 3 | brel 5588 |
. . . . . . . 8
⊢ (𝑣𝑅𝑤 → (𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) |
34 | 33 | simprd 499 |
. . . . . . 7
⊢ (𝑣𝑅𝑤 → 𝑤 ∈ 𝑋) |
35 | 32, 34 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑢𝑅𝑣 ∧ 𝑣𝑅𝑤)) → 𝑤 ∈ 𝑋) |
36 | 1 | brdifun 8351 |
. . . . . 6
⊢ ((𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) → (𝑣𝑅𝑤 ↔ ¬ (𝑣 < 𝑤 ∨ 𝑤 < 𝑣))) |
37 | 29, 35, 36 | syl2anc 587 |
. . . . 5
⊢ ((𝜑 ∧ (𝑢𝑅𝑣 ∧ 𝑣𝑅𝑤)) → (𝑣𝑅𝑤 ↔ ¬ (𝑣 < 𝑤 ∨ 𝑤 < 𝑣))) |
38 | 32, 37 | mpbid 235 |
. . . 4
⊢ ((𝜑 ∧ (𝑢𝑅𝑣 ∧ 𝑣𝑅𝑤)) → ¬ (𝑣 < 𝑤 ∨ 𝑤 < 𝑣)) |
39 | | simpl 486 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑢𝑅𝑣 ∧ 𝑣𝑅𝑤)) → 𝜑) |
40 | | swoer.3 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦))) |
41 | 40 | swopolem 5452 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑢 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → (𝑢 < 𝑤 → (𝑢 < 𝑣 ∨ 𝑣 < 𝑤))) |
42 | 39, 27, 35, 29, 41 | syl13anc 1373 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑢𝑅𝑣 ∧ 𝑣𝑅𝑤)) → (𝑢 < 𝑤 → (𝑢 < 𝑣 ∨ 𝑣 < 𝑤))) |
43 | 40 | swopolem 5452 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑤 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → (𝑤 < 𝑢 → (𝑤 < 𝑣 ∨ 𝑣 < 𝑢))) |
44 | 39, 35, 27, 29, 43 | syl13anc 1373 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑢𝑅𝑣 ∧ 𝑣𝑅𝑤)) → (𝑤 < 𝑢 → (𝑤 < 𝑣 ∨ 𝑣 < 𝑢))) |
45 | | orcom 869 |
. . . . . . 7
⊢ ((𝑣 < 𝑢 ∨ 𝑤 < 𝑣) ↔ (𝑤 < 𝑣 ∨ 𝑣 < 𝑢)) |
46 | 44, 45 | syl6ibr 255 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑢𝑅𝑣 ∧ 𝑣𝑅𝑤)) → (𝑤 < 𝑢 → (𝑣 < 𝑢 ∨ 𝑤 < 𝑣))) |
47 | 42, 46 | orim12d 964 |
. . . . 5
⊢ ((𝜑 ∧ (𝑢𝑅𝑣 ∧ 𝑣𝑅𝑤)) → ((𝑢 < 𝑤 ∨ 𝑤 < 𝑢) → ((𝑢 < 𝑣 ∨ 𝑣 < 𝑤) ∨ (𝑣 < 𝑢 ∨ 𝑤 < 𝑣)))) |
48 | | or4 926 |
. . . . 5
⊢ (((𝑢 < 𝑣 ∨ 𝑣 < 𝑤) ∨ (𝑣 < 𝑢 ∨ 𝑤 < 𝑣)) ↔ ((𝑢 < 𝑣 ∨ 𝑣 < 𝑢) ∨ (𝑣 < 𝑤 ∨ 𝑤 < 𝑣))) |
49 | 47, 48 | syl6ib 254 |
. . . 4
⊢ ((𝜑 ∧ (𝑢𝑅𝑣 ∧ 𝑣𝑅𝑤)) → ((𝑢 < 𝑤 ∨ 𝑤 < 𝑢) → ((𝑢 < 𝑣 ∨ 𝑣 < 𝑢) ∨ (𝑣 < 𝑤 ∨ 𝑤 < 𝑣)))) |
50 | 31, 38, 49 | mtord 879 |
. . 3
⊢ ((𝜑 ∧ (𝑢𝑅𝑣 ∧ 𝑣𝑅𝑤)) → ¬ (𝑢 < 𝑤 ∨ 𝑤 < 𝑢)) |
51 | 1 | brdifun 8351 |
. . . 4
⊢ ((𝑢 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) → (𝑢𝑅𝑤 ↔ ¬ (𝑢 < 𝑤 ∨ 𝑤 < 𝑢))) |
52 | 27, 35, 51 | syl2anc 587 |
. . 3
⊢ ((𝜑 ∧ (𝑢𝑅𝑣 ∧ 𝑣𝑅𝑤)) → (𝑢𝑅𝑤 ↔ ¬ (𝑢 < 𝑤 ∨ 𝑤 < 𝑢))) |
53 | 50, 52 | mpbird 260 |
. 2
⊢ ((𝜑 ∧ (𝑢𝑅𝑣 ∧ 𝑣𝑅𝑤)) → 𝑢𝑅𝑤) |
54 | | swoer.2 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑦 < 𝑧 → ¬ 𝑧 < 𝑦)) |
55 | 54, 40 | swopo 5453 |
. . . . . 6
⊢ (𝜑 → < Po 𝑋) |
56 | | poirr 5454 |
. . . . . 6
⊢ (( < Po 𝑋 ∧ 𝑢 ∈ 𝑋) → ¬ 𝑢 < 𝑢) |
57 | 55, 56 | sylan 583 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑋) → ¬ 𝑢 < 𝑢) |
58 | | pm1.2 903 |
. . . . 5
⊢ ((𝑢 < 𝑢 ∨ 𝑢 < 𝑢) → 𝑢 < 𝑢) |
59 | 57, 58 | nsyl 142 |
. . . 4
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑋) → ¬ (𝑢 < 𝑢 ∨ 𝑢 < 𝑢)) |
60 | | simpr 488 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑋) → 𝑢 ∈ 𝑋) |
61 | 1 | brdifun 8351 |
. . . . 5
⊢ ((𝑢 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋) → (𝑢𝑅𝑢 ↔ ¬ (𝑢 < 𝑢 ∨ 𝑢 < 𝑢))) |
62 | 60, 60, 61 | syl2anc 587 |
. . . 4
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑋) → (𝑢𝑅𝑢 ↔ ¬ (𝑢 < 𝑢 ∨ 𝑢 < 𝑢))) |
63 | 59, 62 | mpbird 260 |
. . 3
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑋) → 𝑢𝑅𝑢) |
64 | 3 | ssbri 5075 |
. . . . 5
⊢ (𝑢𝑅𝑢 → 𝑢(𝑋 × 𝑋)𝑢) |
65 | | brxp 5572 |
. . . . . 6
⊢ (𝑢(𝑋 × 𝑋)𝑢 ↔ (𝑢 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋)) |
66 | 65 | simplbi 501 |
. . . . 5
⊢ (𝑢(𝑋 × 𝑋)𝑢 → 𝑢 ∈ 𝑋) |
67 | 64, 66 | syl 17 |
. . . 4
⊢ (𝑢𝑅𝑢 → 𝑢 ∈ 𝑋) |
68 | 67 | adantl 485 |
. . 3
⊢ ((𝜑 ∧ 𝑢𝑅𝑢) → 𝑢 ∈ 𝑋) |
69 | 63, 68 | impbida 801 |
. 2
⊢ (𝜑 → (𝑢 ∈ 𝑋 ↔ 𝑢𝑅𝑢)) |
70 | 7, 23, 53, 69 | iserd 8348 |
1
⊢ (𝜑 → 𝑅 Er 𝑋) |