Step | Hyp | Ref
| Expression |
1 | | opsrtoslem.d |
. . . . . . . 8
⊢ 𝐷 = {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} |
2 | | ovex 7168 |
. . . . . . . 8
⊢
(ℕ0 ↑m 𝐼) ∈ V |
3 | 1, 2 | rabex2 5201 |
. . . . . . 7
⊢ 𝐷 ∈ V |
4 | | opsrtoslem.c |
. . . . . . . 8
⊢ 𝐶 = (𝑇 <bag 𝐼) |
5 | | opsrso.i |
. . . . . . . 8
⊢ (𝜑 → 𝐼 ∈ 𝑉) |
6 | 5, 5 | xpexd 7454 |
. . . . . . . . 9
⊢ (𝜑 → (𝐼 × 𝐼) ∈ V) |
7 | | opsrso.t |
. . . . . . . . 9
⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼)) |
8 | 6, 7 | ssexd 5192 |
. . . . . . . 8
⊢ (𝜑 → 𝑇 ∈ V) |
9 | | opsrso.w |
. . . . . . . 8
⊢ (𝜑 → 𝑇 We 𝐼) |
10 | 4, 1, 5, 8, 9 | ltbwe 20712 |
. . . . . . 7
⊢ (𝜑 → 𝐶 We 𝐷) |
11 | | opsrso.r |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 ∈ Toset) |
12 | | eqid 2798 |
. . . . . . . . . . 11
⊢
(Base‘𝑅) =
(Base‘𝑅) |
13 | | eqid 2798 |
. . . . . . . . . . 11
⊢
(le‘𝑅) =
(le‘𝑅) |
14 | | opsrtoslem.q |
. . . . . . . . . . 11
⊢ < =
(lt‘𝑅) |
15 | 12, 13, 14 | tosso 17638 |
. . . . . . . . . 10
⊢ (𝑅 ∈ Toset → (𝑅 ∈ Toset ↔ ( < Or
(Base‘𝑅) ∧ ( I
↾ (Base‘𝑅))
⊆ (le‘𝑅)))) |
16 | 15 | ibi 270 |
. . . . . . . . 9
⊢ (𝑅 ∈ Toset → ( < Or
(Base‘𝑅) ∧ ( I
↾ (Base‘𝑅))
⊆ (le‘𝑅))) |
17 | 11, 16 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ( < Or (Base‘𝑅) ∧ ( I ↾
(Base‘𝑅)) ⊆
(le‘𝑅))) |
18 | 17 | simpld 498 |
. . . . . . 7
⊢ (𝜑 → < Or (Base‘𝑅)) |
19 | | opsrtoslem.ps |
. . . . . . . . 9
⊢ (𝜓 ↔ ∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤𝐶𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))) |
20 | 19 | opabbii 5097 |
. . . . . . . 8
⊢
{〈𝑥, 𝑦〉 ∣ 𝜓} = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤𝐶𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))} |
21 | 20 | wemapso 8999 |
. . . . . . 7
⊢ ((𝐷 ∈ V ∧ 𝐶 We 𝐷 ∧ < Or (Base‘𝑅)) → {〈𝑥, 𝑦〉 ∣ 𝜓} Or ((Base‘𝑅) ↑m 𝐷)) |
22 | 3, 10, 18, 21 | mp3an2i 1463 |
. . . . . 6
⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ 𝜓} Or ((Base‘𝑅) ↑m 𝐷)) |
23 | | opsrtoslem.s |
. . . . . . . 8
⊢ 𝑆 = (𝐼 mPwSer 𝑅) |
24 | | opsrtoslem.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝑆) |
25 | 23, 12, 1, 24, 5 | psrbas 20616 |
. . . . . . 7
⊢ (𝜑 → 𝐵 = ((Base‘𝑅) ↑m 𝐷)) |
26 | | soeq2 5459 |
. . . . . . 7
⊢ (𝐵 = ((Base‘𝑅) ↑m 𝐷) → ({〈𝑥, 𝑦〉 ∣ 𝜓} Or 𝐵 ↔ {〈𝑥, 𝑦〉 ∣ 𝜓} Or ((Base‘𝑅) ↑m 𝐷))) |
27 | 25, 26 | syl 17 |
. . . . . 6
⊢ (𝜑 → ({〈𝑥, 𝑦〉 ∣ 𝜓} Or 𝐵 ↔ {〈𝑥, 𝑦〉 ∣ 𝜓} Or ((Base‘𝑅) ↑m 𝐷))) |
28 | 22, 27 | mpbird 260 |
. . . . 5
⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ 𝜓} Or 𝐵) |
29 | | soinxp 5597 |
. . . . 5
⊢
({〈𝑥, 𝑦〉 ∣ 𝜓} Or 𝐵 ↔ ({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) Or 𝐵) |
30 | 28, 29 | sylib 221 |
. . . 4
⊢ (𝜑 → ({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) Or 𝐵) |
31 | | opsrso.o |
. . . . . . . 8
⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇) |
32 | 31 | fvexi 6659 |
. . . . . . 7
⊢ 𝑂 ∈ V |
33 | | opsrtoslem.l |
. . . . . . . 8
⊢ ≤ =
(le‘𝑂) |
34 | | eqid 2798 |
. . . . . . . 8
⊢
(lt‘𝑂) =
(lt‘𝑂) |
35 | 33, 34 | pltfval 17561 |
. . . . . . 7
⊢ (𝑂 ∈ V → (lt‘𝑂) = ( ≤ ∖ I
)) |
36 | 32, 35 | ax-mp 5 |
. . . . . 6
⊢
(lt‘𝑂) = (
≤
∖ I ) |
37 | | difundir 4207 |
. . . . . . . 8
⊢
((({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∪ ( I ↾ 𝐵)) ∖ I ) = ((({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∖ I ) ∪ (( I ↾ 𝐵) ∖ I )) |
38 | | resss 5843 |
. . . . . . . . . 10
⊢ ( I
↾ 𝐵) ⊆
I |
39 | | ssdif0 4277 |
. . . . . . . . . 10
⊢ (( I
↾ 𝐵) ⊆ I ↔
(( I ↾ 𝐵) ∖ I )
= ∅) |
40 | 38, 39 | mpbi 233 |
. . . . . . . . 9
⊢ (( I
↾ 𝐵) ∖ I ) =
∅ |
41 | 40 | uneq2i 4087 |
. . . . . . . 8
⊢
((({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∖ I ) ∪ (( I ↾ 𝐵) ∖ I )) = ((({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∖ I ) ∪
∅) |
42 | | un0 4298 |
. . . . . . . 8
⊢
((({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∖ I ) ∪ ∅) =
(({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∖ I ) |
43 | 37, 41, 42 | 3eqtri 2825 |
. . . . . . 7
⊢
((({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∪ ( I ↾ 𝐵)) ∖ I ) = (({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∖ I ) |
44 | 31, 5, 11, 7, 9, 23, 24, 14, 4, 1, 19, 33 | opsrtoslem1 20723 |
. . . . . . . 8
⊢ (𝜑 → ≤ = (({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∪ ( I ↾ 𝐵))) |
45 | 44 | difeq1d 4049 |
. . . . . . 7
⊢ (𝜑 → ( ≤ ∖ I ) =
((({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∪ ( I ↾ 𝐵)) ∖ I )) |
46 | | relinxp 5651 |
. . . . . . . . . . 11
⊢ Rel
({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) |
47 | 46 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → Rel ({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵))) |
48 | | df-br 5031 |
. . . . . . . . . . . . . 14
⊢ (𝑎 I 𝑏 ↔ 〈𝑎, 𝑏〉 ∈ I ) |
49 | | vex 3444 |
. . . . . . . . . . . . . . 15
⊢ 𝑏 ∈ V |
50 | 49 | ideq 5687 |
. . . . . . . . . . . . . 14
⊢ (𝑎 I 𝑏 ↔ 𝑎 = 𝑏) |
51 | 48, 50 | bitr3i 280 |
. . . . . . . . . . . . 13
⊢
(〈𝑎, 𝑏〉 ∈ I ↔ 𝑎 = 𝑏) |
52 | | brin 5082 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵))𝑎 ↔ (𝑎{〈𝑥, 𝑦〉 ∣ 𝜓}𝑎 ∧ 𝑎(𝐵 × 𝐵)𝑎)) |
53 | 52 | simprbi 500 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵))𝑎 → 𝑎(𝐵 × 𝐵)𝑎) |
54 | | brxp 5565 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎(𝐵 × 𝐵)𝑎 ↔ (𝑎 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵)) |
55 | 54 | simprbi 500 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎(𝐵 × 𝐵)𝑎 → 𝑎 ∈ 𝐵) |
56 | 53, 55 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵))𝑎 → 𝑎 ∈ 𝐵) |
57 | | sonr 5460 |
. . . . . . . . . . . . . . . . 17
⊢
((({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) Or 𝐵 ∧ 𝑎 ∈ 𝐵) → ¬ 𝑎({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵))𝑎) |
58 | 57 | ex 416 |
. . . . . . . . . . . . . . . 16
⊢
(({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) Or 𝐵 → (𝑎 ∈ 𝐵 → ¬ 𝑎({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵))𝑎)) |
59 | 30, 56, 58 | syl2im 40 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑎({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵))𝑎 → ¬ 𝑎({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵))𝑎)) |
60 | 59 | pm2.01d 193 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ¬ 𝑎({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵))𝑎) |
61 | | breq2 5034 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = 𝑏 → (𝑎({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵))𝑎 ↔ 𝑎({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵))𝑏)) |
62 | | df-br 5031 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵))𝑏 ↔ 〈𝑎, 𝑏〉 ∈ ({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵))) |
63 | 61, 62 | syl6bb 290 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = 𝑏 → (𝑎({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵))𝑎 ↔ 〈𝑎, 𝑏〉 ∈ ({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)))) |
64 | 63 | notbid 321 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = 𝑏 → (¬ 𝑎({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵))𝑎 ↔ ¬ 〈𝑎, 𝑏〉 ∈ ({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)))) |
65 | 60, 64 | syl5ibcom 248 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑎 = 𝑏 → ¬ 〈𝑎, 𝑏〉 ∈ ({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)))) |
66 | 51, 65 | syl5bi 245 |
. . . . . . . . . . . 12
⊢ (𝜑 → (〈𝑎, 𝑏〉 ∈ I → ¬ 〈𝑎, 𝑏〉 ∈ ({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)))) |
67 | 66 | con2d 136 |
. . . . . . . . . . 11
⊢ (𝜑 → (〈𝑎, 𝑏〉 ∈ ({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) → ¬ 〈𝑎, 𝑏〉 ∈ I )) |
68 | | opex 5321 |
. . . . . . . . . . . 12
⊢
〈𝑎, 𝑏〉 ∈ V |
69 | | eldif 3891 |
. . . . . . . . . . . 12
⊢
(〈𝑎, 𝑏〉 ∈ (V ∖ I )
↔ (〈𝑎, 𝑏〉 ∈ V ∧ ¬
〈𝑎, 𝑏〉 ∈ I )) |
70 | 68, 69 | mpbiran 708 |
. . . . . . . . . . 11
⊢
(〈𝑎, 𝑏〉 ∈ (V ∖ I )
↔ ¬ 〈𝑎, 𝑏〉 ∈ I
) |
71 | 67, 70 | syl6ibr 255 |
. . . . . . . . . 10
⊢ (𝜑 → (〈𝑎, 𝑏〉 ∈ ({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) → 〈𝑎, 𝑏〉 ∈ (V ∖ I
))) |
72 | 47, 71 | relssdv 5625 |
. . . . . . . . 9
⊢ (𝜑 → ({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) ⊆ (V ∖ I )) |
73 | | disj2 4365 |
. . . . . . . . 9
⊢
((({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∩ I ) = ∅ ↔ ({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) ⊆ (V ∖ I )) |
74 | 72, 73 | sylibr 237 |
. . . . . . . 8
⊢ (𝜑 → (({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∩ I ) = ∅) |
75 | | disj3 4361 |
. . . . . . . 8
⊢
((({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∩ I ) = ∅ ↔ ({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) = (({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∖ I )) |
76 | 74, 75 | sylib 221 |
. . . . . . 7
⊢ (𝜑 → ({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) = (({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∖ I )) |
77 | 43, 45, 76 | 3eqtr4a 2859 |
. . . . . 6
⊢ (𝜑 → ( ≤ ∖ I ) =
({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵))) |
78 | 36, 77 | syl5eq 2845 |
. . . . 5
⊢ (𝜑 → (lt‘𝑂) = ({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵))) |
79 | | soeq1 5458 |
. . . . 5
⊢
((lt‘𝑂) =
({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) → ((lt‘𝑂) Or 𝐵 ↔ ({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) Or 𝐵)) |
80 | 78, 79 | syl 17 |
. . . 4
⊢ (𝜑 → ((lt‘𝑂) Or 𝐵 ↔ ({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) Or 𝐵)) |
81 | 30, 80 | mpbird 260 |
. . 3
⊢ (𝜑 → (lt‘𝑂) Or 𝐵) |
82 | 23, 31, 7 | opsrbas 20718 |
. . . . 5
⊢ (𝜑 → (Base‘𝑆) = (Base‘𝑂)) |
83 | 24, 82 | syl5eq 2845 |
. . . 4
⊢ (𝜑 → 𝐵 = (Base‘𝑂)) |
84 | | soeq2 5459 |
. . . 4
⊢ (𝐵 = (Base‘𝑂) → ((lt‘𝑂) Or 𝐵 ↔ (lt‘𝑂) Or (Base‘𝑂))) |
85 | 83, 84 | syl 17 |
. . 3
⊢ (𝜑 → ((lt‘𝑂) Or 𝐵 ↔ (lt‘𝑂) Or (Base‘𝑂))) |
86 | 81, 85 | mpbid 235 |
. 2
⊢ (𝜑 → (lt‘𝑂) Or (Base‘𝑂)) |
87 | 83 | reseq2d 5818 |
. . . 4
⊢ (𝜑 → ( I ↾ 𝐵) = ( I ↾
(Base‘𝑂))) |
88 | | ssun2 4100 |
. . . 4
⊢ ( I
↾ 𝐵) ⊆
(({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∪ ( I ↾ 𝐵)) |
89 | 87, 88 | eqsstrrdi 3970 |
. . 3
⊢ (𝜑 → ( I ↾
(Base‘𝑂)) ⊆
(({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∪ ( I ↾ 𝐵))) |
90 | 89, 44 | sseqtrrd 3956 |
. 2
⊢ (𝜑 → ( I ↾
(Base‘𝑂)) ⊆
≤
) |
91 | | eqid 2798 |
. . . 4
⊢
(Base‘𝑂) =
(Base‘𝑂) |
92 | 91, 33, 34 | tosso 17638 |
. . 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 586 |
1
⊢ (𝜑 → 𝑂 ∈ Toset) |