Step | Hyp | Ref
| Expression |
1 | | df-br 5059 |
. . 3
⊢ (𝐹(
≃ph‘𝐽)𝐺 ↔ 〈𝐹, 𝐺〉 ∈ (
≃ph‘𝐽)) |
2 | | df-phtpc 23894 |
. . . 4
⊢
≃ph = (𝑗 ∈ Top ↦ {〈𝑓, 𝑔〉 ∣ ({𝑓, 𝑔} ⊆ (II Cn 𝑗) ∧ (𝑓(PHtpy‘𝑗)𝑔) ≠ ∅)}) |
3 | 2 | mptrcl 6832 |
. . 3
⊢
(〈𝐹, 𝐺〉 ∈ (
≃ph‘𝐽) → 𝐽 ∈ Top) |
4 | 1, 3 | sylbi 220 |
. 2
⊢ (𝐹(
≃ph‘𝐽)𝐺 → 𝐽 ∈ Top) |
5 | | cntop2 22143 |
. . 3
⊢ (𝐹 ∈ (II Cn 𝐽) → 𝐽 ∈ Top) |
6 | 5 | 3ad2ant1 1135 |
. 2
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝐺 ∈ (II Cn 𝐽) ∧ (𝐹(PHtpy‘𝐽)𝐺) ≠ ∅) → 𝐽 ∈ Top) |
7 | | oveq2 7226 |
. . . . . . . . 9
⊢ (𝑗 = 𝐽 → (II Cn 𝑗) = (II Cn 𝐽)) |
8 | 7 | sseq2d 3938 |
. . . . . . . 8
⊢ (𝑗 = 𝐽 → ({𝑓, 𝑔} ⊆ (II Cn 𝑗) ↔ {𝑓, 𝑔} ⊆ (II Cn 𝐽))) |
9 | | vex 3417 |
. . . . . . . . 9
⊢ 𝑓 ∈ V |
10 | | vex 3417 |
. . . . . . . . 9
⊢ 𝑔 ∈ V |
11 | 9, 10 | prss 4738 |
. . . . . . . 8
⊢ ((𝑓 ∈ (II Cn 𝐽) ∧ 𝑔 ∈ (II Cn 𝐽)) ↔ {𝑓, 𝑔} ⊆ (II Cn 𝐽)) |
12 | 8, 11 | bitr4di 292 |
. . . . . . 7
⊢ (𝑗 = 𝐽 → ({𝑓, 𝑔} ⊆ (II Cn 𝑗) ↔ (𝑓 ∈ (II Cn 𝐽) ∧ 𝑔 ∈ (II Cn 𝐽)))) |
13 | | fveq2 6722 |
. . . . . . . . 9
⊢ (𝑗 = 𝐽 → (PHtpy‘𝑗) = (PHtpy‘𝐽)) |
14 | 13 | oveqd 7235 |
. . . . . . . 8
⊢ (𝑗 = 𝐽 → (𝑓(PHtpy‘𝑗)𝑔) = (𝑓(PHtpy‘𝐽)𝑔)) |
15 | 14 | neeq1d 3000 |
. . . . . . 7
⊢ (𝑗 = 𝐽 → ((𝑓(PHtpy‘𝑗)𝑔) ≠ ∅ ↔ (𝑓(PHtpy‘𝐽)𝑔) ≠ ∅)) |
16 | 12, 15 | anbi12d 634 |
. . . . . 6
⊢ (𝑗 = 𝐽 → (({𝑓, 𝑔} ⊆ (II Cn 𝑗) ∧ (𝑓(PHtpy‘𝑗)𝑔) ≠ ∅) ↔ ((𝑓 ∈ (II Cn 𝐽) ∧ 𝑔 ∈ (II Cn 𝐽)) ∧ (𝑓(PHtpy‘𝐽)𝑔) ≠ ∅))) |
17 | 16 | opabbidv 5124 |
. . . . 5
⊢ (𝑗 = 𝐽 → {〈𝑓, 𝑔〉 ∣ ({𝑓, 𝑔} ⊆ (II Cn 𝑗) ∧ (𝑓(PHtpy‘𝑗)𝑔) ≠ ∅)} = {〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ (II Cn 𝐽) ∧ 𝑔 ∈ (II Cn 𝐽)) ∧ (𝑓(PHtpy‘𝐽)𝑔) ≠ ∅)}) |
18 | | ovex 7251 |
. . . . . . 7
⊢ (II Cn
𝐽) ∈
V |
19 | 18, 18 | xpex 7543 |
. . . . . 6
⊢ ((II Cn
𝐽) × (II Cn 𝐽)) ∈ V |
20 | | opabssxp 5645 |
. . . . . 6
⊢
{〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ (II Cn 𝐽) ∧ 𝑔 ∈ (II Cn 𝐽)) ∧ (𝑓(PHtpy‘𝐽)𝑔) ≠ ∅)} ⊆ ((II Cn 𝐽) × (II Cn 𝐽)) |
21 | 19, 20 | ssexi 5220 |
. . . . 5
⊢
{〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ (II Cn 𝐽) ∧ 𝑔 ∈ (II Cn 𝐽)) ∧ (𝑓(PHtpy‘𝐽)𝑔) ≠ ∅)} ∈ V |
22 | 17, 2, 21 | fvmpt 6823 |
. . . 4
⊢ (𝐽 ∈ Top → (
≃ph‘𝐽) = {〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ (II Cn 𝐽) ∧ 𝑔 ∈ (II Cn 𝐽)) ∧ (𝑓(PHtpy‘𝐽)𝑔) ≠ ∅)}) |
23 | 22 | breqd 5069 |
. . 3
⊢ (𝐽 ∈ Top → (𝐹(
≃ph‘𝐽)𝐺 ↔ 𝐹{〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ (II Cn 𝐽) ∧ 𝑔 ∈ (II Cn 𝐽)) ∧ (𝑓(PHtpy‘𝐽)𝑔) ≠ ∅)}𝐺)) |
24 | | oveq12 7227 |
. . . . . 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 5646 |
. . . 4
⊢ (𝐹{〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ (II Cn 𝐽) ∧ 𝑔 ∈ (II Cn 𝐽)) ∧ (𝑓(PHtpy‘𝐽)𝑔) ≠ ∅)}𝐺 ↔ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝐺 ∈ (II Cn 𝐽)) ∧ (𝐹(PHtpy‘𝐽)𝐺) ≠ ∅)) |
28 | | df-3an 1091 |
. . . 4
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝐺 ∈ (II Cn 𝐽) ∧ (𝐹(PHtpy‘𝐽)𝐺) ≠ ∅) ↔ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝐺 ∈ (II Cn 𝐽)) ∧ (𝐹(PHtpy‘𝐽)𝐺) ≠ ∅)) |
29 | 27, 28 | bitr4i 281 |
. . 3
⊢ (𝐹{〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ (II Cn 𝐽) ∧ 𝑔 ∈ (II Cn 𝐽)) ∧ (𝑓(PHtpy‘𝐽)𝑔) ≠ ∅)}𝐺 ↔ (𝐹 ∈ (II Cn 𝐽) ∧ 𝐺 ∈ (II Cn 𝐽) ∧ (𝐹(PHtpy‘𝐽)𝐺) ≠ ∅)) |
30 | 23, 29 | bitrdi 290 |
. 2
⊢ (𝐽 ∈ Top → (𝐹(
≃ph‘𝐽)𝐺 ↔ (𝐹 ∈ (II Cn 𝐽) ∧ 𝐺 ∈ (II Cn 𝐽) ∧ (𝐹(PHtpy‘𝐽)𝐺) ≠ ∅))) |
31 | 4, 6, 30 | pm5.21nii 383 |
1
⊢ (𝐹(
≃ph‘𝐽)𝐺 ↔ (𝐹 ∈ (II Cn 𝐽) ∧ 𝐺 ∈ (II Cn 𝐽) ∧ (𝐹(PHtpy‘𝐽)𝐺) ≠ ∅)) |