| Step | Hyp | Ref
| Expression |
| 1 | | df-br 5144 |
. . 3
⊢ (𝐹(
≃ph‘𝐽)𝐺 ↔ 〈𝐹, 𝐺〉 ∈ (
≃ph‘𝐽)) |
| 2 | | df-phtpc 25024 |
. . . 4
⊢
≃ph = (𝑗 ∈ Top ↦ {〈𝑓, 𝑔〉 ∣ ({𝑓, 𝑔} ⊆ (II Cn 𝑗) ∧ (𝑓(PHtpy‘𝑗)𝑔) ≠ ∅)}) |
| 3 | 2 | mptrcl 7025 |
. . 3
⊢
(〈𝐹, 𝐺〉 ∈ (
≃ph‘𝐽) → 𝐽 ∈ Top) |
| 4 | 1, 3 | sylbi 217 |
. 2
⊢ (𝐹(
≃ph‘𝐽)𝐺 → 𝐽 ∈ Top) |
| 5 | | cntop2 23249 |
. . 3
⊢ (𝐹 ∈ (II Cn 𝐽) → 𝐽 ∈ Top) |
| 6 | 5 | 3ad2ant1 1134 |
. 2
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝐺 ∈ (II Cn 𝐽) ∧ (𝐹(PHtpy‘𝐽)𝐺) ≠ ∅) → 𝐽 ∈ Top) |
| 7 | | oveq2 7439 |
. . . . . . . . 9
⊢ (𝑗 = 𝐽 → (II Cn 𝑗) = (II Cn 𝐽)) |
| 8 | 7 | sseq2d 4016 |
. . . . . . . 8
⊢ (𝑗 = 𝐽 → ({𝑓, 𝑔} ⊆ (II Cn 𝑗) ↔ {𝑓, 𝑔} ⊆ (II Cn 𝐽))) |
| 9 | | vex 3484 |
. . . . . . . . 9
⊢ 𝑓 ∈ V |
| 10 | | vex 3484 |
. . . . . . . . 9
⊢ 𝑔 ∈ V |
| 11 | 9, 10 | prss 4820 |
. . . . . . . 8
⊢ ((𝑓 ∈ (II Cn 𝐽) ∧ 𝑔 ∈ (II Cn 𝐽)) ↔ {𝑓, 𝑔} ⊆ (II Cn 𝐽)) |
| 12 | 8, 11 | bitr4di 289 |
. . . . . . 7
⊢ (𝑗 = 𝐽 → ({𝑓, 𝑔} ⊆ (II Cn 𝑗) ↔ (𝑓 ∈ (II Cn 𝐽) ∧ 𝑔 ∈ (II Cn 𝐽)))) |
| 13 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑗 = 𝐽 → (PHtpy‘𝑗) = (PHtpy‘𝐽)) |
| 14 | 13 | oveqd 7448 |
. . . . . . . 8
⊢ (𝑗 = 𝐽 → (𝑓(PHtpy‘𝑗)𝑔) = (𝑓(PHtpy‘𝐽)𝑔)) |
| 15 | 14 | neeq1d 3000 |
. . . . . . 7
⊢ (𝑗 = 𝐽 → ((𝑓(PHtpy‘𝑗)𝑔) ≠ ∅ ↔ (𝑓(PHtpy‘𝐽)𝑔) ≠ ∅)) |
| 16 | 12, 15 | anbi12d 632 |
. . . . . 6
⊢ (𝑗 = 𝐽 → (({𝑓, 𝑔} ⊆ (II Cn 𝑗) ∧ (𝑓(PHtpy‘𝑗)𝑔) ≠ ∅) ↔ ((𝑓 ∈ (II Cn 𝐽) ∧ 𝑔 ∈ (II Cn 𝐽)) ∧ (𝑓(PHtpy‘𝐽)𝑔) ≠ ∅))) |
| 17 | 16 | opabbidv 5209 |
. . . . 5
⊢ (𝑗 = 𝐽 → {〈𝑓, 𝑔〉 ∣ ({𝑓, 𝑔} ⊆ (II Cn 𝑗) ∧ (𝑓(PHtpy‘𝑗)𝑔) ≠ ∅)} = {〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ (II Cn 𝐽) ∧ 𝑔 ∈ (II Cn 𝐽)) ∧ (𝑓(PHtpy‘𝐽)𝑔) ≠ ∅)}) |
| 18 | | ovex 7464 |
. . . . . . 7
⊢ (II Cn
𝐽) ∈
V |
| 19 | 18, 18 | xpex 7773 |
. . . . . 6
⊢ ((II Cn
𝐽) × (II Cn 𝐽)) ∈ V |
| 20 | | opabssxp 5778 |
. . . . . 6
⊢
{〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ (II Cn 𝐽) ∧ 𝑔 ∈ (II Cn 𝐽)) ∧ (𝑓(PHtpy‘𝐽)𝑔) ≠ ∅)} ⊆ ((II Cn 𝐽) × (II Cn 𝐽)) |
| 21 | 19, 20 | ssexi 5322 |
. . . . 5
⊢
{〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ (II Cn 𝐽) ∧ 𝑔 ∈ (II Cn 𝐽)) ∧ (𝑓(PHtpy‘𝐽)𝑔) ≠ ∅)} ∈ V |
| 22 | 17, 2, 21 | fvmpt 7016 |
. . . 4
⊢ (𝐽 ∈ Top → (
≃ph‘𝐽) = {〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ (II Cn 𝐽) ∧ 𝑔 ∈ (II Cn 𝐽)) ∧ (𝑓(PHtpy‘𝐽)𝑔) ≠ ∅)}) |
| 23 | 22 | breqd 5154 |
. . 3
⊢ (𝐽 ∈ Top → (𝐹(
≃ph‘𝐽)𝐺 ↔ 𝐹{〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ (II Cn 𝐽) ∧ 𝑔 ∈ (II Cn 𝐽)) ∧ (𝑓(PHtpy‘𝐽)𝑔) ≠ ∅)}𝐺)) |
| 24 | | oveq12 7440 |
. . . . . 6
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑓(PHtpy‘𝐽)𝑔) = (𝐹(PHtpy‘𝐽)𝐺)) |
| 25 | 24 | neeq1d 3000 |
. . . . 5
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ((𝑓(PHtpy‘𝐽)𝑔) ≠ ∅ ↔ (𝐹(PHtpy‘𝐽)𝐺) ≠ ∅)) |
| 26 | | eqid 2737 |
. . . . 5
⊢
{〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ (II Cn 𝐽) ∧ 𝑔 ∈ (II Cn 𝐽)) ∧ (𝑓(PHtpy‘𝐽)𝑔) ≠ ∅)} = {〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ (II Cn 𝐽) ∧ 𝑔 ∈ (II Cn 𝐽)) ∧ (𝑓(PHtpy‘𝐽)𝑔) ≠ ∅)} |
| 27 | 25, 26 | brab2a 5779 |
. . . 4
⊢ (𝐹{〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ (II Cn 𝐽) ∧ 𝑔 ∈ (II Cn 𝐽)) ∧ (𝑓(PHtpy‘𝐽)𝑔) ≠ ∅)}𝐺 ↔ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝐺 ∈ (II Cn 𝐽)) ∧ (𝐹(PHtpy‘𝐽)𝐺) ≠ ∅)) |
| 28 | | df-3an 1089 |
. . . 4
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝐺 ∈ (II Cn 𝐽) ∧ (𝐹(PHtpy‘𝐽)𝐺) ≠ ∅) ↔ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝐺 ∈ (II Cn 𝐽)) ∧ (𝐹(PHtpy‘𝐽)𝐺) ≠ ∅)) |
| 29 | 27, 28 | bitr4i 278 |
. . 3
⊢ (𝐹{〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ (II Cn 𝐽) ∧ 𝑔 ∈ (II Cn 𝐽)) ∧ (𝑓(PHtpy‘𝐽)𝑔) ≠ ∅)}𝐺 ↔ (𝐹 ∈ (II Cn 𝐽) ∧ 𝐺 ∈ (II Cn 𝐽) ∧ (𝐹(PHtpy‘𝐽)𝐺) ≠ ∅)) |
| 30 | 23, 29 | bitrdi 287 |
. 2
⊢ (𝐽 ∈ Top → (𝐹(
≃ph‘𝐽)𝐺 ↔ (𝐹 ∈ (II Cn 𝐽) ∧ 𝐺 ∈ (II Cn 𝐽) ∧ (𝐹(PHtpy‘𝐽)𝐺) ≠ ∅))) |
| 31 | 4, 6, 30 | pm5.21nii 378 |
1
⊢ (𝐹(
≃ph‘𝐽)𝐺 ↔ (𝐹 ∈ (II Cn 𝐽) ∧ 𝐺 ∈ (II Cn 𝐽) ∧ (𝐹(PHtpy‘𝐽)𝐺) ≠ ∅)) |