| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | prproropf1o.p | . . . . 5
⊢ 𝑃 = {𝑝 ∈ 𝒫 𝑉 ∣ (♯‘𝑝) = 2} | 
| 2 | 1 | prpair 47488 | . . . 4
⊢ (𝑋 ∈ 𝑃 ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑋 = {𝑎, 𝑏} ∧ 𝑎 ≠ 𝑏)) | 
| 3 |  | simpll 767 | . . . . . . . . . 10
⊢ (((𝑅 Or 𝑉 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑋 = {𝑎, 𝑏} ∧ 𝑎 ≠ 𝑏)) → 𝑅 Or 𝑉) | 
| 4 |  | simplrl 777 | . . . . . . . . . 10
⊢ (((𝑅 Or 𝑉 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑋 = {𝑎, 𝑏} ∧ 𝑎 ≠ 𝑏)) → 𝑎 ∈ 𝑉) | 
| 5 |  | simplrr 778 | . . . . . . . . . 10
⊢ (((𝑅 Or 𝑉 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑋 = {𝑎, 𝑏} ∧ 𝑎 ≠ 𝑏)) → 𝑏 ∈ 𝑉) | 
| 6 |  | simprr 773 | . . . . . . . . . 10
⊢ (((𝑅 Or 𝑉 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑋 = {𝑎, 𝑏} ∧ 𝑎 ≠ 𝑏)) → 𝑎 ≠ 𝑏) | 
| 7 |  | infsupprpr 9544 | . . . . . . . . . 10
⊢ ((𝑅 Or 𝑉 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑎 ≠ 𝑏)) → inf({𝑎, 𝑏}, 𝑉, 𝑅)𝑅sup({𝑎, 𝑏}, 𝑉, 𝑅)) | 
| 8 | 3, 4, 5, 6, 7 | syl13anc 1374 | . . . . . . . . 9
⊢ (((𝑅 Or 𝑉 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑋 = {𝑎, 𝑏} ∧ 𝑎 ≠ 𝑏)) → inf({𝑎, 𝑏}, 𝑉, 𝑅)𝑅sup({𝑎, 𝑏}, 𝑉, 𝑅)) | 
| 9 |  | df-br 5144 | . . . . . . . . 9
⊢
(inf({𝑎, 𝑏}, 𝑉, 𝑅)𝑅sup({𝑎, 𝑏}, 𝑉, 𝑅) ↔ 〈inf({𝑎, 𝑏}, 𝑉, 𝑅), sup({𝑎, 𝑏}, 𝑉, 𝑅)〉 ∈ 𝑅) | 
| 10 | 8, 9 | sylib 218 | . . . . . . . 8
⊢ (((𝑅 Or 𝑉 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑋 = {𝑎, 𝑏} ∧ 𝑎 ≠ 𝑏)) → 〈inf({𝑎, 𝑏}, 𝑉, 𝑅), sup({𝑎, 𝑏}, 𝑉, 𝑅)〉 ∈ 𝑅) | 
| 11 |  | infpr 9543 | . . . . . . . . . . . . 13
⊢ ((𝑅 Or 𝑉 ∧ 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) → inf({𝑎, 𝑏}, 𝑉, 𝑅) = if(𝑎𝑅𝑏, 𝑎, 𝑏)) | 
| 12 |  | ifcl 4571 | . . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) → if(𝑎𝑅𝑏, 𝑎, 𝑏) ∈ 𝑉) | 
| 13 | 12 | 3adant1 1131 | . . . . . . . . . . . . 13
⊢ ((𝑅 Or 𝑉 ∧ 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) → if(𝑎𝑅𝑏, 𝑎, 𝑏) ∈ 𝑉) | 
| 14 | 11, 13 | eqeltrd 2841 | . . . . . . . . . . . 12
⊢ ((𝑅 Or 𝑉 ∧ 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) → inf({𝑎, 𝑏}, 𝑉, 𝑅) ∈ 𝑉) | 
| 15 |  | suppr 9511 | . . . . . . . . . . . . 13
⊢ ((𝑅 Or 𝑉 ∧ 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) → sup({𝑎, 𝑏}, 𝑉, 𝑅) = if(𝑏𝑅𝑎, 𝑎, 𝑏)) | 
| 16 |  | ifcl 4571 | . . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) → if(𝑏𝑅𝑎, 𝑎, 𝑏) ∈ 𝑉) | 
| 17 | 16 | 3adant1 1131 | . . . . . . . . . . . . 13
⊢ ((𝑅 Or 𝑉 ∧ 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) → if(𝑏𝑅𝑎, 𝑎, 𝑏) ∈ 𝑉) | 
| 18 | 15, 17 | eqeltrd 2841 | . . . . . . . . . . . 12
⊢ ((𝑅 Or 𝑉 ∧ 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) → sup({𝑎, 𝑏}, 𝑉, 𝑅) ∈ 𝑉) | 
| 19 | 14, 18 | jca 511 | . . . . . . . . . . 11
⊢ ((𝑅 Or 𝑉 ∧ 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) → (inf({𝑎, 𝑏}, 𝑉, 𝑅) ∈ 𝑉 ∧ sup({𝑎, 𝑏}, 𝑉, 𝑅) ∈ 𝑉)) | 
| 20 | 19 | 3expb 1121 | . . . . . . . . . 10
⊢ ((𝑅 Or 𝑉 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (inf({𝑎, 𝑏}, 𝑉, 𝑅) ∈ 𝑉 ∧ sup({𝑎, 𝑏}, 𝑉, 𝑅) ∈ 𝑉)) | 
| 21 | 20 | adantr 480 | . . . . . . . . 9
⊢ (((𝑅 Or 𝑉 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑋 = {𝑎, 𝑏} ∧ 𝑎 ≠ 𝑏)) → (inf({𝑎, 𝑏}, 𝑉, 𝑅) ∈ 𝑉 ∧ sup({𝑎, 𝑏}, 𝑉, 𝑅) ∈ 𝑉)) | 
| 22 |  | opelxp 5721 | . . . . . . . . 9
⊢
(〈inf({𝑎, 𝑏}, 𝑉, 𝑅), sup({𝑎, 𝑏}, 𝑉, 𝑅)〉 ∈ (𝑉 × 𝑉) ↔ (inf({𝑎, 𝑏}, 𝑉, 𝑅) ∈ 𝑉 ∧ sup({𝑎, 𝑏}, 𝑉, 𝑅) ∈ 𝑉)) | 
| 23 | 21, 22 | sylibr 234 | . . . . . . . 8
⊢ (((𝑅 Or 𝑉 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑋 = {𝑎, 𝑏} ∧ 𝑎 ≠ 𝑏)) → 〈inf({𝑎, 𝑏}, 𝑉, 𝑅), sup({𝑎, 𝑏}, 𝑉, 𝑅)〉 ∈ (𝑉 × 𝑉)) | 
| 24 | 10, 23 | elind 4200 | . . . . . . 7
⊢ (((𝑅 Or 𝑉 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑋 = {𝑎, 𝑏} ∧ 𝑎 ≠ 𝑏)) → 〈inf({𝑎, 𝑏}, 𝑉, 𝑅), sup({𝑎, 𝑏}, 𝑉, 𝑅)〉 ∈ (𝑅 ∩ (𝑉 × 𝑉))) | 
| 25 |  | infeq1 9516 | . . . . . . . . . 10
⊢ (𝑋 = {𝑎, 𝑏} → inf(𝑋, 𝑉, 𝑅) = inf({𝑎, 𝑏}, 𝑉, 𝑅)) | 
| 26 |  | supeq1 9485 | . . . . . . . . . 10
⊢ (𝑋 = {𝑎, 𝑏} → sup(𝑋, 𝑉, 𝑅) = sup({𝑎, 𝑏}, 𝑉, 𝑅)) | 
| 27 | 25, 26 | opeq12d 4881 | . . . . . . . . 9
⊢ (𝑋 = {𝑎, 𝑏} → 〈inf(𝑋, 𝑉, 𝑅), sup(𝑋, 𝑉, 𝑅)〉 = 〈inf({𝑎, 𝑏}, 𝑉, 𝑅), sup({𝑎, 𝑏}, 𝑉, 𝑅)〉) | 
| 28 | 27 | eleq1d 2826 | . . . . . . . 8
⊢ (𝑋 = {𝑎, 𝑏} → (〈inf(𝑋, 𝑉, 𝑅), sup(𝑋, 𝑉, 𝑅)〉 ∈ (𝑅 ∩ (𝑉 × 𝑉)) ↔ 〈inf({𝑎, 𝑏}, 𝑉, 𝑅), sup({𝑎, 𝑏}, 𝑉, 𝑅)〉 ∈ (𝑅 ∩ (𝑉 × 𝑉)))) | 
| 29 | 28 | ad2antrl 728 | . . . . . . 7
⊢ (((𝑅 Or 𝑉 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑋 = {𝑎, 𝑏} ∧ 𝑎 ≠ 𝑏)) → (〈inf(𝑋, 𝑉, 𝑅), sup(𝑋, 𝑉, 𝑅)〉 ∈ (𝑅 ∩ (𝑉 × 𝑉)) ↔ 〈inf({𝑎, 𝑏}, 𝑉, 𝑅), sup({𝑎, 𝑏}, 𝑉, 𝑅)〉 ∈ (𝑅 ∩ (𝑉 × 𝑉)))) | 
| 30 | 24, 29 | mpbird 257 | . . . . . 6
⊢ (((𝑅 Or 𝑉 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑋 = {𝑎, 𝑏} ∧ 𝑎 ≠ 𝑏)) → 〈inf(𝑋, 𝑉, 𝑅), sup(𝑋, 𝑉, 𝑅)〉 ∈ (𝑅 ∩ (𝑉 × 𝑉))) | 
| 31 | 30 | ex 412 | . . . . 5
⊢ ((𝑅 Or 𝑉 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → ((𝑋 = {𝑎, 𝑏} ∧ 𝑎 ≠ 𝑏) → 〈inf(𝑋, 𝑉, 𝑅), sup(𝑋, 𝑉, 𝑅)〉 ∈ (𝑅 ∩ (𝑉 × 𝑉)))) | 
| 32 | 31 | rexlimdvva 3213 | . . . 4
⊢ (𝑅 Or 𝑉 → (∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑋 = {𝑎, 𝑏} ∧ 𝑎 ≠ 𝑏) → 〈inf(𝑋, 𝑉, 𝑅), sup(𝑋, 𝑉, 𝑅)〉 ∈ (𝑅 ∩ (𝑉 × 𝑉)))) | 
| 33 | 2, 32 | biimtrid 242 | . . 3
⊢ (𝑅 Or 𝑉 → (𝑋 ∈ 𝑃 → 〈inf(𝑋, 𝑉, 𝑅), sup(𝑋, 𝑉, 𝑅)〉 ∈ (𝑅 ∩ (𝑉 × 𝑉)))) | 
| 34 | 33 | imp 406 | . 2
⊢ ((𝑅 Or 𝑉 ∧ 𝑋 ∈ 𝑃) → 〈inf(𝑋, 𝑉, 𝑅), sup(𝑋, 𝑉, 𝑅)〉 ∈ (𝑅 ∩ (𝑉 × 𝑉))) | 
| 35 |  | prproropf1o.o | . 2
⊢ 𝑂 = (𝑅 ∩ (𝑉 × 𝑉)) | 
| 36 | 34, 35 | eleqtrrdi 2852 | 1
⊢ ((𝑅 Or 𝑉 ∧ 𝑋 ∈ 𝑃) → 〈inf(𝑋, 𝑉, 𝑅), sup(𝑋, 𝑉, 𝑅)〉 ∈ 𝑂) |