Step | Hyp | Ref
| Expression |
1 | | simp1 1138 |
. 2
⊢ ((𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → 𝑅 Or 𝐴) |
2 | | ifcl 4484 |
. . 3
⊢ ((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → if(𝐵𝑅𝐶, 𝐵, 𝐶) ∈ 𝐴) |
3 | 2 | 3adant1 1132 |
. 2
⊢ ((𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → if(𝐵𝑅𝐶, 𝐵, 𝐶) ∈ 𝐴) |
4 | | ifpr 4607 |
. . 3
⊢ ((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → if(𝐵𝑅𝐶, 𝐵, 𝐶) ∈ {𝐵, 𝐶}) |
5 | 4 | 3adant1 1132 |
. 2
⊢ ((𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → if(𝐵𝑅𝐶, 𝐵, 𝐶) ∈ {𝐵, 𝐶}) |
6 | | breq2 5057 |
. . . . . 6
⊢ (𝐵 = if(𝐵𝑅𝐶, 𝐵, 𝐶) → (𝐵𝑅𝐵 ↔ 𝐵𝑅if(𝐵𝑅𝐶, 𝐵, 𝐶))) |
7 | 6 | notbid 321 |
. . . . 5
⊢ (𝐵 = if(𝐵𝑅𝐶, 𝐵, 𝐶) → (¬ 𝐵𝑅𝐵 ↔ ¬ 𝐵𝑅if(𝐵𝑅𝐶, 𝐵, 𝐶))) |
8 | | breq2 5057 |
. . . . . 6
⊢ (𝐶 = if(𝐵𝑅𝐶, 𝐵, 𝐶) → (𝐵𝑅𝐶 ↔ 𝐵𝑅if(𝐵𝑅𝐶, 𝐵, 𝐶))) |
9 | 8 | notbid 321 |
. . . . 5
⊢ (𝐶 = if(𝐵𝑅𝐶, 𝐵, 𝐶) → (¬ 𝐵𝑅𝐶 ↔ ¬ 𝐵𝑅if(𝐵𝑅𝐶, 𝐵, 𝐶))) |
10 | | sonr 5491 |
. . . . . . 7
⊢ ((𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴) → ¬ 𝐵𝑅𝐵) |
11 | 10 | 3adant3 1134 |
. . . . . 6
⊢ ((𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → ¬ 𝐵𝑅𝐵) |
12 | 11 | adantr 484 |
. . . . 5
⊢ (((𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) ∧ 𝐵𝑅𝐶) → ¬ 𝐵𝑅𝐵) |
13 | | simpr 488 |
. . . . 5
⊢ (((𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) ∧ ¬ 𝐵𝑅𝐶) → ¬ 𝐵𝑅𝐶) |
14 | 7, 9, 12, 13 | ifbothda 4477 |
. . . 4
⊢ ((𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → ¬ 𝐵𝑅if(𝐵𝑅𝐶, 𝐵, 𝐶)) |
15 | | breq2 5057 |
. . . . . 6
⊢ (𝐵 = if(𝐵𝑅𝐶, 𝐵, 𝐶) → (𝐶𝑅𝐵 ↔ 𝐶𝑅if(𝐵𝑅𝐶, 𝐵, 𝐶))) |
16 | 15 | notbid 321 |
. . . . 5
⊢ (𝐵 = if(𝐵𝑅𝐶, 𝐵, 𝐶) → (¬ 𝐶𝑅𝐵 ↔ ¬ 𝐶𝑅if(𝐵𝑅𝐶, 𝐵, 𝐶))) |
17 | | breq2 5057 |
. . . . . 6
⊢ (𝐶 = if(𝐵𝑅𝐶, 𝐵, 𝐶) → (𝐶𝑅𝐶 ↔ 𝐶𝑅if(𝐵𝑅𝐶, 𝐵, 𝐶))) |
18 | 17 | notbid 321 |
. . . . 5
⊢ (𝐶 = if(𝐵𝑅𝐶, 𝐵, 𝐶) → (¬ 𝐶𝑅𝐶 ↔ ¬ 𝐶𝑅if(𝐵𝑅𝐶, 𝐵, 𝐶))) |
19 | | so2nr 5494 |
. . . . . . . 8
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → ¬ (𝐵𝑅𝐶 ∧ 𝐶𝑅𝐵)) |
20 | 19 | 3impb 1117 |
. . . . . . 7
⊢ ((𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → ¬ (𝐵𝑅𝐶 ∧ 𝐶𝑅𝐵)) |
21 | | imnan 403 |
. . . . . . 7
⊢ ((𝐵𝑅𝐶 → ¬ 𝐶𝑅𝐵) ↔ ¬ (𝐵𝑅𝐶 ∧ 𝐶𝑅𝐵)) |
22 | 20, 21 | sylibr 237 |
. . . . . 6
⊢ ((𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → (𝐵𝑅𝐶 → ¬ 𝐶𝑅𝐵)) |
23 | 22 | imp 410 |
. . . . 5
⊢ (((𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) ∧ 𝐵𝑅𝐶) → ¬ 𝐶𝑅𝐵) |
24 | | sonr 5491 |
. . . . . . 7
⊢ ((𝑅 Or 𝐴 ∧ 𝐶 ∈ 𝐴) → ¬ 𝐶𝑅𝐶) |
25 | 24 | 3adant2 1133 |
. . . . . 6
⊢ ((𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → ¬ 𝐶𝑅𝐶) |
26 | 25 | adantr 484 |
. . . . 5
⊢ (((𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) ∧ ¬ 𝐵𝑅𝐶) → ¬ 𝐶𝑅𝐶) |
27 | 16, 18, 23, 26 | ifbothda 4477 |
. . . 4
⊢ ((𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → ¬ 𝐶𝑅if(𝐵𝑅𝐶, 𝐵, 𝐶)) |
28 | | breq1 5056 |
. . . . . . 7
⊢ (𝑦 = 𝐵 → (𝑦𝑅if(𝐵𝑅𝐶, 𝐵, 𝐶) ↔ 𝐵𝑅if(𝐵𝑅𝐶, 𝐵, 𝐶))) |
29 | 28 | notbid 321 |
. . . . . 6
⊢ (𝑦 = 𝐵 → (¬ 𝑦𝑅if(𝐵𝑅𝐶, 𝐵, 𝐶) ↔ ¬ 𝐵𝑅if(𝐵𝑅𝐶, 𝐵, 𝐶))) |
30 | | breq1 5056 |
. . . . . . 7
⊢ (𝑦 = 𝐶 → (𝑦𝑅if(𝐵𝑅𝐶, 𝐵, 𝐶) ↔ 𝐶𝑅if(𝐵𝑅𝐶, 𝐵, 𝐶))) |
31 | 30 | notbid 321 |
. . . . . 6
⊢ (𝑦 = 𝐶 → (¬ 𝑦𝑅if(𝐵𝑅𝐶, 𝐵, 𝐶) ↔ ¬ 𝐶𝑅if(𝐵𝑅𝐶, 𝐵, 𝐶))) |
32 | 29, 31 | ralprg 4610 |
. . . . 5
⊢ ((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → (∀𝑦 ∈ {𝐵, 𝐶} ¬ 𝑦𝑅if(𝐵𝑅𝐶, 𝐵, 𝐶) ↔ (¬ 𝐵𝑅if(𝐵𝑅𝐶, 𝐵, 𝐶) ∧ ¬ 𝐶𝑅if(𝐵𝑅𝐶, 𝐵, 𝐶)))) |
33 | 32 | 3adant1 1132 |
. . . 4
⊢ ((𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → (∀𝑦 ∈ {𝐵, 𝐶} ¬ 𝑦𝑅if(𝐵𝑅𝐶, 𝐵, 𝐶) ↔ (¬ 𝐵𝑅if(𝐵𝑅𝐶, 𝐵, 𝐶) ∧ ¬ 𝐶𝑅if(𝐵𝑅𝐶, 𝐵, 𝐶)))) |
34 | 14, 27, 33 | mpbir2and 713 |
. . 3
⊢ ((𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → ∀𝑦 ∈ {𝐵, 𝐶} ¬ 𝑦𝑅if(𝐵𝑅𝐶, 𝐵, 𝐶)) |
35 | 34 | r19.21bi 3130 |
. 2
⊢ (((𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) ∧ 𝑦 ∈ {𝐵, 𝐶}) → ¬ 𝑦𝑅if(𝐵𝑅𝐶, 𝐵, 𝐶)) |
36 | 1, 3, 5, 35 | infmin 9110 |
1
⊢ ((𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → inf({𝐵, 𝐶}, 𝐴, 𝑅) = if(𝐵𝑅𝐶, 𝐵, 𝐶)) |