Step | Hyp | Ref
| Expression |
1 | | df-br 5107 |
. . 3
⊢ (𝐹(
≃ph‘𝐽)𝐺 ↔ ⟨𝐹, 𝐺⟩ ∈ (
≃ph‘𝐽)) |
2 | | df-phtpc 24371 |
. . . 4
⊢
≃ph = (𝑗 ∈ Top ↦ {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ (II Cn 𝑗) ∧ (𝑓(PHtpy‘𝑗)𝑔) ≠ ∅)}) |
3 | 2 | mptrcl 6958 |
. . 3
⊢
(⟨𝐹, 𝐺⟩ ∈ (
≃ph‘𝐽) → 𝐽 ∈ Top) |
4 | 1, 3 | sylbi 216 |
. 2
⊢ (𝐹(
≃ph‘𝐽)𝐺 → 𝐽 ∈ Top) |
5 | | cntop2 22608 |
. . 3
⊢ (𝐹 ∈ (II Cn 𝐽) → 𝐽 ∈ Top) |
6 | 5 | 3ad2ant1 1134 |
. 2
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝐺 ∈ (II Cn 𝐽) ∧ (𝐹(PHtpy‘𝐽)𝐺) ≠ ∅) → 𝐽 ∈ Top) |
7 | | oveq2 7366 |
. . . . . . . . 9
⊢ (𝑗 = 𝐽 → (II Cn 𝑗) = (II Cn 𝐽)) |
8 | 7 | sseq2d 3977 |
. . . . . . . 8
⊢ (𝑗 = 𝐽 → ({𝑓, 𝑔} ⊆ (II Cn 𝑗) ↔ {𝑓, 𝑔} ⊆ (II Cn 𝐽))) |
9 | | vex 3448 |
. . . . . . . . 9
⊢ 𝑓 ∈ V |
10 | | vex 3448 |
. . . . . . . . 9
⊢ 𝑔 ∈ V |
11 | 9, 10 | prss 4781 |
. . . . . . . 8
⊢ ((𝑓 ∈ (II Cn 𝐽) ∧ 𝑔 ∈ (II Cn 𝐽)) ↔ {𝑓, 𝑔} ⊆ (II Cn 𝐽)) |
12 | 8, 11 | bitr4di 289 |
. . . . . . 7
⊢ (𝑗 = 𝐽 → ({𝑓, 𝑔} ⊆ (II Cn 𝑗) ↔ (𝑓 ∈ (II Cn 𝐽) ∧ 𝑔 ∈ (II Cn 𝐽)))) |
13 | | fveq2 6843 |
. . . . . . . . 9
⊢ (𝑗 = 𝐽 → (PHtpy‘𝑗) = (PHtpy‘𝐽)) |
14 | 13 | oveqd 7375 |
. . . . . . . 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 5172 |
. . . . 5
⊢ (𝑗 = 𝐽 → {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ (II Cn 𝑗) ∧ (𝑓(PHtpy‘𝑗)𝑔) ≠ ∅)} = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (II Cn 𝐽) ∧ 𝑔 ∈ (II Cn 𝐽)) ∧ (𝑓(PHtpy‘𝐽)𝑔) ≠ ∅)}) |
18 | | ovex 7391 |
. . . . . . 7
⊢ (II Cn
𝐽) ∈
V |
19 | 18, 18 | xpex 7688 |
. . . . . 6
⊢ ((II Cn
𝐽) × (II Cn 𝐽)) ∈ V |
20 | | opabssxp 5725 |
. . . . . 6
⊢
{⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (II Cn 𝐽) ∧ 𝑔 ∈ (II Cn 𝐽)) ∧ (𝑓(PHtpy‘𝐽)𝑔) ≠ ∅)} ⊆ ((II Cn 𝐽) × (II Cn 𝐽)) |
21 | 19, 20 | ssexi 5280 |
. . . . 5
⊢
{⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (II Cn 𝐽) ∧ 𝑔 ∈ (II Cn 𝐽)) ∧ (𝑓(PHtpy‘𝐽)𝑔) ≠ ∅)} ∈ V |
22 | 17, 2, 21 | fvmpt 6949 |
. . . 4
⊢ (𝐽 ∈ Top → (
≃ph‘𝐽) = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (II Cn 𝐽) ∧ 𝑔 ∈ (II Cn 𝐽)) ∧ (𝑓(PHtpy‘𝐽)𝑔) ≠ ∅)}) |
23 | 22 | breqd 5117 |
. . 3
⊢ (𝐽 ∈ Top → (𝐹(
≃ph‘𝐽)𝐺 ↔ 𝐹{⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (II Cn 𝐽) ∧ 𝑔 ∈ (II Cn 𝐽)) ∧ (𝑓(PHtpy‘𝐽)𝑔) ≠ ∅)}𝐺)) |
24 | | oveq12 7367 |
. . . . . 6
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑓(PHtpy‘𝐽)𝑔) = (𝐹(PHtpy‘𝐽)𝐺)) |
25 | 24 | neeq1d 3000 |
. . . . 5
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ((𝑓(PHtpy‘𝐽)𝑔) ≠ ∅ ↔ (𝐹(PHtpy‘𝐽)𝐺) ≠ ∅)) |
26 | | eqid 2733 |
. . . . 5
⊢
{⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (II Cn 𝐽) ∧ 𝑔 ∈ (II Cn 𝐽)) ∧ (𝑓(PHtpy‘𝐽)𝑔) ≠ ∅)} = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (II Cn 𝐽) ∧ 𝑔 ∈ (II Cn 𝐽)) ∧ (𝑓(PHtpy‘𝐽)𝑔) ≠ ∅)} |
27 | 25, 26 | brab2a 5726 |
. . . 4
⊢ (𝐹{⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (II Cn 𝐽) ∧ 𝑔 ∈ (II Cn 𝐽)) ∧ (𝑓(PHtpy‘𝐽)𝑔) ≠ ∅)}𝐺 ↔ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝐺 ∈ (II Cn 𝐽)) ∧ (𝐹(PHtpy‘𝐽)𝐺) ≠ ∅)) |
28 | | df-3an 1090 |
. . . 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 380 |
1
⊢ (𝐹(
≃ph‘𝐽)𝐺 ↔ (𝐹 ∈ (II Cn 𝐽) ∧ 𝐺 ∈ (II Cn 𝐽) ∧ (𝐹(PHtpy‘𝐽)𝐺) ≠ ∅)) |