Proof of Theorem prproropf1olem3
| Step | Hyp | Ref
| Expression |
| 1 | | prproropf1o.f |
. 2
⊢ 𝐹 = (𝑝 ∈ 𝑃 ↦ 〈inf(𝑝, 𝑉, 𝑅), sup(𝑝, 𝑉, 𝑅)〉) |
| 2 | | infeq1 9516 |
. . . 4
⊢ (𝑝 = {(1st ‘𝑊), (2nd ‘𝑊)} → inf(𝑝, 𝑉, 𝑅) = inf({(1st ‘𝑊), (2nd ‘𝑊)}, 𝑉, 𝑅)) |
| 3 | | supeq1 9485 |
. . . 4
⊢ (𝑝 = {(1st ‘𝑊), (2nd ‘𝑊)} → sup(𝑝, 𝑉, 𝑅) = sup({(1st ‘𝑊), (2nd ‘𝑊)}, 𝑉, 𝑅)) |
| 4 | 2, 3 | opeq12d 4881 |
. . 3
⊢ (𝑝 = {(1st ‘𝑊), (2nd ‘𝑊)} → 〈inf(𝑝, 𝑉, 𝑅), sup(𝑝, 𝑉, 𝑅)〉 = 〈inf({(1st
‘𝑊), (2nd
‘𝑊)}, 𝑉, 𝑅), sup({(1st ‘𝑊), (2nd ‘𝑊)}, 𝑉, 𝑅)〉) |
| 5 | | prproropf1o.o |
. . . . 5
⊢ 𝑂 = (𝑅 ∩ (𝑉 × 𝑉)) |
| 6 | 5 | prproropf1olem0 47489 |
. . . 4
⊢ (𝑊 ∈ 𝑂 ↔ (𝑊 = 〈(1st ‘𝑊), (2nd ‘𝑊)〉 ∧ ((1st
‘𝑊) ∈ 𝑉 ∧ (2nd
‘𝑊) ∈ 𝑉) ∧ (1st
‘𝑊)𝑅(2nd ‘𝑊))) |
| 7 | | simpl 482 |
. . . . . . . 8
⊢ ((𝑅 Or 𝑉 ∧ (((1st ‘𝑊) ∈ 𝑉 ∧ (2nd ‘𝑊) ∈ 𝑉) ∧ (1st ‘𝑊)𝑅(2nd ‘𝑊))) → 𝑅 Or 𝑉) |
| 8 | | simprll 779 |
. . . . . . . 8
⊢ ((𝑅 Or 𝑉 ∧ (((1st ‘𝑊) ∈ 𝑉 ∧ (2nd ‘𝑊) ∈ 𝑉) ∧ (1st ‘𝑊)𝑅(2nd ‘𝑊))) → (1st ‘𝑊) ∈ 𝑉) |
| 9 | | simprlr 780 |
. . . . . . . 8
⊢ ((𝑅 Or 𝑉 ∧ (((1st ‘𝑊) ∈ 𝑉 ∧ (2nd ‘𝑊) ∈ 𝑉) ∧ (1st ‘𝑊)𝑅(2nd ‘𝑊))) → (2nd ‘𝑊) ∈ 𝑉) |
| 10 | | infpr 9543 |
. . . . . . . 8
⊢ ((𝑅 Or 𝑉 ∧ (1st ‘𝑊) ∈ 𝑉 ∧ (2nd ‘𝑊) ∈ 𝑉) → inf({(1st ‘𝑊), (2nd ‘𝑊)}, 𝑉, 𝑅) = if((1st ‘𝑊)𝑅(2nd ‘𝑊), (1st ‘𝑊), (2nd ‘𝑊))) |
| 11 | 7, 8, 9, 10 | syl3anc 1373 |
. . . . . . 7
⊢ ((𝑅 Or 𝑉 ∧ (((1st ‘𝑊) ∈ 𝑉 ∧ (2nd ‘𝑊) ∈ 𝑉) ∧ (1st ‘𝑊)𝑅(2nd ‘𝑊))) → inf({(1st ‘𝑊), (2nd ‘𝑊)}, 𝑉, 𝑅) = if((1st ‘𝑊)𝑅(2nd ‘𝑊), (1st ‘𝑊), (2nd ‘𝑊))) |
| 12 | | iftrue 4531 |
. . . . . . . 8
⊢
((1st ‘𝑊)𝑅(2nd ‘𝑊) → if((1st ‘𝑊)𝑅(2nd ‘𝑊), (1st ‘𝑊), (2nd ‘𝑊)) = (1st ‘𝑊)) |
| 13 | 12 | ad2antll 729 |
. . . . . . 7
⊢ ((𝑅 Or 𝑉 ∧ (((1st ‘𝑊) ∈ 𝑉 ∧ (2nd ‘𝑊) ∈ 𝑉) ∧ (1st ‘𝑊)𝑅(2nd ‘𝑊))) → if((1st ‘𝑊)𝑅(2nd ‘𝑊), (1st ‘𝑊), (2nd ‘𝑊)) = (1st ‘𝑊)) |
| 14 | 11, 13 | eqtrd 2777 |
. . . . . 6
⊢ ((𝑅 Or 𝑉 ∧ (((1st ‘𝑊) ∈ 𝑉 ∧ (2nd ‘𝑊) ∈ 𝑉) ∧ (1st ‘𝑊)𝑅(2nd ‘𝑊))) → inf({(1st ‘𝑊), (2nd ‘𝑊)}, 𝑉, 𝑅) = (1st ‘𝑊)) |
| 15 | | suppr 9511 |
. . . . . . . 8
⊢ ((𝑅 Or 𝑉 ∧ (1st ‘𝑊) ∈ 𝑉 ∧ (2nd ‘𝑊) ∈ 𝑉) → sup({(1st ‘𝑊), (2nd ‘𝑊)}, 𝑉, 𝑅) = if((2nd ‘𝑊)𝑅(1st ‘𝑊), (1st ‘𝑊), (2nd ‘𝑊))) |
| 16 | 7, 8, 9, 15 | syl3anc 1373 |
. . . . . . 7
⊢ ((𝑅 Or 𝑉 ∧ (((1st ‘𝑊) ∈ 𝑉 ∧ (2nd ‘𝑊) ∈ 𝑉) ∧ (1st ‘𝑊)𝑅(2nd ‘𝑊))) → sup({(1st ‘𝑊), (2nd ‘𝑊)}, 𝑉, 𝑅) = if((2nd ‘𝑊)𝑅(1st ‘𝑊), (1st ‘𝑊), (2nd ‘𝑊))) |
| 17 | | soasym 5625 |
. . . . . . . . 9
⊢ ((𝑅 Or 𝑉 ∧ ((1st ‘𝑊) ∈ 𝑉 ∧ (2nd ‘𝑊) ∈ 𝑉)) → ((1st ‘𝑊)𝑅(2nd ‘𝑊) → ¬ (2nd ‘𝑊)𝑅(1st ‘𝑊))) |
| 18 | 17 | impr 454 |
. . . . . . . 8
⊢ ((𝑅 Or 𝑉 ∧ (((1st ‘𝑊) ∈ 𝑉 ∧ (2nd ‘𝑊) ∈ 𝑉) ∧ (1st ‘𝑊)𝑅(2nd ‘𝑊))) → ¬ (2nd
‘𝑊)𝑅(1st ‘𝑊)) |
| 19 | 18 | iffalsed 4536 |
. . . . . . 7
⊢ ((𝑅 Or 𝑉 ∧ (((1st ‘𝑊) ∈ 𝑉 ∧ (2nd ‘𝑊) ∈ 𝑉) ∧ (1st ‘𝑊)𝑅(2nd ‘𝑊))) → if((2nd ‘𝑊)𝑅(1st ‘𝑊), (1st ‘𝑊), (2nd ‘𝑊)) = (2nd ‘𝑊)) |
| 20 | 16, 19 | eqtrd 2777 |
. . . . . 6
⊢ ((𝑅 Or 𝑉 ∧ (((1st ‘𝑊) ∈ 𝑉 ∧ (2nd ‘𝑊) ∈ 𝑉) ∧ (1st ‘𝑊)𝑅(2nd ‘𝑊))) → sup({(1st ‘𝑊), (2nd ‘𝑊)}, 𝑉, 𝑅) = (2nd ‘𝑊)) |
| 21 | 14, 20 | opeq12d 4881 |
. . . . 5
⊢ ((𝑅 Or 𝑉 ∧ (((1st ‘𝑊) ∈ 𝑉 ∧ (2nd ‘𝑊) ∈ 𝑉) ∧ (1st ‘𝑊)𝑅(2nd ‘𝑊))) → 〈inf({(1st
‘𝑊), (2nd
‘𝑊)}, 𝑉, 𝑅), sup({(1st ‘𝑊), (2nd ‘𝑊)}, 𝑉, 𝑅)〉 = 〈(1st ‘𝑊), (2nd ‘𝑊)〉) |
| 22 | 21 | 3adantr1 1170 |
. . . 4
⊢ ((𝑅 Or 𝑉 ∧ (𝑊 = 〈(1st ‘𝑊), (2nd ‘𝑊)〉 ∧ ((1st
‘𝑊) ∈ 𝑉 ∧ (2nd
‘𝑊) ∈ 𝑉) ∧ (1st
‘𝑊)𝑅(2nd ‘𝑊))) → 〈inf({(1st
‘𝑊), (2nd
‘𝑊)}, 𝑉, 𝑅), sup({(1st ‘𝑊), (2nd ‘𝑊)}, 𝑉, 𝑅)〉 = 〈(1st ‘𝑊), (2nd ‘𝑊)〉) |
| 23 | 6, 22 | sylan2b 594 |
. . 3
⊢ ((𝑅 Or 𝑉 ∧ 𝑊 ∈ 𝑂) → 〈inf({(1st
‘𝑊), (2nd
‘𝑊)}, 𝑉, 𝑅), sup({(1st ‘𝑊), (2nd ‘𝑊)}, 𝑉, 𝑅)〉 = 〈(1st ‘𝑊), (2nd ‘𝑊)〉) |
| 24 | 4, 23 | sylan9eqr 2799 |
. 2
⊢ (((𝑅 Or 𝑉 ∧ 𝑊 ∈ 𝑂) ∧ 𝑝 = {(1st ‘𝑊), (2nd ‘𝑊)}) → 〈inf(𝑝, 𝑉, 𝑅), sup(𝑝, 𝑉, 𝑅)〉 = 〈(1st ‘𝑊), (2nd ‘𝑊)〉) |
| 25 | | prproropf1o.p |
. . 3
⊢ 𝑃 = {𝑝 ∈ 𝒫 𝑉 ∣ (♯‘𝑝) = 2} |
| 26 | 5, 25 | prproropf1olem1 47490 |
. 2
⊢ ((𝑅 Or 𝑉 ∧ 𝑊 ∈ 𝑂) → {(1st ‘𝑊), (2nd ‘𝑊)} ∈ 𝑃) |
| 27 | | opex 5469 |
. . 3
⊢
〈(1st ‘𝑊), (2nd ‘𝑊)〉 ∈ V |
| 28 | 27 | a1i 11 |
. 2
⊢ ((𝑅 Or 𝑉 ∧ 𝑊 ∈ 𝑂) → 〈(1st ‘𝑊), (2nd ‘𝑊)〉 ∈
V) |
| 29 | 1, 24, 26, 28 | fvmptd2 7024 |
1
⊢ ((𝑅 Or 𝑉 ∧ 𝑊 ∈ 𝑂) → (𝐹‘{(1st ‘𝑊), (2nd ‘𝑊)}) = 〈(1st
‘𝑊), (2nd
‘𝑊)〉) |