Step | Hyp | Ref
| Expression |
1 | | opsrtoslem.d |
. . . . . . . 8
⊢ 𝐷 = {ℎ ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} |
2 | | ovex 6678 |
. . . . . . . 8
⊢
(ℕ0 ↑𝑚 𝐼) ∈ V |
3 | 1, 2 | rabex2 4815 |
. . . . . . 7
⊢ 𝐷 ∈ V |
4 | | opsrtoslem.c |
. . . . . . . 8
⊢ 𝐶 = (𝑇 <bag 𝐼) |
5 | | opsrso.i |
. . . . . . . 8
⊢ (𝜑 → 𝐼 ∈ 𝑉) |
6 | | xpexg 6960 |
. . . . . . . . . 10
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐼 ∈ 𝑉) → (𝐼 × 𝐼) ∈ V) |
7 | 5, 5, 6 | syl2anc 693 |
. . . . . . . . 9
⊢ (𝜑 → (𝐼 × 𝐼) ∈ V) |
8 | | opsrso.t |
. . . . . . . . 9
⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼)) |
9 | 7, 8 | ssexd 4805 |
. . . . . . . 8
⊢ (𝜑 → 𝑇 ∈ V) |
10 | | opsrso.w |
. . . . . . . 8
⊢ (𝜑 → 𝑇 We 𝐼) |
11 | 4, 1, 5, 9, 10 | ltbwe 19472 |
. . . . . . 7
⊢ (𝜑 → 𝐶 We 𝐷) |
12 | | opsrso.r |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 ∈ Toset) |
13 | | eqid 2622 |
. . . . . . . . . . 11
⊢
(Base‘𝑅) =
(Base‘𝑅) |
14 | | eqid 2622 |
. . . . . . . . . . 11
⊢
(le‘𝑅) =
(le‘𝑅) |
15 | | opsrtoslem.q |
. . . . . . . . . . 11
⊢ < =
(lt‘𝑅) |
16 | 13, 14, 15 | tosso 17036 |
. . . . . . . . . 10
⊢ (𝑅 ∈ Toset → (𝑅 ∈ Toset ↔ ( < Or
(Base‘𝑅) ∧ ( I
↾ (Base‘𝑅))
⊆ (le‘𝑅)))) |
17 | 16 | ibi 256 |
. . . . . . . . 9
⊢ (𝑅 ∈ Toset → ( < Or
(Base‘𝑅) ∧ ( I
↾ (Base‘𝑅))
⊆ (le‘𝑅))) |
18 | 12, 17 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ( < Or (Base‘𝑅) ∧ ( I ↾
(Base‘𝑅)) ⊆
(le‘𝑅))) |
19 | 18 | simpld 475 |
. . . . . . 7
⊢ (𝜑 → < Or (Base‘𝑅)) |
20 | | opsrtoslem.ps |
. . . . . . . . 9
⊢ (𝜓 ↔ ∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤𝐶𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))) |
21 | 20 | opabbii 4717 |
. . . . . . . 8
⊢
{〈𝑥, 𝑦〉 ∣ 𝜓} = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤𝐶𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))} |
22 | 21 | wemapso 8456 |
. . . . . . 7
⊢ ((𝐷 ∈ V ∧ 𝐶 We 𝐷 ∧ < Or (Base‘𝑅)) → {〈𝑥, 𝑦〉 ∣ 𝜓} Or ((Base‘𝑅) ↑𝑚 𝐷)) |
23 | 3, 11, 19, 22 | mp3an2i 1429 |
. . . . . 6
⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ 𝜓} Or ((Base‘𝑅) ↑𝑚 𝐷)) |
24 | | opsrtoslem.s |
. . . . . . . 8
⊢ 𝑆 = (𝐼 mPwSer 𝑅) |
25 | | opsrtoslem.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝑆) |
26 | 24, 13, 1, 25, 5 | psrbas 19378 |
. . . . . . 7
⊢ (𝜑 → 𝐵 = ((Base‘𝑅) ↑𝑚 𝐷)) |
27 | | soeq2 5055 |
. . . . . . 7
⊢ (𝐵 = ((Base‘𝑅) ↑𝑚
𝐷) → ({〈𝑥, 𝑦〉 ∣ 𝜓} Or 𝐵 ↔ {〈𝑥, 𝑦〉 ∣ 𝜓} Or ((Base‘𝑅) ↑𝑚 𝐷))) |
28 | 26, 27 | syl 17 |
. . . . . 6
⊢ (𝜑 → ({〈𝑥, 𝑦〉 ∣ 𝜓} Or 𝐵 ↔ {〈𝑥, 𝑦〉 ∣ 𝜓} Or ((Base‘𝑅) ↑𝑚 𝐷))) |
29 | 23, 28 | mpbird 247 |
. . . . 5
⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ 𝜓} Or 𝐵) |
30 | | soinxp 5183 |
. . . . 5
⊢
({〈𝑥, 𝑦〉 ∣ 𝜓} Or 𝐵 ↔ ({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) Or 𝐵) |
31 | 29, 30 | sylib 208 |
. . . 4
⊢ (𝜑 → ({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) Or 𝐵) |
32 | | opsrso.o |
. . . . . . . 8
⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇) |
33 | | fvex 6201 |
. . . . . . . 8
⊢ ((𝐼 ordPwSer 𝑅)‘𝑇) ∈ V |
34 | 32, 33 | eqeltri 2697 |
. . . . . . 7
⊢ 𝑂 ∈ V |
35 | | opsrtoslem.l |
. . . . . . . 8
⊢ ≤ =
(le‘𝑂) |
36 | | eqid 2622 |
. . . . . . . 8
⊢
(lt‘𝑂) =
(lt‘𝑂) |
37 | 35, 36 | pltfval 16959 |
. . . . . . 7
⊢ (𝑂 ∈ V → (lt‘𝑂) = ( ≤ ∖ I
)) |
38 | 34, 37 | ax-mp 5 |
. . . . . 6
⊢
(lt‘𝑂) = (
≤
∖ I ) |
39 | | difundir 3880 |
. . . . . . . 8
⊢
((({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∪ ( I ↾ 𝐵)) ∖ I ) = ((({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∖ I ) ∪ (( I ↾ 𝐵) ∖ I )) |
40 | | resss 5422 |
. . . . . . . . . 10
⊢ ( I
↾ 𝐵) ⊆
I |
41 | | ssdif0 3942 |
. . . . . . . . . 10
⊢ (( I
↾ 𝐵) ⊆ I ↔
(( I ↾ 𝐵) ∖ I )
= ∅) |
42 | 40, 41 | mpbi 220 |
. . . . . . . . 9
⊢ (( I
↾ 𝐵) ∖ I ) =
∅ |
43 | 42 | uneq2i 3764 |
. . . . . . . 8
⊢
((({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∖ I ) ∪ (( I ↾ 𝐵) ∖ I )) = ((({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∖ I ) ∪
∅) |
44 | | un0 3967 |
. . . . . . . 8
⊢
((({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∖ I ) ∪ ∅) =
(({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∖ I ) |
45 | 39, 43, 44 | 3eqtri 2648 |
. . . . . . 7
⊢
((({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∪ ( I ↾ 𝐵)) ∖ I ) = (({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∖ I ) |
46 | 32, 5, 12, 8, 10, 24, 25, 15, 4, 1, 20, 35 | opsrtoslem1 19484 |
. . . . . . . 8
⊢ (𝜑 → ≤ = (({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∪ ( I ↾ 𝐵))) |
47 | 46 | difeq1d 3727 |
. . . . . . 7
⊢ (𝜑 → ( ≤ ∖ I ) =
((({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∪ ( I ↾ 𝐵)) ∖ I )) |
48 | | inss2 3834 |
. . . . . . . . . . . 12
⊢
({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) ⊆ (𝐵 × 𝐵) |
49 | | relxp 5227 |
. . . . . . . . . . . 12
⊢ Rel
(𝐵 × 𝐵) |
50 | | relss 5206 |
. . . . . . . . . . . 12
⊢
(({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) ⊆ (𝐵 × 𝐵) → (Rel (𝐵 × 𝐵) → Rel ({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)))) |
51 | 48, 49, 50 | mp2 9 |
. . . . . . . . . . 11
⊢ Rel
({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) |
52 | 51 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → Rel ({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵))) |
53 | | df-br 4654 |
. . . . . . . . . . . . . 14
⊢ (𝑎 I 𝑏 ↔ 〈𝑎, 𝑏〉 ∈ I ) |
54 | | vex 3203 |
. . . . . . . . . . . . . . 15
⊢ 𝑏 ∈ V |
55 | 54 | ideq 5274 |
. . . . . . . . . . . . . 14
⊢ (𝑎 I 𝑏 ↔ 𝑎 = 𝑏) |
56 | 53, 55 | bitr3i 266 |
. . . . . . . . . . . . 13
⊢
(〈𝑎, 𝑏〉 ∈ I ↔ 𝑎 = 𝑏) |
57 | | brin 4704 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵))𝑎 ↔ (𝑎{〈𝑥, 𝑦〉 ∣ 𝜓}𝑎 ∧ 𝑎(𝐵 × 𝐵)𝑎)) |
58 | 57 | simprbi 480 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵))𝑎 → 𝑎(𝐵 × 𝐵)𝑎) |
59 | | brxp 5147 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎(𝐵 × 𝐵)𝑎 ↔ (𝑎 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵)) |
60 | 59 | simprbi 480 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎(𝐵 × 𝐵)𝑎 → 𝑎 ∈ 𝐵) |
61 | 58, 60 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵))𝑎 → 𝑎 ∈ 𝐵) |
62 | | sonr 5056 |
. . . . . . . . . . . . . . . . 17
⊢
((({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) Or 𝐵 ∧ 𝑎 ∈ 𝐵) → ¬ 𝑎({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵))𝑎) |
63 | 62 | ex 450 |
. . . . . . . . . . . . . . . 16
⊢
(({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) Or 𝐵 → (𝑎 ∈ 𝐵 → ¬ 𝑎({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵))𝑎)) |
64 | 31, 61, 63 | syl2im 40 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑎({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵))𝑎 → ¬ 𝑎({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵))𝑎)) |
65 | 64 | pm2.01d 181 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ¬ 𝑎({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵))𝑎) |
66 | | breq2 4657 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = 𝑏 → (𝑎({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵))𝑎 ↔ 𝑎({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵))𝑏)) |
67 | | df-br 4654 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵))𝑏 ↔ 〈𝑎, 𝑏〉 ∈ ({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵))) |
68 | 66, 67 | syl6bb 276 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = 𝑏 → (𝑎({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵))𝑎 ↔ 〈𝑎, 𝑏〉 ∈ ({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)))) |
69 | 68 | notbid 308 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = 𝑏 → (¬ 𝑎({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵))𝑎 ↔ ¬ 〈𝑎, 𝑏〉 ∈ ({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)))) |
70 | 65, 69 | syl5ibcom 235 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑎 = 𝑏 → ¬ 〈𝑎, 𝑏〉 ∈ ({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)))) |
71 | 56, 70 | syl5bi 232 |
. . . . . . . . . . . 12
⊢ (𝜑 → (〈𝑎, 𝑏〉 ∈ I → ¬ 〈𝑎, 𝑏〉 ∈ ({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)))) |
72 | 71 | con2d 129 |
. . . . . . . . . . 11
⊢ (𝜑 → (〈𝑎, 𝑏〉 ∈ ({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) → ¬ 〈𝑎, 𝑏〉 ∈ I )) |
73 | | opex 4932 |
. . . . . . . . . . . 12
⊢
〈𝑎, 𝑏〉 ∈ V |
74 | | eldif 3584 |
. . . . . . . . . . . 12
⊢
(〈𝑎, 𝑏〉 ∈ (V ∖ I )
↔ (〈𝑎, 𝑏〉 ∈ V ∧ ¬
〈𝑎, 𝑏〉 ∈ I )) |
75 | 73, 74 | mpbiran 953 |
. . . . . . . . . . 11
⊢
(〈𝑎, 𝑏〉 ∈ (V ∖ I )
↔ ¬ 〈𝑎, 𝑏〉 ∈ I
) |
76 | 72, 75 | syl6ibr 242 |
. . . . . . . . . 10
⊢ (𝜑 → (〈𝑎, 𝑏〉 ∈ ({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) → 〈𝑎, 𝑏〉 ∈ (V ∖ I
))) |
77 | 52, 76 | relssdv 5212 |
. . . . . . . . 9
⊢ (𝜑 → ({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) ⊆ (V ∖ I )) |
78 | | disj2 4024 |
. . . . . . . . 9
⊢
((({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∩ I ) = ∅ ↔ ({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) ⊆ (V ∖ I )) |
79 | 77, 78 | sylibr 224 |
. . . . . . . 8
⊢ (𝜑 → (({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∩ I ) = ∅) |
80 | | disj3 4021 |
. . . . . . . 8
⊢
((({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∩ I ) = ∅ ↔ ({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) = (({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∖ I )) |
81 | 79, 80 | sylib 208 |
. . . . . . 7
⊢ (𝜑 → ({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) = (({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∖ I )) |
82 | 45, 47, 81 | 3eqtr4a 2682 |
. . . . . 6
⊢ (𝜑 → ( ≤ ∖ I ) =
({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵))) |
83 | 38, 82 | syl5eq 2668 |
. . . . 5
⊢ (𝜑 → (lt‘𝑂) = ({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵))) |
84 | | soeq1 5054 |
. . . . 5
⊢
((lt‘𝑂) =
({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) → ((lt‘𝑂) Or 𝐵 ↔ ({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) Or 𝐵)) |
85 | 83, 84 | syl 17 |
. . . 4
⊢ (𝜑 → ((lt‘𝑂) Or 𝐵 ↔ ({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) Or 𝐵)) |
86 | 31, 85 | mpbird 247 |
. . 3
⊢ (𝜑 → (lt‘𝑂) Or 𝐵) |
87 | 24, 32, 8 | opsrbas 19479 |
. . . . 5
⊢ (𝜑 → (Base‘𝑆) = (Base‘𝑂)) |
88 | 25, 87 | syl5eq 2668 |
. . . 4
⊢ (𝜑 → 𝐵 = (Base‘𝑂)) |
89 | | soeq2 5055 |
. . . 4
⊢ (𝐵 = (Base‘𝑂) → ((lt‘𝑂) Or 𝐵 ↔ (lt‘𝑂) Or (Base‘𝑂))) |
90 | 88, 89 | syl 17 |
. . 3
⊢ (𝜑 → ((lt‘𝑂) Or 𝐵 ↔ (lt‘𝑂) Or (Base‘𝑂))) |
91 | 86, 90 | mpbid 222 |
. 2
⊢ (𝜑 → (lt‘𝑂) Or (Base‘𝑂)) |
92 | 88 | reseq2d 5396 |
. . . 4
⊢ (𝜑 → ( I ↾ 𝐵) = ( I ↾
(Base‘𝑂))) |
93 | | ssun2 3777 |
. . . 4
⊢ ( I
↾ 𝐵) ⊆
(({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∪ ( I ↾ 𝐵)) |
94 | 92, 93 | syl6eqssr 3656 |
. . 3
⊢ (𝜑 → ( I ↾
(Base‘𝑂)) ⊆
(({〈𝑥, 𝑦〉 ∣ 𝜓} ∩ (𝐵 × 𝐵)) ∪ ( I ↾ 𝐵))) |
95 | 94, 46 | sseqtr4d 3642 |
. 2
⊢ (𝜑 → ( I ↾
(Base‘𝑂)) ⊆
≤
) |
96 | | eqid 2622 |
. . . 4
⊢
(Base‘𝑂) =
(Base‘𝑂) |
97 | 96, 35, 36 | tosso 17036 |
. . 3
⊢ (𝑂 ∈ V → (𝑂 ∈ Toset ↔
((lt‘𝑂) Or
(Base‘𝑂) ∧ ( I
↾ (Base‘𝑂))
⊆ ≤ ))) |
98 | 34, 97 | ax-mp 5 |
. 2
⊢ (𝑂 ∈ Toset ↔
((lt‘𝑂) Or
(Base‘𝑂) ∧ ( I
↾ (Base‘𝑂))
⊆ ≤ )) |
99 | 91, 95, 98 | sylanbrc 698 |
1
⊢ (𝜑 → 𝑂 ∈ Toset) |