Step | Hyp | Ref
| Expression |
1 | | opsrtoslem.d |
. . . . . . . 8
⊢ 𝐷 = {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} |
2 | | ovex 7191 |
. . . . . . . 8
⊢
(ℕ0 ↑m 𝐼) ∈ V |
3 | 1, 2 | rabex2 5239 |
. . . . . . 7
⊢ 𝐷 ∈ V |
4 | | opsrtoslem.c |
. . . . . . . 8
⊢ 𝐶 = (𝑇 <bag 𝐼) |
5 | | opsrso.i |
. . . . . . . 8
⊢ (𝜑 → 𝐼 ∈ 𝑉) |
6 | 5, 5 | xpexd 7476 |
. . . . . . . . 9
⊢ (𝜑 → (𝐼 × 𝐼) ∈ V) |
7 | | opsrso.t |
. . . . . . . . 9
⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼)) |
8 | 6, 7 | ssexd 5230 |
. . . . . . . 8
⊢ (𝜑 → 𝑇 ∈ V) |
9 | | opsrso.w |
. . . . . . . 8
⊢ (𝜑 → 𝑇 We 𝐼) |
10 | 4, 1, 5, 8, 9 | ltbwe 20255 |
. . . . . . 7
⊢ (𝜑 → 𝐶 We 𝐷) |
11 | | opsrso.r |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 ∈ Toset) |
12 | | eqid 2823 |
. . . . . . . . . . 11
⊢
(Base‘𝑅) =
(Base‘𝑅) |
13 | | eqid 2823 |
. . . . . . . . . . 11
⊢
(le‘𝑅) =
(le‘𝑅) |
14 | | opsrtoslem.q |
. . . . . . . . . . 11
⊢ < =
(lt‘𝑅) |
15 | 12, 13, 14 | tosso 17648 |
. . . . . . . . . 10
⊢ (𝑅 ∈ Toset → (𝑅 ∈ Toset ↔ ( < Or
(Base‘𝑅) ∧ ( I
↾ (Base‘𝑅))
⊆ (le‘𝑅)))) |
16 | 15 | ibi 269 |
. . . . . . . . 9
⊢ (𝑅 ∈ Toset → ( < Or
(Base‘𝑅) ∧ ( I
↾ (Base‘𝑅))
⊆ (le‘𝑅))) |
17 | 11, 16 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ( < Or (Base‘𝑅) ∧ ( I ↾
(Base‘𝑅)) ⊆
(le‘𝑅))) |
18 | 17 | simpld 497 |
. . . . . . 7
⊢ (𝜑 → < Or (Base‘𝑅)) |
19 | | opsrtoslem.ps |
. . . . . . . . 9
⊢ (𝜓 ↔ ∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤𝐶𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))) |
20 | 19 | opabbii 5135 |
. . . . . . . 8
⊢
{〈𝑥, 𝑦〉 ∣ 𝜓} = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤𝐶𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))} |
21 | 20 | wemapso 9017 |
. . . . . . 7
⊢ ((𝐷 ∈ V ∧ 𝐶 We 𝐷 ∧ < Or (Base‘𝑅)) → {〈𝑥, 𝑦〉 ∣ 𝜓} Or ((Base‘𝑅) ↑m 𝐷)) |
22 | 3, 10, 18, 21 | mp3an2i 1462 |
. . . . . 6
⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ 𝜓} Or ((Base‘𝑅) ↑m 𝐷)) |
23 | | opsrtoslem.s |
. . . . . . . 8
⊢ 𝑆 = (𝐼 mPwSer 𝑅) |
24 | | opsrtoslem.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝑆) |
25 | 23, 12, 1, 24, 5 | psrbas 20160 |
. . . . . . 7
⊢ (𝜑 → 𝐵 = ((Base‘𝑅) ↑m 𝐷)) |
26 | | soeq2 5497 |
. . . . . . 7
⊢ (𝐵 = ((Base‘𝑅) ↑m 𝐷) → ({〈𝑥, 𝑦〉 ∣ 𝜓} Or 𝐵 ↔ {〈𝑥, 𝑦〉 ∣ 𝜓} Or ((Base‘𝑅) ↑m 𝐷))) |
27 | 25, 26 | syl 17 |
. . . . . 6
⊢ (𝜑 → ({〈𝑥, 𝑦〉 ∣ 𝜓} Or 𝐵 ↔ {〈𝑥, 𝑦〉 ∣ 𝜓} Or ((Base‘𝑅) ↑m 𝐷))) |
28 | 22, 27 | mpbird 259 |
. . . . 5
⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ 𝜓} Or 𝐵) |
29 | | soinxp 5635 |
. . . . 5
⊢
({〈𝑥, 𝑦〉 ∣ 𝜓} Or 𝐵 ↔ ({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) Or 𝐵) |
30 | 28, 29 | sylib 220 |
. . . 4
⊢ (𝜑 → ({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) Or 𝐵) |
31 | | opsrso.o |
. . . . . . . 8
⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇) |
32 | 31 | fvexi 6686 |
. . . . . . 7
⊢ 𝑂 ∈ V |
33 | | opsrtoslem.l |
. . . . . . . 8
⊢ ≤ =
(le‘𝑂) |
34 | | eqid 2823 |
. . . . . . . 8
⊢
(lt‘𝑂) =
(lt‘𝑂) |
35 | 33, 34 | pltfval 17571 |
. . . . . . 7
⊢ (𝑂 ∈ V → (lt‘𝑂) = ( ≤ ∖ I
)) |
36 | 32, 35 | ax-mp 5 |
. . . . . 6
⊢
(lt‘𝑂) = (
≤
∖ I ) |
37 | | difundir 4259 |
. . . . . . . 8
⊢
((({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∪ ( I ↾ 𝐵)) ∖ I ) = ((({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∖ I ) ∪ (( I ↾ 𝐵) ∖ I )) |
38 | | resss 5880 |
. . . . . . . . . 10
⊢ ( I
↾ 𝐵) ⊆
I |
39 | | ssdif0 4325 |
. . . . . . . . . 10
⊢ (( I
↾ 𝐵) ⊆ I ↔
(( I ↾ 𝐵) ∖ I )
= ∅) |
40 | 38, 39 | mpbi 232 |
. . . . . . . . 9
⊢ (( I
↾ 𝐵) ∖ I ) =
∅ |
41 | 40 | uneq2i 4138 |
. . . . . . . 8
⊢
((({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∖ I ) ∪ (( I ↾ 𝐵) ∖ I )) = ((({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∖ I ) ∪
∅) |
42 | | un0 4346 |
. . . . . . . 8
⊢
((({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∖ I ) ∪ ∅) =
(({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∖ I ) |
43 | 37, 41, 42 | 3eqtri 2850 |
. . . . . . 7
⊢
((({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∪ ( I ↾ 𝐵)) ∖ I ) = (({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∖ I ) |
44 | 31, 5, 11, 7, 9, 23, 24, 14, 4, 1, 19, 33 | opsrtoslem1 20266 |
. . . . . . . 8
⊢ (𝜑 → ≤ = (({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∪ ( I ↾ 𝐵))) |
45 | 44 | difeq1d 4100 |
. . . . . . 7
⊢ (𝜑 → ( ≤ ∖ I ) =
((({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∪ ( I ↾ 𝐵)) ∖ I )) |
46 | | relinxp 5689 |
. . . . . . . . . . 11
⊢ Rel
({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) |
47 | 46 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → Rel ({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵))) |
48 | | df-br 5069 |
. . . . . . . . . . . . . 14
⊢ (𝑎 I 𝑏 ↔ 〈𝑎, 𝑏〉 ∈ I ) |
49 | | vex 3499 |
. . . . . . . . . . . . . . 15
⊢ 𝑏 ∈ V |
50 | 49 | ideq 5725 |
. . . . . . . . . . . . . 14
⊢ (𝑎 I 𝑏 ↔ 𝑎 = 𝑏) |
51 | 48, 50 | bitr3i 279 |
. . . . . . . . . . . . 13
⊢
(〈𝑎, 𝑏〉 ∈ I ↔ 𝑎 = 𝑏) |
52 | | brin 5120 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵))𝑎 ↔ (𝑎{〈𝑥, 𝑦〉 ∣ 𝜓}𝑎 ∧ 𝑎(𝐵 × 𝐵)𝑎)) |
53 | 52 | simprbi 499 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵))𝑎 → 𝑎(𝐵 × 𝐵)𝑎) |
54 | | brxp 5603 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎(𝐵 × 𝐵)𝑎 ↔ (𝑎 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵)) |
55 | 54 | simprbi 499 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎(𝐵 × 𝐵)𝑎 → 𝑎 ∈ 𝐵) |
56 | 53, 55 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵))𝑎 → 𝑎 ∈ 𝐵) |
57 | | sonr 5498 |
. . . . . . . . . . . . . . . . 17
⊢
((({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) Or 𝐵 ∧ 𝑎 ∈ 𝐵) → ¬ 𝑎({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵))𝑎) |
58 | 57 | ex 415 |
. . . . . . . . . . . . . . . 16
⊢
(({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) Or 𝐵 → (𝑎 ∈ 𝐵 → ¬ 𝑎({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵))𝑎)) |
59 | 30, 56, 58 | syl2im 40 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑎({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵))𝑎 → ¬ 𝑎({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵))𝑎)) |
60 | 59 | pm2.01d 192 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ¬ 𝑎({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵))𝑎) |
61 | | breq2 5072 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = 𝑏 → (𝑎({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵))𝑎 ↔ 𝑎({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵))𝑏)) |
62 | | df-br 5069 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵))𝑏 ↔ 〈𝑎, 𝑏〉 ∈ ({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵))) |
63 | 61, 62 | syl6bb 289 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = 𝑏 → (𝑎({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵))𝑎 ↔ 〈𝑎, 𝑏〉 ∈ ({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)))) |
64 | 63 | notbid 320 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = 𝑏 → (¬ 𝑎({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵))𝑎 ↔ ¬ 〈𝑎, 𝑏〉 ∈ ({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)))) |
65 | 60, 64 | syl5ibcom 247 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑎 = 𝑏 → ¬ 〈𝑎, 𝑏〉 ∈ ({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)))) |
66 | 51, 65 | syl5bi 244 |
. . . . . . . . . . . 12
⊢ (𝜑 → (〈𝑎, 𝑏〉 ∈ I → ¬ 〈𝑎, 𝑏〉 ∈ ({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)))) |
67 | 66 | con2d 136 |
. . . . . . . . . . 11
⊢ (𝜑 → (〈𝑎, 𝑏〉 ∈ ({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) → ¬ 〈𝑎, 𝑏〉 ∈ I )) |
68 | | opex 5358 |
. . . . . . . . . . . 12
⊢
〈𝑎, 𝑏〉 ∈ V |
69 | | eldif 3948 |
. . . . . . . . . . . 12
⊢
(〈𝑎, 𝑏〉 ∈ (V ∖ I )
↔ (〈𝑎, 𝑏〉 ∈ V ∧ ¬
〈𝑎, 𝑏〉 ∈ I )) |
70 | 68, 69 | mpbiran 707 |
. . . . . . . . . . 11
⊢
(〈𝑎, 𝑏〉 ∈ (V ∖ I )
↔ ¬ 〈𝑎, 𝑏〉 ∈ I
) |
71 | 67, 70 | syl6ibr 254 |
. . . . . . . . . 10
⊢ (𝜑 → (〈𝑎, 𝑏〉 ∈ ({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) → 〈𝑎, 𝑏〉 ∈ (V ∖ I
))) |
72 | 47, 71 | relssdv 5663 |
. . . . . . . . 9
⊢ (𝜑 → ({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) ⊆ (V ∖ I )) |
73 | | disj2 4409 |
. . . . . . . . 9
⊢
((({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∩ I ) = ∅ ↔ ({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) ⊆ (V ∖ I )) |
74 | 72, 73 | sylibr 236 |
. . . . . . . 8
⊢ (𝜑 → (({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∩ I ) = ∅) |
75 | | disj3 4405 |
. . . . . . . 8
⊢
((({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∩ I ) = ∅ ↔ ({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) = (({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∖ I )) |
76 | 74, 75 | sylib 220 |
. . . . . . 7
⊢ (𝜑 → ({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) = (({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∖ I )) |
77 | 43, 45, 76 | 3eqtr4a 2884 |
. . . . . 6
⊢ (𝜑 → ( ≤ ∖ I ) =
({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵))) |
78 | 36, 77 | syl5eq 2870 |
. . . . 5
⊢ (𝜑 → (lt‘𝑂) = ({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵))) |
79 | | soeq1 5496 |
. . . . 5
⊢
((lt‘𝑂) =
({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) → ((lt‘𝑂) Or 𝐵 ↔ ({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) Or 𝐵)) |
80 | 78, 79 | syl 17 |
. . . 4
⊢ (𝜑 → ((lt‘𝑂) Or 𝐵 ↔ ({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) Or 𝐵)) |
81 | 30, 80 | mpbird 259 |
. . 3
⊢ (𝜑 → (lt‘𝑂) Or 𝐵) |
82 | 23, 31, 7 | opsrbas 20261 |
. . . . 5
⊢ (𝜑 → (Base‘𝑆) = (Base‘𝑂)) |
83 | 24, 82 | syl5eq 2870 |
. . . 4
⊢ (𝜑 → 𝐵 = (Base‘𝑂)) |
84 | | soeq2 5497 |
. . . 4
⊢ (𝐵 = (Base‘𝑂) → ((lt‘𝑂) Or 𝐵 ↔ (lt‘𝑂) Or (Base‘𝑂))) |
85 | 83, 84 | syl 17 |
. . 3
⊢ (𝜑 → ((lt‘𝑂) Or 𝐵 ↔ (lt‘𝑂) Or (Base‘𝑂))) |
86 | 81, 85 | mpbid 234 |
. 2
⊢ (𝜑 → (lt‘𝑂) Or (Base‘𝑂)) |
87 | 83 | reseq2d 5855 |
. . . 4
⊢ (𝜑 → ( I ↾ 𝐵) = ( I ↾
(Base‘𝑂))) |
88 | | ssun2 4151 |
. . . 4
⊢ ( I
↾ 𝐵) ⊆
(({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∪ ( I ↾ 𝐵)) |
89 | 87, 88 | eqsstrrdi 4024 |
. . 3
⊢ (𝜑 → ( I ↾
(Base‘𝑂)) ⊆
(({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∪ ( I ↾ 𝐵))) |
90 | 89, 44 | sseqtrrd 4010 |
. 2
⊢ (𝜑 → ( I ↾
(Base‘𝑂)) ⊆
≤
) |
91 | | eqid 2823 |
. . . 4
⊢
(Base‘𝑂) =
(Base‘𝑂) |
92 | 91, 33, 34 | tosso 17648 |
. . 3
⊢ (𝑂 ∈ V → (𝑂 ∈ Toset ↔
((lt‘𝑂) Or
(Base‘𝑂) ∧ ( I
↾ (Base‘𝑂))
⊆ ≤ ))) |
93 | 32, 92 | ax-mp 5 |
. 2
⊢ (𝑂 ∈ Toset ↔
((lt‘𝑂) Or
(Base‘𝑂) ∧ ( I
↾ (Base‘𝑂))
⊆ ≤ )) |
94 | 86, 90, 93 | sylanbrc 585 |
1
⊢ (𝜑 → 𝑂 ∈ Toset) |