Step | Hyp | Ref
| Expression |
1 | | opsrval.o |
. 2
⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇) |
2 | | opsrval.i |
. . . . 5
⊢ (𝜑 → 𝐼 ∈ 𝑉) |
3 | | elex 3429 |
. . . . 5
⊢ (𝐼 ∈ 𝑉 → 𝐼 ∈ V) |
4 | 2, 3 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐼 ∈ V) |
5 | | opsrval.r |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ 𝑊) |
6 | | elex 3429 |
. . . . 5
⊢ (𝑅 ∈ 𝑊 → 𝑅 ∈ V) |
7 | 5, 6 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑅 ∈ V) |
8 | 2, 2 | xpexd 7221 |
. . . . 5
⊢ (𝜑 → (𝐼 × 𝐼) ∈ V) |
9 | | pwexg 5078 |
. . . . 5
⊢ ((𝐼 × 𝐼) ∈ V → 𝒫 (𝐼 × 𝐼) ∈ V) |
10 | | mptexg 6740 |
. . . . 5
⊢
(𝒫 (𝐼
× 𝐼) ∈ V →
(𝑟 ∈ 𝒫 (𝐼 × 𝐼) ↦ (𝑆 sSet 〈(le‘ndx), {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))}〉)) ∈ V) |
11 | 8, 9, 10 | 3syl 18 |
. . . 4
⊢ (𝜑 → (𝑟 ∈ 𝒫 (𝐼 × 𝐼) ↦ (𝑆 sSet 〈(le‘ndx), {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))}〉)) ∈ V) |
12 | | simpl 476 |
. . . . . . . 8
⊢ ((𝑖 = 𝐼 ∧ 𝑠 = 𝑅) → 𝑖 = 𝐼) |
13 | 12 | sqxpeqd 5374 |
. . . . . . 7
⊢ ((𝑖 = 𝐼 ∧ 𝑠 = 𝑅) → (𝑖 × 𝑖) = (𝐼 × 𝐼)) |
14 | 13 | pweqd 4383 |
. . . . . 6
⊢ ((𝑖 = 𝐼 ∧ 𝑠 = 𝑅) → 𝒫 (𝑖 × 𝑖) = 𝒫 (𝐼 × 𝐼)) |
15 | | ovexd 6939 |
. . . . . . 7
⊢ ((𝑖 = 𝐼 ∧ 𝑠 = 𝑅) → (𝑖 mPwSer 𝑠) ∈ V) |
16 | | id 22 |
. . . . . . . . . 10
⊢ (𝑝 = (𝑖 mPwSer 𝑠) → 𝑝 = (𝑖 mPwSer 𝑠)) |
17 | | oveq12 6914 |
. . . . . . . . . 10
⊢ ((𝑖 = 𝐼 ∧ 𝑠 = 𝑅) → (𝑖 mPwSer 𝑠) = (𝐼 mPwSer 𝑅)) |
18 | 16, 17 | sylan9eqr 2883 |
. . . . . . . . 9
⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → 𝑝 = (𝐼 mPwSer 𝑅)) |
19 | | opsrval.s |
. . . . . . . . 9
⊢ 𝑆 = (𝐼 mPwSer 𝑅) |
20 | 18, 19 | syl6eqr 2879 |
. . . . . . . 8
⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → 𝑝 = 𝑆) |
21 | 20 | fveq2d 6437 |
. . . . . . . . . . . . 13
⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → (Base‘𝑝) = (Base‘𝑆)) |
22 | | opsrval.b |
. . . . . . . . . . . . 13
⊢ 𝐵 = (Base‘𝑆) |
23 | 21, 22 | syl6eqr 2879 |
. . . . . . . . . . . 12
⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → (Base‘𝑝) = 𝐵) |
24 | 23 | sseq2d 3858 |
. . . . . . . . . . 11
⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → ({𝑥, 𝑦} ⊆ (Base‘𝑝) ↔ {𝑥, 𝑦} ⊆ 𝐵)) |
25 | | ovex 6937 |
. . . . . . . . . . . . . . 15
⊢
(ℕ0 ↑𝑚 𝑖) ∈ V |
26 | 25 | rabex 5037 |
. . . . . . . . . . . . . 14
⊢ {ℎ ∈ (ℕ0
↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ∈
V |
27 | 26 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → {ℎ ∈ (ℕ0
↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ∈
V) |
28 | 12 | adantr 474 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → 𝑖 = 𝐼) |
29 | 28 | oveq2d 6921 |
. . . . . . . . . . . . . . 15
⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → (ℕ0
↑𝑚 𝑖) = (ℕ0
↑𝑚 𝐼)) |
30 | | rabeq 3405 |
. . . . . . . . . . . . . . 15
⊢
((ℕ0 ↑𝑚 𝑖) = (ℕ0
↑𝑚 𝐼) → {ℎ ∈ (ℕ0
↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} = {ℎ ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈
Fin}) |
31 | 29, 30 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → {ℎ ∈ (ℕ0
↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} = {ℎ ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈
Fin}) |
32 | | opsrval.d |
. . . . . . . . . . . . . 14
⊢ 𝐷 = {ℎ ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} |
33 | 31, 32 | syl6eqr 2879 |
. . . . . . . . . . . . 13
⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → {ℎ ∈ (ℕ0
↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} = 𝐷) |
34 | | simpr 479 |
. . . . . . . . . . . . . 14
⊢ ((((𝑖 = 𝐼 ∧ 𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → 𝑑 = 𝐷) |
35 | | simpllr 795 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑖 = 𝐼 ∧ 𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → 𝑠 = 𝑅) |
36 | 35 | fveq2d 6437 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑖 = 𝐼 ∧ 𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → (lt‘𝑠) = (lt‘𝑅)) |
37 | | opsrval.q |
. . . . . . . . . . . . . . . . 17
⊢ < =
(lt‘𝑅) |
38 | 36, 37 | syl6eqr 2879 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑖 = 𝐼 ∧ 𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → (lt‘𝑠) = < ) |
39 | 38 | breqd 4884 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑖 = 𝐼 ∧ 𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → ((𝑥‘𝑧)(lt‘𝑠)(𝑦‘𝑧) ↔ (𝑥‘𝑧) < (𝑦‘𝑧))) |
40 | 28 | adantr 474 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑖 = 𝐼 ∧ 𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → 𝑖 = 𝐼) |
41 | 40 | oveq2d 6921 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑖 = 𝐼 ∧ 𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → (𝑟 <bag 𝑖) = (𝑟 <bag 𝐼)) |
42 | 41 | breqd 4884 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑖 = 𝐼 ∧ 𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → (𝑤(𝑟 <bag 𝑖)𝑧 ↔ 𝑤(𝑟 <bag 𝐼)𝑧)) |
43 | 42 | imbi1d 333 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑖 = 𝐼 ∧ 𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → ((𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))) |
44 | 34, 43 | raleqbidv 3364 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑖 = 𝐼 ∧ 𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → (∀𝑤 ∈ 𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ ∀𝑤 ∈ 𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))) |
45 | 39, 44 | anbi12d 626 |
. . . . . . . . . . . . . 14
⊢ ((((𝑖 = 𝐼 ∧ 𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → (((𝑥‘𝑧)(lt‘𝑠)(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))))) |
46 | 34, 45 | rexeqbidv 3365 |
. . . . . . . . . . . . 13
⊢ ((((𝑖 = 𝐼 ∧ 𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → (∃𝑧 ∈ 𝑑 ((𝑥‘𝑧)(lt‘𝑠)(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))))) |
47 | 27, 33, 46 | sbcied2 3700 |
. . . . . . . . . . . 12
⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → ([{ℎ ∈ (ℕ0
↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} / 𝑑]∃𝑧 ∈ 𝑑 ((𝑥‘𝑧)(lt‘𝑠)(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))))) |
48 | 47 | orbi1d 947 |
. . . . . . . . . . 11
⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → (([{ℎ ∈ (ℕ0
↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} / 𝑑]∃𝑧 ∈ 𝑑 ((𝑥‘𝑧)(lt‘𝑠)(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦) ↔ (∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))) |
49 | 24, 48 | anbi12d 626 |
. . . . . . . . . 10
⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → (({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ℎ ∈ (ℕ0
↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} / 𝑑]∃𝑧 ∈ 𝑑 ((𝑥‘𝑧)(lt‘𝑠)(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦)) ↔ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦)))) |
50 | 49 | opabbidv 4939 |
. . . . . . . . 9
⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ℎ ∈ (ℕ0
↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} / 𝑑]∃𝑧 ∈ 𝑑 ((𝑥‘𝑧)(lt‘𝑠)(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))} = {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))}) |
51 | 50 | opeq2d 4630 |
. . . . . . . 8
⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → 〈(le‘ndx), {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ℎ ∈ (ℕ0
↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} / 𝑑]∃𝑧 ∈ 𝑑 ((𝑥‘𝑧)(lt‘𝑠)(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))}〉 = 〈(le‘ndx),
{〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))}〉) |
52 | 20, 51 | oveq12d 6923 |
. . . . . . 7
⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → (𝑝 sSet 〈(le‘ndx), {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ℎ ∈ (ℕ0
↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} / 𝑑]∃𝑧 ∈ 𝑑 ((𝑥‘𝑧)(lt‘𝑠)(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))}〉) = (𝑆 sSet 〈(le‘ndx), {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))}〉)) |
53 | 15, 52 | csbied 3784 |
. . . . . 6
⊢ ((𝑖 = 𝐼 ∧ 𝑠 = 𝑅) → ⦋(𝑖 mPwSer 𝑠) / 𝑝⦌(𝑝 sSet 〈(le‘ndx), {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ℎ ∈ (ℕ0
↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} / 𝑑]∃𝑧 ∈ 𝑑 ((𝑥‘𝑧)(lt‘𝑠)(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))}〉) = (𝑆 sSet 〈(le‘ndx), {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))}〉)) |
54 | 14, 53 | mpteq12dv 4956 |
. . . . 5
⊢ ((𝑖 = 𝐼 ∧ 𝑠 = 𝑅) → (𝑟 ∈ 𝒫 (𝑖 × 𝑖) ↦ ⦋(𝑖 mPwSer 𝑠) / 𝑝⦌(𝑝 sSet 〈(le‘ndx), {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ℎ ∈ (ℕ0
↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} / 𝑑]∃𝑧 ∈ 𝑑 ((𝑥‘𝑧)(lt‘𝑠)(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))}〉)) = (𝑟 ∈ 𝒫 (𝐼 × 𝐼) ↦ (𝑆 sSet 〈(le‘ndx), {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))}〉))) |
55 | | df-opsr 19721 |
. . . . 5
⊢ ordPwSer
= (𝑖 ∈ V, 𝑠 ∈ V ↦ (𝑟 ∈ 𝒫 (𝑖 × 𝑖) ↦ ⦋(𝑖 mPwSer 𝑠) / 𝑝⦌(𝑝 sSet 〈(le‘ndx), {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ℎ ∈ (ℕ0
↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} / 𝑑]∃𝑧 ∈ 𝑑 ((𝑥‘𝑧)(lt‘𝑠)(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))}〉))) |
56 | 54, 55 | ovmpt2ga 7050 |
. . . 4
⊢ ((𝐼 ∈ V ∧ 𝑅 ∈ V ∧ (𝑟 ∈ 𝒫 (𝐼 × 𝐼) ↦ (𝑆 sSet 〈(le‘ndx), {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))}〉)) ∈ V) → (𝐼 ordPwSer 𝑅) = (𝑟 ∈ 𝒫 (𝐼 × 𝐼) ↦ (𝑆 sSet 〈(le‘ndx), {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))}〉))) |
57 | 4, 7, 11, 56 | syl3anc 1496 |
. . 3
⊢ (𝜑 → (𝐼 ordPwSer 𝑅) = (𝑟 ∈ 𝒫 (𝐼 × 𝐼) ↦ (𝑆 sSet 〈(le‘ndx), {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))}〉))) |
58 | | simpr 479 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑟 = 𝑇) → 𝑟 = 𝑇) |
59 | 58 | oveq1d 6920 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑟 = 𝑇) → (𝑟 <bag 𝐼) = (𝑇 <bag 𝐼)) |
60 | | opsrval.c |
. . . . . . . . . . . . . . 15
⊢ 𝐶 = (𝑇 <bag 𝐼) |
61 | 59, 60 | syl6eqr 2879 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑟 = 𝑇) → (𝑟 <bag 𝐼) = 𝐶) |
62 | 61 | breqd 4884 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑟 = 𝑇) → (𝑤(𝑟 <bag 𝐼)𝑧 ↔ 𝑤𝐶𝑧)) |
63 | 62 | imbi1d 333 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑟 = 𝑇) → ((𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ (𝑤𝐶𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))) |
64 | 63 | ralbidv 3195 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑟 = 𝑇) → (∀𝑤 ∈ 𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ ∀𝑤 ∈ 𝐷 (𝑤𝐶𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))) |
65 | 64 | anbi2d 624 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑟 = 𝑇) → (((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤𝐶𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))))) |
66 | 65 | rexbidv 3262 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑟 = 𝑇) → (∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤𝐶𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))))) |
67 | 66 | orbi1d 947 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑟 = 𝑇) → ((∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦) ↔ (∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤𝐶𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))) |
68 | 67 | anbi2d 624 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑟 = 𝑇) → (({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦)) ↔ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤𝐶𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦)))) |
69 | 68 | opabbidv 4939 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑟 = 𝑇) → {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))} = {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤𝐶𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))}) |
70 | | opsrval.l |
. . . . . 6
⊢ ≤ =
{〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤𝐶𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))} |
71 | 69, 70 | syl6eqr 2879 |
. . . . 5
⊢ ((𝜑 ∧ 𝑟 = 𝑇) → {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))} = ≤ ) |
72 | 71 | opeq2d 4630 |
. . . 4
⊢ ((𝜑 ∧ 𝑟 = 𝑇) → 〈(le‘ndx), {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))}〉 = 〈(le‘ndx), ≤
〉) |
73 | 72 | oveq2d 6921 |
. . 3
⊢ ((𝜑 ∧ 𝑟 = 𝑇) → (𝑆 sSet 〈(le‘ndx), {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))}〉) = (𝑆 sSet 〈(le‘ndx), ≤
〉)) |
74 | | opsrval.t |
. . . 4
⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼)) |
75 | | elpw2g 5049 |
. . . . 5
⊢ ((𝐼 × 𝐼) ∈ V → (𝑇 ∈ 𝒫 (𝐼 × 𝐼) ↔ 𝑇 ⊆ (𝐼 × 𝐼))) |
76 | 8, 75 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑇 ∈ 𝒫 (𝐼 × 𝐼) ↔ 𝑇 ⊆ (𝐼 × 𝐼))) |
77 | 74, 76 | mpbird 249 |
. . 3
⊢ (𝜑 → 𝑇 ∈ 𝒫 (𝐼 × 𝐼)) |
78 | | ovexd 6939 |
. . 3
⊢ (𝜑 → (𝑆 sSet 〈(le‘ndx), ≤ 〉)
∈ V) |
79 | 57, 73, 77, 78 | fvmptd 6535 |
. 2
⊢ (𝜑 → ((𝐼 ordPwSer 𝑅)‘𝑇) = (𝑆 sSet 〈(le‘ndx), ≤
〉)) |
80 | 1, 79 | syl5eq 2873 |
1
⊢ (𝜑 → 𝑂 = (𝑆 sSet 〈(le‘ndx), ≤
〉)) |