Step | Hyp | Ref
| Expression |
1 | | df-br 4874 |
. . 3
⊢ (𝐹(
≃ph‘𝐽)𝐺 ↔ 〈𝐹, 𝐺〉 ∈ (
≃ph‘𝐽)) |
2 | | df-phtpc 23161 |
. . . . 5
⊢
≃ph = (𝑗 ∈ Top ↦ {〈𝑓, 𝑔〉 ∣ ({𝑓, 𝑔} ⊆ (II Cn 𝑗) ∧ (𝑓(PHtpy‘𝑗)𝑔) ≠ ∅)}) |
3 | 2 | dmmptss 5872 |
. . . 4
⊢ dom
≃ph ⊆ Top |
4 | | elfvdm 6465 |
. . . 4
⊢
(〈𝐹, 𝐺〉 ∈ (
≃ph‘𝐽) → 𝐽 ∈ dom
≃ph) |
5 | 3, 4 | sseldi 3825 |
. . 3
⊢
(〈𝐹, 𝐺〉 ∈ (
≃ph‘𝐽) → 𝐽 ∈ Top) |
6 | 1, 5 | sylbi 209 |
. 2
⊢ (𝐹(
≃ph‘𝐽)𝐺 → 𝐽 ∈ Top) |
7 | | cntop2 21416 |
. . 3
⊢ (𝐹 ∈ (II Cn 𝐽) → 𝐽 ∈ Top) |
8 | 7 | 3ad2ant1 1167 |
. 2
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝐺 ∈ (II Cn 𝐽) ∧ (𝐹(PHtpy‘𝐽)𝐺) ≠ ∅) → 𝐽 ∈ Top) |
9 | | oveq2 6913 |
. . . . . . . . 9
⊢ (𝑗 = 𝐽 → (II Cn 𝑗) = (II Cn 𝐽)) |
10 | 9 | sseq2d 3858 |
. . . . . . . 8
⊢ (𝑗 = 𝐽 → ({𝑓, 𝑔} ⊆ (II Cn 𝑗) ↔ {𝑓, 𝑔} ⊆ (II Cn 𝐽))) |
11 | | vex 3417 |
. . . . . . . . 9
⊢ 𝑓 ∈ V |
12 | | vex 3417 |
. . . . . . . . 9
⊢ 𝑔 ∈ V |
13 | 11, 12 | prss 4569 |
. . . . . . . 8
⊢ ((𝑓 ∈ (II Cn 𝐽) ∧ 𝑔 ∈ (II Cn 𝐽)) ↔ {𝑓, 𝑔} ⊆ (II Cn 𝐽)) |
14 | 10, 13 | syl6bbr 281 |
. . . . . . 7
⊢ (𝑗 = 𝐽 → ({𝑓, 𝑔} ⊆ (II Cn 𝑗) ↔ (𝑓 ∈ (II Cn 𝐽) ∧ 𝑔 ∈ (II Cn 𝐽)))) |
15 | | fveq2 6433 |
. . . . . . . . 9
⊢ (𝑗 = 𝐽 → (PHtpy‘𝑗) = (PHtpy‘𝐽)) |
16 | 15 | oveqd 6922 |
. . . . . . . 8
⊢ (𝑗 = 𝐽 → (𝑓(PHtpy‘𝑗)𝑔) = (𝑓(PHtpy‘𝐽)𝑔)) |
17 | 16 | neeq1d 3058 |
. . . . . . 7
⊢ (𝑗 = 𝐽 → ((𝑓(PHtpy‘𝑗)𝑔) ≠ ∅ ↔ (𝑓(PHtpy‘𝐽)𝑔) ≠ ∅)) |
18 | 14, 17 | anbi12d 624 |
. . . . . 6
⊢ (𝑗 = 𝐽 → (({𝑓, 𝑔} ⊆ (II Cn 𝑗) ∧ (𝑓(PHtpy‘𝑗)𝑔) ≠ ∅) ↔ ((𝑓 ∈ (II Cn 𝐽) ∧ 𝑔 ∈ (II Cn 𝐽)) ∧ (𝑓(PHtpy‘𝐽)𝑔) ≠ ∅))) |
19 | 18 | opabbidv 4939 |
. . . . 5
⊢ (𝑗 = 𝐽 → {〈𝑓, 𝑔〉 ∣ ({𝑓, 𝑔} ⊆ (II Cn 𝑗) ∧ (𝑓(PHtpy‘𝑗)𝑔) ≠ ∅)} = {〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ (II Cn 𝐽) ∧ 𝑔 ∈ (II Cn 𝐽)) ∧ (𝑓(PHtpy‘𝐽)𝑔) ≠ ∅)}) |
20 | | ovex 6937 |
. . . . . . 7
⊢ (II Cn
𝐽) ∈
V |
21 | 20, 20 | xpex 7223 |
. . . . . 6
⊢ ((II Cn
𝐽) × (II Cn 𝐽)) ∈ V |
22 | | opabssxp 5428 |
. . . . . 6
⊢
{〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ (II Cn 𝐽) ∧ 𝑔 ∈ (II Cn 𝐽)) ∧ (𝑓(PHtpy‘𝐽)𝑔) ≠ ∅)} ⊆ ((II Cn 𝐽) × (II Cn 𝐽)) |
23 | 21, 22 | ssexi 5028 |
. . . . 5
⊢
{〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ (II Cn 𝐽) ∧ 𝑔 ∈ (II Cn 𝐽)) ∧ (𝑓(PHtpy‘𝐽)𝑔) ≠ ∅)} ∈ V |
24 | 19, 2, 23 | fvmpt 6529 |
. . . 4
⊢ (𝐽 ∈ Top → (
≃ph‘𝐽) = {〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ (II Cn 𝐽) ∧ 𝑔 ∈ (II Cn 𝐽)) ∧ (𝑓(PHtpy‘𝐽)𝑔) ≠ ∅)}) |
25 | 24 | breqd 4884 |
. . 3
⊢ (𝐽 ∈ Top → (𝐹(
≃ph‘𝐽)𝐺 ↔ 𝐹{〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ (II Cn 𝐽) ∧ 𝑔 ∈ (II Cn 𝐽)) ∧ (𝑓(PHtpy‘𝐽)𝑔) ≠ ∅)}𝐺)) |
26 | | oveq12 6914 |
. . . . . 6
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑓(PHtpy‘𝐽)𝑔) = (𝐹(PHtpy‘𝐽)𝐺)) |
27 | 26 | neeq1d 3058 |
. . . . 5
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ((𝑓(PHtpy‘𝐽)𝑔) ≠ ∅ ↔ (𝐹(PHtpy‘𝐽)𝐺) ≠ ∅)) |
28 | | eqid 2825 |
. . . . 5
⊢
{〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ (II Cn 𝐽) ∧ 𝑔 ∈ (II Cn 𝐽)) ∧ (𝑓(PHtpy‘𝐽)𝑔) ≠ ∅)} = {〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ (II Cn 𝐽) ∧ 𝑔 ∈ (II Cn 𝐽)) ∧ (𝑓(PHtpy‘𝐽)𝑔) ≠ ∅)} |
29 | 27, 28 | brab2a 5429 |
. . . 4
⊢ (𝐹{〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ (II Cn 𝐽) ∧ 𝑔 ∈ (II Cn 𝐽)) ∧ (𝑓(PHtpy‘𝐽)𝑔) ≠ ∅)}𝐺 ↔ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝐺 ∈ (II Cn 𝐽)) ∧ (𝐹(PHtpy‘𝐽)𝐺) ≠ ∅)) |
30 | | df-3an 1113 |
. . . 4
⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝐺 ∈ (II Cn 𝐽) ∧ (𝐹(PHtpy‘𝐽)𝐺) ≠ ∅) ↔ ((𝐹 ∈ (II Cn 𝐽) ∧ 𝐺 ∈ (II Cn 𝐽)) ∧ (𝐹(PHtpy‘𝐽)𝐺) ≠ ∅)) |
31 | 29, 30 | bitr4i 270 |
. . 3
⊢ (𝐹{〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ (II Cn 𝐽) ∧ 𝑔 ∈ (II Cn 𝐽)) ∧ (𝑓(PHtpy‘𝐽)𝑔) ≠ ∅)}𝐺 ↔ (𝐹 ∈ (II Cn 𝐽) ∧ 𝐺 ∈ (II Cn 𝐽) ∧ (𝐹(PHtpy‘𝐽)𝐺) ≠ ∅)) |
32 | 25, 31 | syl6bb 279 |
. 2
⊢ (𝐽 ∈ Top → (𝐹(
≃ph‘𝐽)𝐺 ↔ (𝐹 ∈ (II Cn 𝐽) ∧ 𝐺 ∈ (II Cn 𝐽) ∧ (𝐹(PHtpy‘𝐽)𝐺) ≠ ∅))) |
33 | 6, 8, 32 | pm5.21nii 370 |
1
⊢ (𝐹(
≃ph‘𝐽)𝐺 ↔ (𝐹 ∈ (II Cn 𝐽) ∧ 𝐺 ∈ (II Cn 𝐽) ∧ (𝐹(PHtpy‘𝐽)𝐺) ≠ ∅)) |