Step | Hyp | Ref
| Expression |
1 | | catprs.1 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 ↔ (𝑥𝐻𝑦) ≠ ∅)) |
2 | | breq1 5073 |
. . . . 5
⊢ (𝑥 = 𝑧 → (𝑥 ≤ 𝑦 ↔ 𝑧 ≤ 𝑦)) |
3 | | oveq1 7262 |
. . . . . 6
⊢ (𝑥 = 𝑧 → (𝑥𝐻𝑦) = (𝑧𝐻𝑦)) |
4 | 3 | neeq1d 3002 |
. . . . 5
⊢ (𝑥 = 𝑧 → ((𝑥𝐻𝑦) ≠ ∅ ↔ (𝑧𝐻𝑦) ≠ ∅)) |
5 | 2, 4 | bibi12d 345 |
. . . 4
⊢ (𝑥 = 𝑧 → ((𝑥 ≤ 𝑦 ↔ (𝑥𝐻𝑦) ≠ ∅) ↔ (𝑧 ≤ 𝑦 ↔ (𝑧𝐻𝑦) ≠ ∅))) |
6 | | breq2 5074 |
. . . . 5
⊢ (𝑦 = 𝑤 → (𝑧 ≤ 𝑦 ↔ 𝑧 ≤ 𝑤)) |
7 | | oveq2 7263 |
. . . . . 6
⊢ (𝑦 = 𝑤 → (𝑧𝐻𝑦) = (𝑧𝐻𝑤)) |
8 | 7 | neeq1d 3002 |
. . . . 5
⊢ (𝑦 = 𝑤 → ((𝑧𝐻𝑦) ≠ ∅ ↔ (𝑧𝐻𝑤) ≠ ∅)) |
9 | 6, 8 | bibi12d 345 |
. . . 4
⊢ (𝑦 = 𝑤 → ((𝑧 ≤ 𝑦 ↔ (𝑧𝐻𝑦) ≠ ∅) ↔ (𝑧 ≤ 𝑤 ↔ (𝑧𝐻𝑤) ≠ ∅))) |
10 | 5, 9 | cbvral2vw 3385 |
. . 3
⊢
(∀𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 ↔ (𝑥𝐻𝑦) ≠ ∅) ↔ ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (𝑧 ≤ 𝑤 ↔ (𝑧𝐻𝑤) ≠ ∅)) |
11 | 1, 10 | sylib 217 |
. 2
⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (𝑧 ≤ 𝑤 ↔ (𝑧𝐻𝑤) ≠ ∅)) |
12 | | catprslem.x |
. . 3
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
13 | | catprslem.y |
. . 3
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
14 | | breq12 5075 |
. . . . 5
⊢ ((𝑧 = 𝑋 ∧ 𝑤 = 𝑌) → (𝑧 ≤ 𝑤 ↔ 𝑋 ≤ 𝑌)) |
15 | | oveq12 7264 |
. . . . . 6
⊢ ((𝑧 = 𝑋 ∧ 𝑤 = 𝑌) → (𝑧𝐻𝑤) = (𝑋𝐻𝑌)) |
16 | 15 | neeq1d 3002 |
. . . . 5
⊢ ((𝑧 = 𝑋 ∧ 𝑤 = 𝑌) → ((𝑧𝐻𝑤) ≠ ∅ ↔ (𝑋𝐻𝑌) ≠ ∅)) |
17 | 14, 16 | bibi12d 345 |
. . . 4
⊢ ((𝑧 = 𝑋 ∧ 𝑤 = 𝑌) → ((𝑧 ≤ 𝑤 ↔ (𝑧𝐻𝑤) ≠ ∅) ↔ (𝑋 ≤ 𝑌 ↔ (𝑋𝐻𝑌) ≠ ∅))) |
18 | 17 | rspc2gv 3561 |
. . 3
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (𝑧 ≤ 𝑤 ↔ (𝑧𝐻𝑤) ≠ ∅) → (𝑋 ≤ 𝑌 ↔ (𝑋𝐻𝑌) ≠ ∅))) |
19 | 12, 13, 18 | syl2anc 583 |
. 2
⊢ (𝜑 → (∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (𝑧 ≤ 𝑤 ↔ (𝑧𝐻𝑤) ≠ ∅) → (𝑋 ≤ 𝑌 ↔ (𝑋𝐻𝑌) ≠ ∅))) |
20 | 11, 19 | mpd 15 |
1
⊢ (𝜑 → (𝑋 ≤ 𝑌 ↔ (𝑋𝐻𝑌) ≠ ∅)) |