Step |
Hyp |
Ref |
Expression |
1 |
|
opsrso.o |
⊢ 𝑂 = ( ( 𝐼 ordPwSer 𝑅 ) ‘ 𝑇 ) |
2 |
|
opsrso.i |
⊢ ( 𝜑 → 𝐼 ∈ 𝑉 ) |
3 |
|
opsrso.r |
⊢ ( 𝜑 → 𝑅 ∈ Toset ) |
4 |
|
opsrso.t |
⊢ ( 𝜑 → 𝑇 ⊆ ( 𝐼 × 𝐼 ) ) |
5 |
|
opsrso.w |
⊢ ( 𝜑 → 𝑇 We 𝐼 ) |
6 |
|
opsrtoslem.s |
⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 ) |
7 |
|
opsrtoslem.b |
⊢ 𝐵 = ( Base ‘ 𝑆 ) |
8 |
|
opsrtoslem.q |
⊢ < = ( lt ‘ 𝑅 ) |
9 |
|
opsrtoslem.c |
⊢ 𝐶 = ( 𝑇 <bag 𝐼 ) |
10 |
|
opsrtoslem.d |
⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } |
11 |
|
opsrtoslem.ps |
⊢ ( 𝜓 ↔ ∃ 𝑧 ∈ 𝐷 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 𝐶 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ) |
12 |
|
opsrtoslem.l |
⊢ ≤ = ( le ‘ 𝑂 ) |
13 |
6 1 7 8 9 10 12 4
|
opsrle |
⊢ ( 𝜑 → ≤ = { 〈 𝑥 , 𝑦 〉 ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ( ∃ 𝑧 ∈ 𝐷 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 𝐶 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) } ) |
14 |
|
unopab |
⊢ ( { 〈 𝑥 , 𝑦 〉 ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ 𝜓 ) } ∪ { 〈 𝑥 , 𝑦 〉 ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ 𝑥 = 𝑦 ) } ) = { 〈 𝑥 , 𝑦 〉 ∣ ( ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ 𝜓 ) ∨ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ 𝑥 = 𝑦 ) ) } |
15 |
|
inopab |
⊢ ( { 〈 𝑥 , 𝑦 〉 ∣ 𝜓 } ∩ { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) } ) = { 〈 𝑥 , 𝑦 〉 ∣ ( 𝜓 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) } |
16 |
|
df-xp |
⊢ ( 𝐵 × 𝐵 ) = { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) } |
17 |
16
|
ineq2i |
⊢ ( { 〈 𝑥 , 𝑦 〉 ∣ 𝜓 } ∩ ( 𝐵 × 𝐵 ) ) = ( { 〈 𝑥 , 𝑦 〉 ∣ 𝜓 } ∩ { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) } ) |
18 |
|
vex |
⊢ 𝑥 ∈ V |
19 |
|
vex |
⊢ 𝑦 ∈ V |
20 |
18 19
|
prss |
⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ↔ { 𝑥 , 𝑦 } ⊆ 𝐵 ) |
21 |
20
|
anbi1i |
⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜓 ) ↔ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ 𝜓 ) ) |
22 |
|
ancom |
⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜓 ) ↔ ( 𝜓 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ) |
23 |
21 22
|
bitr3i |
⊢ ( ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ 𝜓 ) ↔ ( 𝜓 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ) |
24 |
23
|
opabbii |
⊢ { 〈 𝑥 , 𝑦 〉 ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ 𝜓 ) } = { 〈 𝑥 , 𝑦 〉 ∣ ( 𝜓 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) } |
25 |
15 17 24
|
3eqtr4i |
⊢ ( { 〈 𝑥 , 𝑦 〉 ∣ 𝜓 } ∩ ( 𝐵 × 𝐵 ) ) = { 〈 𝑥 , 𝑦 〉 ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ 𝜓 ) } |
26 |
|
opabresid |
⊢ ( I ↾ 𝐵 ) = { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝐵 ∧ 𝑦 = 𝑥 ) } |
27 |
|
equcom |
⊢ ( 𝑥 = 𝑦 ↔ 𝑦 = 𝑥 ) |
28 |
27
|
anbi2i |
⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑥 = 𝑦 ) ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑦 = 𝑥 ) ) |
29 |
|
eleq1w |
⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵 ) ) |
30 |
29
|
biimpac |
⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑥 = 𝑦 ) → 𝑦 ∈ 𝐵 ) |
31 |
30
|
pm4.71i |
⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑥 = 𝑦 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑥 = 𝑦 ) ∧ 𝑦 ∈ 𝐵 ) ) |
32 |
28 31
|
bitr3i |
⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 = 𝑥 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑥 = 𝑦 ) ∧ 𝑦 ∈ 𝐵 ) ) |
33 |
|
an32 |
⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑥 = 𝑦 ) ∧ 𝑦 ∈ 𝐵 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 = 𝑦 ) ) |
34 |
20
|
anbi1i |
⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 = 𝑦 ) ↔ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ 𝑥 = 𝑦 ) ) |
35 |
32 33 34
|
3bitri |
⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 = 𝑥 ) ↔ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ 𝑥 = 𝑦 ) ) |
36 |
35
|
opabbii |
⊢ { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝐵 ∧ 𝑦 = 𝑥 ) } = { 〈 𝑥 , 𝑦 〉 ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ 𝑥 = 𝑦 ) } |
37 |
26 36
|
eqtri |
⊢ ( I ↾ 𝐵 ) = { 〈 𝑥 , 𝑦 〉 ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ 𝑥 = 𝑦 ) } |
38 |
25 37
|
uneq12i |
⊢ ( ( { 〈 𝑥 , 𝑦 〉 ∣ 𝜓 } ∩ ( 𝐵 × 𝐵 ) ) ∪ ( I ↾ 𝐵 ) ) = ( { 〈 𝑥 , 𝑦 〉 ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ 𝜓 ) } ∪ { 〈 𝑥 , 𝑦 〉 ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ 𝑥 = 𝑦 ) } ) |
39 |
11
|
orbi1i |
⊢ ( ( 𝜓 ∨ 𝑥 = 𝑦 ) ↔ ( ∃ 𝑧 ∈ 𝐷 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 𝐶 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) |
40 |
39
|
anbi2i |
⊢ ( ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ( 𝜓 ∨ 𝑥 = 𝑦 ) ) ↔ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ( ∃ 𝑧 ∈ 𝐷 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 𝐶 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) ) |
41 |
|
andi |
⊢ ( ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ( 𝜓 ∨ 𝑥 = 𝑦 ) ) ↔ ( ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ 𝜓 ) ∨ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ 𝑥 = 𝑦 ) ) ) |
42 |
40 41
|
bitr3i |
⊢ ( ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ( ∃ 𝑧 ∈ 𝐷 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 𝐶 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) ↔ ( ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ 𝜓 ) ∨ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ 𝑥 = 𝑦 ) ) ) |
43 |
42
|
opabbii |
⊢ { 〈 𝑥 , 𝑦 〉 ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ( ∃ 𝑧 ∈ 𝐷 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 𝐶 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) } = { 〈 𝑥 , 𝑦 〉 ∣ ( ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ 𝜓 ) ∨ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ 𝑥 = 𝑦 ) ) } |
44 |
14 38 43
|
3eqtr4ri |
⊢ { 〈 𝑥 , 𝑦 〉 ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ( ∃ 𝑧 ∈ 𝐷 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 𝐶 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) } = ( ( { 〈 𝑥 , 𝑦 〉 ∣ 𝜓 } ∩ ( 𝐵 × 𝐵 ) ) ∪ ( I ↾ 𝐵 ) ) |
45 |
13 44
|
eqtrdi |
⊢ ( 𝜑 → ≤ = ( ( { 〈 𝑥 , 𝑦 〉 ∣ 𝜓 } ∩ ( 𝐵 × 𝐵 ) ) ∪ ( I ↾ 𝐵 ) ) ) |