Step |
Hyp |
Ref |
Expression |
1 |
|
swoer.1 |
⊢ 𝑅 = ( ( 𝑋 × 𝑋 ) ∖ ( < ∪ ◡ < ) ) |
2 |
|
swoer.2 |
⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑦 < 𝑧 → ¬ 𝑧 < 𝑦 ) ) |
3 |
|
swoer.3 |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑥 < 𝑦 → ( 𝑥 < 𝑧 ∨ 𝑧 < 𝑦 ) ) ) |
4 |
|
difss |
⊢ ( ( 𝑋 × 𝑋 ) ∖ ( < ∪ ◡ < ) ) ⊆ ( 𝑋 × 𝑋 ) |
5 |
1 4
|
eqsstri |
⊢ 𝑅 ⊆ ( 𝑋 × 𝑋 ) |
6 |
|
relxp |
⊢ Rel ( 𝑋 × 𝑋 ) |
7 |
|
relss |
⊢ ( 𝑅 ⊆ ( 𝑋 × 𝑋 ) → ( Rel ( 𝑋 × 𝑋 ) → Rel 𝑅 ) ) |
8 |
5 6 7
|
mp2 |
⊢ Rel 𝑅 |
9 |
8
|
a1i |
⊢ ( 𝜑 → Rel 𝑅 ) |
10 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑢 𝑅 𝑣 ) → 𝑢 𝑅 𝑣 ) |
11 |
|
orcom |
⊢ ( ( 𝑢 < 𝑣 ∨ 𝑣 < 𝑢 ) ↔ ( 𝑣 < 𝑢 ∨ 𝑢 < 𝑣 ) ) |
12 |
11
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑢 𝑅 𝑣 ) → ( ( 𝑢 < 𝑣 ∨ 𝑣 < 𝑢 ) ↔ ( 𝑣 < 𝑢 ∨ 𝑢 < 𝑣 ) ) ) |
13 |
12
|
notbid |
⊢ ( ( 𝜑 ∧ 𝑢 𝑅 𝑣 ) → ( ¬ ( 𝑢 < 𝑣 ∨ 𝑣 < 𝑢 ) ↔ ¬ ( 𝑣 < 𝑢 ∨ 𝑢 < 𝑣 ) ) ) |
14 |
5
|
ssbri |
⊢ ( 𝑢 𝑅 𝑣 → 𝑢 ( 𝑋 × 𝑋 ) 𝑣 ) |
15 |
14
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑢 𝑅 𝑣 ) → 𝑢 ( 𝑋 × 𝑋 ) 𝑣 ) |
16 |
|
brxp |
⊢ ( 𝑢 ( 𝑋 × 𝑋 ) 𝑣 ↔ ( 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋 ) ) |
17 |
15 16
|
sylib |
⊢ ( ( 𝜑 ∧ 𝑢 𝑅 𝑣 ) → ( 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋 ) ) |
18 |
1
|
brdifun |
⊢ ( ( 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋 ) → ( 𝑢 𝑅 𝑣 ↔ ¬ ( 𝑢 < 𝑣 ∨ 𝑣 < 𝑢 ) ) ) |
19 |
17 18
|
syl |
⊢ ( ( 𝜑 ∧ 𝑢 𝑅 𝑣 ) → ( 𝑢 𝑅 𝑣 ↔ ¬ ( 𝑢 < 𝑣 ∨ 𝑣 < 𝑢 ) ) ) |
20 |
17
|
simprd |
⊢ ( ( 𝜑 ∧ 𝑢 𝑅 𝑣 ) → 𝑣 ∈ 𝑋 ) |
21 |
17
|
simpld |
⊢ ( ( 𝜑 ∧ 𝑢 𝑅 𝑣 ) → 𝑢 ∈ 𝑋 ) |
22 |
1
|
brdifun |
⊢ ( ( 𝑣 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋 ) → ( 𝑣 𝑅 𝑢 ↔ ¬ ( 𝑣 < 𝑢 ∨ 𝑢 < 𝑣 ) ) ) |
23 |
20 21 22
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑢 𝑅 𝑣 ) → ( 𝑣 𝑅 𝑢 ↔ ¬ ( 𝑣 < 𝑢 ∨ 𝑢 < 𝑣 ) ) ) |
24 |
13 19 23
|
3bitr4d |
⊢ ( ( 𝜑 ∧ 𝑢 𝑅 𝑣 ) → ( 𝑢 𝑅 𝑣 ↔ 𝑣 𝑅 𝑢 ) ) |
25 |
10 24
|
mpbid |
⊢ ( ( 𝜑 ∧ 𝑢 𝑅 𝑣 ) → 𝑣 𝑅 𝑢 ) |
26 |
|
simprl |
⊢ ( ( 𝜑 ∧ ( 𝑢 𝑅 𝑣 ∧ 𝑣 𝑅 𝑤 ) ) → 𝑢 𝑅 𝑣 ) |
27 |
14
|
ad2antrl |
⊢ ( ( 𝜑 ∧ ( 𝑢 𝑅 𝑣 ∧ 𝑣 𝑅 𝑤 ) ) → 𝑢 ( 𝑋 × 𝑋 ) 𝑣 ) |
28 |
16
|
simplbi |
⊢ ( 𝑢 ( 𝑋 × 𝑋 ) 𝑣 → 𝑢 ∈ 𝑋 ) |
29 |
27 28
|
syl |
⊢ ( ( 𝜑 ∧ ( 𝑢 𝑅 𝑣 ∧ 𝑣 𝑅 𝑤 ) ) → 𝑢 ∈ 𝑋 ) |
30 |
16
|
simprbi |
⊢ ( 𝑢 ( 𝑋 × 𝑋 ) 𝑣 → 𝑣 ∈ 𝑋 ) |
31 |
27 30
|
syl |
⊢ ( ( 𝜑 ∧ ( 𝑢 𝑅 𝑣 ∧ 𝑣 𝑅 𝑤 ) ) → 𝑣 ∈ 𝑋 ) |
32 |
29 31 18
|
syl2anc |
⊢ ( ( 𝜑 ∧ ( 𝑢 𝑅 𝑣 ∧ 𝑣 𝑅 𝑤 ) ) → ( 𝑢 𝑅 𝑣 ↔ ¬ ( 𝑢 < 𝑣 ∨ 𝑣 < 𝑢 ) ) ) |
33 |
26 32
|
mpbid |
⊢ ( ( 𝜑 ∧ ( 𝑢 𝑅 𝑣 ∧ 𝑣 𝑅 𝑤 ) ) → ¬ ( 𝑢 < 𝑣 ∨ 𝑣 < 𝑢 ) ) |
34 |
|
simprr |
⊢ ( ( 𝜑 ∧ ( 𝑢 𝑅 𝑣 ∧ 𝑣 𝑅 𝑤 ) ) → 𝑣 𝑅 𝑤 ) |
35 |
5
|
brel |
⊢ ( 𝑣 𝑅 𝑤 → ( 𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) |
36 |
35
|
simprd |
⊢ ( 𝑣 𝑅 𝑤 → 𝑤 ∈ 𝑋 ) |
37 |
34 36
|
syl |
⊢ ( ( 𝜑 ∧ ( 𝑢 𝑅 𝑣 ∧ 𝑣 𝑅 𝑤 ) ) → 𝑤 ∈ 𝑋 ) |
38 |
1
|
brdifun |
⊢ ( ( 𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) → ( 𝑣 𝑅 𝑤 ↔ ¬ ( 𝑣 < 𝑤 ∨ 𝑤 < 𝑣 ) ) ) |
39 |
31 37 38
|
syl2anc |
⊢ ( ( 𝜑 ∧ ( 𝑢 𝑅 𝑣 ∧ 𝑣 𝑅 𝑤 ) ) → ( 𝑣 𝑅 𝑤 ↔ ¬ ( 𝑣 < 𝑤 ∨ 𝑤 < 𝑣 ) ) ) |
40 |
34 39
|
mpbid |
⊢ ( ( 𝜑 ∧ ( 𝑢 𝑅 𝑣 ∧ 𝑣 𝑅 𝑤 ) ) → ¬ ( 𝑣 < 𝑤 ∨ 𝑤 < 𝑣 ) ) |
41 |
|
simpl |
⊢ ( ( 𝜑 ∧ ( 𝑢 𝑅 𝑣 ∧ 𝑣 𝑅 𝑤 ) ) → 𝜑 ) |
42 |
3
|
swopolem |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋 ) ) → ( 𝑢 < 𝑤 → ( 𝑢 < 𝑣 ∨ 𝑣 < 𝑤 ) ) ) |
43 |
41 29 37 31 42
|
syl13anc |
⊢ ( ( 𝜑 ∧ ( 𝑢 𝑅 𝑣 ∧ 𝑣 𝑅 𝑤 ) ) → ( 𝑢 < 𝑤 → ( 𝑢 < 𝑣 ∨ 𝑣 < 𝑤 ) ) ) |
44 |
3
|
swopolem |
⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋 ) ) → ( 𝑤 < 𝑢 → ( 𝑤 < 𝑣 ∨ 𝑣 < 𝑢 ) ) ) |
45 |
41 37 29 31 44
|
syl13anc |
⊢ ( ( 𝜑 ∧ ( 𝑢 𝑅 𝑣 ∧ 𝑣 𝑅 𝑤 ) ) → ( 𝑤 < 𝑢 → ( 𝑤 < 𝑣 ∨ 𝑣 < 𝑢 ) ) ) |
46 |
|
orcom |
⊢ ( ( 𝑣 < 𝑢 ∨ 𝑤 < 𝑣 ) ↔ ( 𝑤 < 𝑣 ∨ 𝑣 < 𝑢 ) ) |
47 |
45 46
|
syl6ibr |
⊢ ( ( 𝜑 ∧ ( 𝑢 𝑅 𝑣 ∧ 𝑣 𝑅 𝑤 ) ) → ( 𝑤 < 𝑢 → ( 𝑣 < 𝑢 ∨ 𝑤 < 𝑣 ) ) ) |
48 |
43 47
|
orim12d |
⊢ ( ( 𝜑 ∧ ( 𝑢 𝑅 𝑣 ∧ 𝑣 𝑅 𝑤 ) ) → ( ( 𝑢 < 𝑤 ∨ 𝑤 < 𝑢 ) → ( ( 𝑢 < 𝑣 ∨ 𝑣 < 𝑤 ) ∨ ( 𝑣 < 𝑢 ∨ 𝑤 < 𝑣 ) ) ) ) |
49 |
|
or4 |
⊢ ( ( ( 𝑢 < 𝑣 ∨ 𝑣 < 𝑤 ) ∨ ( 𝑣 < 𝑢 ∨ 𝑤 < 𝑣 ) ) ↔ ( ( 𝑢 < 𝑣 ∨ 𝑣 < 𝑢 ) ∨ ( 𝑣 < 𝑤 ∨ 𝑤 < 𝑣 ) ) ) |
50 |
48 49
|
syl6ib |
⊢ ( ( 𝜑 ∧ ( 𝑢 𝑅 𝑣 ∧ 𝑣 𝑅 𝑤 ) ) → ( ( 𝑢 < 𝑤 ∨ 𝑤 < 𝑢 ) → ( ( 𝑢 < 𝑣 ∨ 𝑣 < 𝑢 ) ∨ ( 𝑣 < 𝑤 ∨ 𝑤 < 𝑣 ) ) ) ) |
51 |
33 40 50
|
mtord |
⊢ ( ( 𝜑 ∧ ( 𝑢 𝑅 𝑣 ∧ 𝑣 𝑅 𝑤 ) ) → ¬ ( 𝑢 < 𝑤 ∨ 𝑤 < 𝑢 ) ) |
52 |
1
|
brdifun |
⊢ ( ( 𝑢 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) → ( 𝑢 𝑅 𝑤 ↔ ¬ ( 𝑢 < 𝑤 ∨ 𝑤 < 𝑢 ) ) ) |
53 |
29 37 52
|
syl2anc |
⊢ ( ( 𝜑 ∧ ( 𝑢 𝑅 𝑣 ∧ 𝑣 𝑅 𝑤 ) ) → ( 𝑢 𝑅 𝑤 ↔ ¬ ( 𝑢 < 𝑤 ∨ 𝑤 < 𝑢 ) ) ) |
54 |
51 53
|
mpbird |
⊢ ( ( 𝜑 ∧ ( 𝑢 𝑅 𝑣 ∧ 𝑣 𝑅 𝑤 ) ) → 𝑢 𝑅 𝑤 ) |
55 |
2 3
|
swopo |
⊢ ( 𝜑 → < Po 𝑋 ) |
56 |
|
poirr |
⊢ ( ( < Po 𝑋 ∧ 𝑢 ∈ 𝑋 ) → ¬ 𝑢 < 𝑢 ) |
57 |
55 56
|
sylan |
⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑋 ) → ¬ 𝑢 < 𝑢 ) |
58 |
|
pm1.2 |
⊢ ( ( 𝑢 < 𝑢 ∨ 𝑢 < 𝑢 ) → 𝑢 < 𝑢 ) |
59 |
57 58
|
nsyl |
⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑋 ) → ¬ ( 𝑢 < 𝑢 ∨ 𝑢 < 𝑢 ) ) |
60 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑋 ) → 𝑢 ∈ 𝑋 ) |
61 |
1
|
brdifun |
⊢ ( ( 𝑢 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋 ) → ( 𝑢 𝑅 𝑢 ↔ ¬ ( 𝑢 < 𝑢 ∨ 𝑢 < 𝑢 ) ) ) |
62 |
60 60 61
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑋 ) → ( 𝑢 𝑅 𝑢 ↔ ¬ ( 𝑢 < 𝑢 ∨ 𝑢 < 𝑢 ) ) ) |
63 |
59 62
|
mpbird |
⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑋 ) → 𝑢 𝑅 𝑢 ) |
64 |
5
|
ssbri |
⊢ ( 𝑢 𝑅 𝑢 → 𝑢 ( 𝑋 × 𝑋 ) 𝑢 ) |
65 |
|
brxp |
⊢ ( 𝑢 ( 𝑋 × 𝑋 ) 𝑢 ↔ ( 𝑢 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋 ) ) |
66 |
65
|
simplbi |
⊢ ( 𝑢 ( 𝑋 × 𝑋 ) 𝑢 → 𝑢 ∈ 𝑋 ) |
67 |
64 66
|
syl |
⊢ ( 𝑢 𝑅 𝑢 → 𝑢 ∈ 𝑋 ) |
68 |
67
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑢 𝑅 𝑢 ) → 𝑢 ∈ 𝑋 ) |
69 |
63 68
|
impbida |
⊢ ( 𝜑 → ( 𝑢 ∈ 𝑋 ↔ 𝑢 𝑅 𝑢 ) ) |
70 |
9 25 54 69
|
iserd |
⊢ ( 𝜑 → 𝑅 Er 𝑋 ) |