Proof of Theorem eqinf
Step | Hyp | Ref
| Expression |
1 | | df-inf 9059 |
. . 3
⊢ inf(𝐵, 𝐴, 𝑅) = sup(𝐵, 𝐴, ◡𝑅) |
2 | | infexd.1 |
. . . . . 6
⊢ (𝜑 → 𝑅 Or 𝐴) |
3 | | cnvso 6151 |
. . . . . 6
⊢ (𝑅 Or 𝐴 ↔ ◡𝑅 Or 𝐴) |
4 | 2, 3 | sylib 221 |
. . . . 5
⊢ (𝜑 → ◡𝑅 Or 𝐴) |
5 | 4 | eqsup 9072 |
. . . 4
⊢ (𝜑 → ((𝐶 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝐶◡𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦◡𝑅𝐶 → ∃𝑧 ∈ 𝐵 𝑦◡𝑅𝑧)) → sup(𝐵, 𝐴, ◡𝑅) = 𝐶)) |
6 | | brcnvg 5748 |
. . . . . . . . . . . 12
⊢ ((𝐶 ∈ 𝐴 ∧ 𝑦 ∈ V) → (𝐶◡𝑅𝑦 ↔ 𝑦𝑅𝐶)) |
7 | 6 | bicomd 226 |
. . . . . . . . . . 11
⊢ ((𝐶 ∈ 𝐴 ∧ 𝑦 ∈ V) → (𝑦𝑅𝐶 ↔ 𝐶◡𝑅𝑦)) |
8 | 7 | elvd 3415 |
. . . . . . . . . 10
⊢ (𝐶 ∈ 𝐴 → (𝑦𝑅𝐶 ↔ 𝐶◡𝑅𝑦)) |
9 | 8 | notbid 321 |
. . . . . . . . 9
⊢ (𝐶 ∈ 𝐴 → (¬ 𝑦𝑅𝐶 ↔ ¬ 𝐶◡𝑅𝑦)) |
10 | 9 | ralbidv 3118 |
. . . . . . . 8
⊢ (𝐶 ∈ 𝐴 → (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝐶 ↔ ∀𝑦 ∈ 𝐵 ¬ 𝐶◡𝑅𝑦)) |
11 | | vex 3412 |
. . . . . . . . . . . 12
⊢ 𝑦 ∈ V |
12 | | brcnvg 5748 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ V ∧ 𝐶 ∈ 𝐴) → (𝑦◡𝑅𝐶 ↔ 𝐶𝑅𝑦)) |
13 | 11, 12 | mpan 690 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ 𝐴 → (𝑦◡𝑅𝐶 ↔ 𝐶𝑅𝑦)) |
14 | 13 | bicomd 226 |
. . . . . . . . . 10
⊢ (𝐶 ∈ 𝐴 → (𝐶𝑅𝑦 ↔ 𝑦◡𝑅𝐶)) |
15 | | vex 3412 |
. . . . . . . . . . . . . 14
⊢ 𝑧 ∈ V |
16 | 11, 15 | brcnv 5751 |
. . . . . . . . . . . . 13
⊢ (𝑦◡𝑅𝑧 ↔ 𝑧𝑅𝑦) |
17 | 16 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝐶 ∈ 𝐴 → (𝑦◡𝑅𝑧 ↔ 𝑧𝑅𝑦)) |
18 | 17 | bicomd 226 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ 𝐴 → (𝑧𝑅𝑦 ↔ 𝑦◡𝑅𝑧)) |
19 | 18 | rexbidv 3216 |
. . . . . . . . . 10
⊢ (𝐶 ∈ 𝐴 → (∃𝑧 ∈ 𝐵 𝑧𝑅𝑦 ↔ ∃𝑧 ∈ 𝐵 𝑦◡𝑅𝑧)) |
20 | 14, 19 | imbi12d 348 |
. . . . . . . . 9
⊢ (𝐶 ∈ 𝐴 → ((𝐶𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦) ↔ (𝑦◡𝑅𝐶 → ∃𝑧 ∈ 𝐵 𝑦◡𝑅𝑧))) |
21 | 20 | ralbidv 3118 |
. . . . . . . 8
⊢ (𝐶 ∈ 𝐴 → (∀𝑦 ∈ 𝐴 (𝐶𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦) ↔ ∀𝑦 ∈ 𝐴 (𝑦◡𝑅𝐶 → ∃𝑧 ∈ 𝐵 𝑦◡𝑅𝑧))) |
22 | 10, 21 | anbi12d 634 |
. . . . . . 7
⊢ (𝐶 ∈ 𝐴 → ((∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝐶 ∧ ∀𝑦 ∈ 𝐴 (𝐶𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦)) ↔ (∀𝑦 ∈ 𝐵 ¬ 𝐶◡𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦◡𝑅𝐶 → ∃𝑧 ∈ 𝐵 𝑦◡𝑅𝑧)))) |
23 | 22 | pm5.32i 578 |
. . . . . 6
⊢ ((𝐶 ∈ 𝐴 ∧ (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝐶 ∧ ∀𝑦 ∈ 𝐴 (𝐶𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦))) ↔ (𝐶 ∈ 𝐴 ∧ (∀𝑦 ∈ 𝐵 ¬ 𝐶◡𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦◡𝑅𝐶 → ∃𝑧 ∈ 𝐵 𝑦◡𝑅𝑧)))) |
24 | | 3anass 1097 |
. . . . . 6
⊢ ((𝐶 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝐶 ∧ ∀𝑦 ∈ 𝐴 (𝐶𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦)) ↔ (𝐶 ∈ 𝐴 ∧ (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝐶 ∧ ∀𝑦 ∈ 𝐴 (𝐶𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦)))) |
25 | | 3anass 1097 |
. . . . . 6
⊢ ((𝐶 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝐶◡𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦◡𝑅𝐶 → ∃𝑧 ∈ 𝐵 𝑦◡𝑅𝑧)) ↔ (𝐶 ∈ 𝐴 ∧ (∀𝑦 ∈ 𝐵 ¬ 𝐶◡𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦◡𝑅𝐶 → ∃𝑧 ∈ 𝐵 𝑦◡𝑅𝑧)))) |
26 | 23, 24, 25 | 3bitr4i 306 |
. . . . 5
⊢ ((𝐶 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝐶 ∧ ∀𝑦 ∈ 𝐴 (𝐶𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦)) ↔ (𝐶 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝐶◡𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦◡𝑅𝐶 → ∃𝑧 ∈ 𝐵 𝑦◡𝑅𝑧))) |
27 | 26 | biimpi 219 |
. . . 4
⊢ ((𝐶 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝐶 ∧ ∀𝑦 ∈ 𝐴 (𝐶𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦)) → (𝐶 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝐶◡𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦◡𝑅𝐶 → ∃𝑧 ∈ 𝐵 𝑦◡𝑅𝑧))) |
28 | 5, 27 | impel 509 |
. . 3
⊢ ((𝜑 ∧ (𝐶 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝐶 ∧ ∀𝑦 ∈ 𝐴 (𝐶𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦))) → sup(𝐵, 𝐴, ◡𝑅) = 𝐶) |
29 | 1, 28 | eqtrid 2789 |
. 2
⊢ ((𝜑 ∧ (𝐶 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝐶 ∧ ∀𝑦 ∈ 𝐴 (𝐶𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦))) → inf(𝐵, 𝐴, 𝑅) = 𝐶) |
30 | 29 | ex 416 |
1
⊢ (𝜑 → ((𝐶 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝐶 ∧ ∀𝑦 ∈ 𝐴 (𝐶𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦)) → inf(𝐵, 𝐴, 𝑅) = 𝐶)) |