Proof of Theorem opsrle
Step | Hyp | Ref
| Expression |
1 | | opsrle.s |
. . . . 5
⊢ 𝑆 = (𝐼 mPwSer 𝑅) |
2 | | opsrle.o |
. . . . 5
⊢ 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇) |
3 | | opsrle.b |
. . . . 5
⊢ 𝐵 = (Base‘𝑆) |
4 | | opsrle.q |
. . . . 5
⊢ < =
(lt‘𝑅) |
5 | | opsrle.c |
. . . . 5
⊢ 𝐶 = (𝑇 <bag 𝐼) |
6 | | opsrle.d |
. . . . 5
⊢ 𝐷 = {ℎ ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} |
7 | | eqid 2610 |
. . . . 5
⊢
{〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤𝐶𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))} = {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤𝐶𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))} |
8 | | simprl 790 |
. . . . 5
⊢ ((𝜑 ∧ (𝐼 ∈ V ∧ 𝑅 ∈ V)) → 𝐼 ∈ V) |
9 | | simprr 792 |
. . . . 5
⊢ ((𝜑 ∧ (𝐼 ∈ V ∧ 𝑅 ∈ V)) → 𝑅 ∈ V) |
10 | | opsrle.t |
. . . . . 6
⊢ (𝜑 → 𝑇 ⊆ (𝐼 × 𝐼)) |
11 | 10 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝐼 ∈ V ∧ 𝑅 ∈ V)) → 𝑇 ⊆ (𝐼 × 𝐼)) |
12 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 11 | opsrval 19295 |
. . . 4
⊢ ((𝜑 ∧ (𝐼 ∈ V ∧ 𝑅 ∈ V)) → 𝑂 = (𝑆 sSet 〈(le‘ndx), {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤𝐶𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))}〉)) |
13 | 12 | fveq2d 6107 |
. . 3
⊢ ((𝜑 ∧ (𝐼 ∈ V ∧ 𝑅 ∈ V)) → (le‘𝑂) = (le‘(𝑆 sSet 〈(le‘ndx), {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤𝐶𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))}〉))) |
14 | | opsrle.l |
. . 3
⊢ ≤ =
(le‘𝑂) |
15 | | ovex 6577 |
. . . . 5
⊢ (𝐼 mPwSer 𝑅) ∈ V |
16 | 1, 15 | eqeltri 2684 |
. . . 4
⊢ 𝑆 ∈ V |
17 | | fvex 6113 |
. . . . . . 7
⊢
(Base‘𝑆)
∈ V |
18 | 3, 17 | eqeltri 2684 |
. . . . . 6
⊢ 𝐵 ∈ V |
19 | 18, 18 | xpex 6860 |
. . . . 5
⊢ (𝐵 × 𝐵) ∈ V |
20 | | vex 3176 |
. . . . . . . . 9
⊢ 𝑥 ∈ V |
21 | | vex 3176 |
. . . . . . . . 9
⊢ 𝑦 ∈ V |
22 | 20, 21 | prss 4291 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ↔ {𝑥, 𝑦} ⊆ 𝐵) |
23 | 22 | anbi1i 727 |
. . . . . . 7
⊢ (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤𝐶𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦)) ↔ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤𝐶𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))) |
24 | 23 | opabbii 4649 |
. . . . . 6
⊢
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤𝐶𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))} = {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤𝐶𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))} |
25 | | opabssxp 5116 |
. . . . . 6
⊢
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤𝐶𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))} ⊆ (𝐵 × 𝐵) |
26 | 24, 25 | eqsstr3i 3599 |
. . . . 5
⊢
{〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤𝐶𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))} ⊆ (𝐵 × 𝐵) |
27 | 19, 26 | ssexi 4731 |
. . . 4
⊢
{〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤𝐶𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))} ∈ V |
28 | | pleid 15872 |
. . . . 5
⊢ le = Slot
(le‘ndx) |
29 | 28 | setsid 15742 |
. . . 4
⊢ ((𝑆 ∈ V ∧ {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤𝐶𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))} ∈ V) → {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤𝐶𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))} = (le‘(𝑆 sSet 〈(le‘ndx), {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤𝐶𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))}〉))) |
30 | 16, 27, 29 | mp2an 704 |
. . 3
⊢
{〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤𝐶𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))} = (le‘(𝑆 sSet 〈(le‘ndx), {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤𝐶𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))}〉)) |
31 | 13, 14, 30 | 3eqtr4g 2669 |
. 2
⊢ ((𝜑 ∧ (𝐼 ∈ V ∧ 𝑅 ∈ V)) → ≤ = {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤𝐶𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))}) |
32 | | reldmopsr 19294 |
. . . . . . . . . 10
⊢ Rel dom
ordPwSer |
33 | 32 | ovprc 6581 |
. . . . . . . . 9
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) → (𝐼 ordPwSer 𝑅) = ∅) |
34 | 33 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ (𝐼 ∈ V ∧ 𝑅 ∈ V)) → (𝐼 ordPwSer 𝑅) = ∅) |
35 | 34 | fveq1d 6105 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ (𝐼 ∈ V ∧ 𝑅 ∈ V)) → ((𝐼 ordPwSer 𝑅)‘𝑇) = (∅‘𝑇)) |
36 | 2, 35 | syl5eq 2656 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ (𝐼 ∈ V ∧ 𝑅 ∈ V)) → 𝑂 = (∅‘𝑇)) |
37 | | 0fv 6137 |
. . . . . 6
⊢
(∅‘𝑇) =
∅ |
38 | 36, 37 | syl6eq 2660 |
. . . . 5
⊢ ((𝜑 ∧ ¬ (𝐼 ∈ V ∧ 𝑅 ∈ V)) → 𝑂 = ∅) |
39 | 38 | fveq2d 6107 |
. . . 4
⊢ ((𝜑 ∧ ¬ (𝐼 ∈ V ∧ 𝑅 ∈ V)) → (le‘𝑂) =
(le‘∅)) |
40 | 28 | str0 15739 |
. . . 4
⊢ ∅ =
(le‘∅) |
41 | 39, 14, 40 | 3eqtr4g 2669 |
. . 3
⊢ ((𝜑 ∧ ¬ (𝐼 ∈ V ∧ 𝑅 ∈ V)) → ≤ =
∅) |
42 | | reldmpsr 19182 |
. . . . . . . . . . 11
⊢ Rel dom
mPwSer |
43 | 42 | ovprc 6581 |
. . . . . . . . . 10
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) → (𝐼 mPwSer 𝑅) = ∅) |
44 | 43 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ (𝐼 ∈ V ∧ 𝑅 ∈ V)) → (𝐼 mPwSer 𝑅) = ∅) |
45 | 1, 44 | syl5eq 2656 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ (𝐼 ∈ V ∧ 𝑅 ∈ V)) → 𝑆 = ∅) |
46 | 45 | fveq2d 6107 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ (𝐼 ∈ V ∧ 𝑅 ∈ V)) → (Base‘𝑆) =
(Base‘∅)) |
47 | | base0 15740 |
. . . . . . 7
⊢ ∅ =
(Base‘∅) |
48 | 46, 3, 47 | 3eqtr4g 2669 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ (𝐼 ∈ V ∧ 𝑅 ∈ V)) → 𝐵 = ∅) |
49 | 48 | xpeq2d 5063 |
. . . . 5
⊢ ((𝜑 ∧ ¬ (𝐼 ∈ V ∧ 𝑅 ∈ V)) → (𝐵 × 𝐵) = (𝐵 × ∅)) |
50 | | xp0 5471 |
. . . . 5
⊢ (𝐵 × ∅) =
∅ |
51 | 49, 50 | syl6eq 2660 |
. . . 4
⊢ ((𝜑 ∧ ¬ (𝐼 ∈ V ∧ 𝑅 ∈ V)) → (𝐵 × 𝐵) = ∅) |
52 | | sseq0 3927 |
. . . 4
⊢
(({〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤𝐶𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))} ⊆ (𝐵 × 𝐵) ∧ (𝐵 × 𝐵) = ∅) → {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤𝐶𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))} = ∅) |
53 | 26, 51, 52 | sylancr 694 |
. . 3
⊢ ((𝜑 ∧ ¬ (𝐼 ∈ V ∧ 𝑅 ∈ V)) → {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤𝐶𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))} = ∅) |
54 | 41, 53 | eqtr4d 2647 |
. 2
⊢ ((𝜑 ∧ ¬ (𝐼 ∈ V ∧ 𝑅 ∈ V)) → ≤ = {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤𝐶𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))}) |
55 | 31, 54 | pm2.61dan 828 |
1
⊢ (𝜑 → ≤ = {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧 ∈ 𝐷 ((𝑥‘𝑧) < (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐷 (𝑤𝐶𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))}) |