Step | Hyp | Ref
| Expression |
1 | | breq 5055 |
. . . . . . 7
⊢ (𝑅 = 𝑆 → (𝑥𝑅𝑦 ↔ 𝑥𝑆𝑦)) |
2 | 1 | notbid 321 |
. . . . . 6
⊢ (𝑅 = 𝑆 → (¬ 𝑥𝑅𝑦 ↔ ¬ 𝑥𝑆𝑦)) |
3 | 2 | ralbidv 3118 |
. . . . 5
⊢ (𝑅 = 𝑆 → (∀𝑦 ∈ 𝐴 ¬ 𝑥𝑅𝑦 ↔ ∀𝑦 ∈ 𝐴 ¬ 𝑥𝑆𝑦)) |
4 | | breq 5055 |
. . . . . . 7
⊢ (𝑅 = 𝑆 → (𝑦𝑅𝑥 ↔ 𝑦𝑆𝑥)) |
5 | | breq 5055 |
. . . . . . . 8
⊢ (𝑅 = 𝑆 → (𝑦𝑅𝑧 ↔ 𝑦𝑆𝑧)) |
6 | 5 | rexbidv 3216 |
. . . . . . 7
⊢ (𝑅 = 𝑆 → (∃𝑧 ∈ 𝐴 𝑦𝑅𝑧 ↔ ∃𝑧 ∈ 𝐴 𝑦𝑆𝑧)) |
7 | 4, 6 | imbi12d 348 |
. . . . . 6
⊢ (𝑅 = 𝑆 → ((𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐴 𝑦𝑅𝑧) ↔ (𝑦𝑆𝑥 → ∃𝑧 ∈ 𝐴 𝑦𝑆𝑧))) |
8 | 7 | ralbidv 3118 |
. . . . 5
⊢ (𝑅 = 𝑆 → (∀𝑦 ∈ 𝐵 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐴 𝑦𝑅𝑧) ↔ ∀𝑦 ∈ 𝐵 (𝑦𝑆𝑥 → ∃𝑧 ∈ 𝐴 𝑦𝑆𝑧))) |
9 | 3, 8 | anbi12d 634 |
. . . 4
⊢ (𝑅 = 𝑆 → ((∀𝑦 ∈ 𝐴 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐵 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐴 𝑦𝑅𝑧)) ↔ (∀𝑦 ∈ 𝐴 ¬ 𝑥𝑆𝑦 ∧ ∀𝑦 ∈ 𝐵 (𝑦𝑆𝑥 → ∃𝑧 ∈ 𝐴 𝑦𝑆𝑧)))) |
10 | 9 | rabbidv 3390 |
. . 3
⊢ (𝑅 = 𝑆 → {𝑥 ∈ 𝐵 ∣ (∀𝑦 ∈ 𝐴 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐵 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐴 𝑦𝑅𝑧))} = {𝑥 ∈ 𝐵 ∣ (∀𝑦 ∈ 𝐴 ¬ 𝑥𝑆𝑦 ∧ ∀𝑦 ∈ 𝐵 (𝑦𝑆𝑥 → ∃𝑧 ∈ 𝐴 𝑦𝑆𝑧))}) |
11 | 10 | unieqd 4833 |
. 2
⊢ (𝑅 = 𝑆 → ∪ {𝑥 ∈ 𝐵 ∣ (∀𝑦 ∈ 𝐴 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐵 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐴 𝑦𝑅𝑧))} = ∪ {𝑥 ∈ 𝐵 ∣ (∀𝑦 ∈ 𝐴 ¬ 𝑥𝑆𝑦 ∧ ∀𝑦 ∈ 𝐵 (𝑦𝑆𝑥 → ∃𝑧 ∈ 𝐴 𝑦𝑆𝑧))}) |
12 | | df-sup 9058 |
. 2
⊢ sup(𝐴, 𝐵, 𝑅) = ∪ {𝑥 ∈ 𝐵 ∣ (∀𝑦 ∈ 𝐴 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐵 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐴 𝑦𝑅𝑧))} |
13 | | df-sup 9058 |
. 2
⊢ sup(𝐴, 𝐵, 𝑆) = ∪ {𝑥 ∈ 𝐵 ∣ (∀𝑦 ∈ 𝐴 ¬ 𝑥𝑆𝑦 ∧ ∀𝑦 ∈ 𝐵 (𝑦𝑆𝑥 → ∃𝑧 ∈ 𝐴 𝑦𝑆𝑧))} |
14 | 11, 12, 13 | 3eqtr4g 2803 |
1
⊢ (𝑅 = 𝑆 → sup(𝐴, 𝐵, 𝑅) = sup(𝐴, 𝐵, 𝑆)) |