Step | Hyp | Ref
| Expression |
1 | | isphtpy.2 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽)) |
2 | | cntop2 21045 |
. . . . 5
⊢ (𝐹 ∈ (II Cn 𝐽) → 𝐽 ∈ Top) |
3 | | oveq2 6658 |
. . . . . . 7
⊢ (𝑗 = 𝐽 → (II Cn 𝑗) = (II Cn 𝐽)) |
4 | | oveq2 6658 |
. . . . . . . . 9
⊢ (𝑗 = 𝐽 → (II Htpy 𝑗) = (II Htpy 𝐽)) |
5 | 4 | oveqd 6667 |
. . . . . . . 8
⊢ (𝑗 = 𝐽 → (𝑓(II Htpy 𝑗)𝑔) = (𝑓(II Htpy 𝐽)𝑔)) |
6 | | rabeq 3192 |
. . . . . . . 8
⊢ ((𝑓(II Htpy 𝑗)𝑔) = (𝑓(II Htpy 𝐽)𝑔) → {ℎ ∈ (𝑓(II Htpy 𝑗)𝑔) ∣ ∀𝑠 ∈ (0[,]1)((0ℎ𝑠) = (𝑓‘0) ∧ (1ℎ𝑠) = (𝑓‘1))} = {ℎ ∈ (𝑓(II Htpy 𝐽)𝑔) ∣ ∀𝑠 ∈ (0[,]1)((0ℎ𝑠) = (𝑓‘0) ∧ (1ℎ𝑠) = (𝑓‘1))}) |
7 | 5, 6 | syl 17 |
. . . . . . 7
⊢ (𝑗 = 𝐽 → {ℎ ∈ (𝑓(II Htpy 𝑗)𝑔) ∣ ∀𝑠 ∈ (0[,]1)((0ℎ𝑠) = (𝑓‘0) ∧ (1ℎ𝑠) = (𝑓‘1))} = {ℎ ∈ (𝑓(II Htpy 𝐽)𝑔) ∣ ∀𝑠 ∈ (0[,]1)((0ℎ𝑠) = (𝑓‘0) ∧ (1ℎ𝑠) = (𝑓‘1))}) |
8 | 3, 3, 7 | mpt2eq123dv 6717 |
. . . . . 6
⊢ (𝑗 = 𝐽 → (𝑓 ∈ (II Cn 𝑗), 𝑔 ∈ (II Cn 𝑗) ↦ {ℎ ∈ (𝑓(II Htpy 𝑗)𝑔) ∣ ∀𝑠 ∈ (0[,]1)((0ℎ𝑠) = (𝑓‘0) ∧ (1ℎ𝑠) = (𝑓‘1))}) = (𝑓 ∈ (II Cn 𝐽), 𝑔 ∈ (II Cn 𝐽) ↦ {ℎ ∈ (𝑓(II Htpy 𝐽)𝑔) ∣ ∀𝑠 ∈ (0[,]1)((0ℎ𝑠) = (𝑓‘0) ∧ (1ℎ𝑠) = (𝑓‘1))})) |
9 | | df-phtpy 22770 |
. . . . . 6
⊢ PHtpy =
(𝑗 ∈ Top ↦
(𝑓 ∈ (II Cn 𝑗), 𝑔 ∈ (II Cn 𝑗) ↦ {ℎ ∈ (𝑓(II Htpy 𝑗)𝑔) ∣ ∀𝑠 ∈ (0[,]1)((0ℎ𝑠) = (𝑓‘0) ∧ (1ℎ𝑠) = (𝑓‘1))})) |
10 | | ovex 6678 |
. . . . . . 7
⊢ (II Cn
𝐽) ∈
V |
11 | 10, 10 | mpt2ex 7247 |
. . . . . 6
⊢ (𝑓 ∈ (II Cn 𝐽), 𝑔 ∈ (II Cn 𝐽) ↦ {ℎ ∈ (𝑓(II Htpy 𝐽)𝑔) ∣ ∀𝑠 ∈ (0[,]1)((0ℎ𝑠) = (𝑓‘0) ∧ (1ℎ𝑠) = (𝑓‘1))}) ∈ V |
12 | 8, 9, 11 | fvmpt 6282 |
. . . . 5
⊢ (𝐽 ∈ Top →
(PHtpy‘𝐽) = (𝑓 ∈ (II Cn 𝐽), 𝑔 ∈ (II Cn 𝐽) ↦ {ℎ ∈ (𝑓(II Htpy 𝐽)𝑔) ∣ ∀𝑠 ∈ (0[,]1)((0ℎ𝑠) = (𝑓‘0) ∧ (1ℎ𝑠) = (𝑓‘1))})) |
13 | 1, 2, 12 | 3syl 18 |
. . . 4
⊢ (𝜑 → (PHtpy‘𝐽) = (𝑓 ∈ (II Cn 𝐽), 𝑔 ∈ (II Cn 𝐽) ↦ {ℎ ∈ (𝑓(II Htpy 𝐽)𝑔) ∣ ∀𝑠 ∈ (0[,]1)((0ℎ𝑠) = (𝑓‘0) ∧ (1ℎ𝑠) = (𝑓‘1))})) |
14 | | oveq12 6659 |
. . . . . 6
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑓(II Htpy 𝐽)𝑔) = (𝐹(II Htpy 𝐽)𝐺)) |
15 | | simpl 473 |
. . . . . . . . . 10
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → 𝑓 = 𝐹) |
16 | 15 | fveq1d 6193 |
. . . . . . . . 9
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑓‘0) = (𝐹‘0)) |
17 | 16 | eqeq2d 2632 |
. . . . . . . 8
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ((0ℎ𝑠) = (𝑓‘0) ↔ (0ℎ𝑠) = (𝐹‘0))) |
18 | 15 | fveq1d 6193 |
. . . . . . . . 9
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑓‘1) = (𝐹‘1)) |
19 | 18 | eqeq2d 2632 |
. . . . . . . 8
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ((1ℎ𝑠) = (𝑓‘1) ↔ (1ℎ𝑠) = (𝐹‘1))) |
20 | 17, 19 | anbi12d 747 |
. . . . . . 7
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (((0ℎ𝑠) = (𝑓‘0) ∧ (1ℎ𝑠) = (𝑓‘1)) ↔ ((0ℎ𝑠) = (𝐹‘0) ∧ (1ℎ𝑠) = (𝐹‘1)))) |
21 | 20 | ralbidv 2986 |
. . . . . 6
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (∀𝑠 ∈ (0[,]1)((0ℎ𝑠) = (𝑓‘0) ∧ (1ℎ𝑠) = (𝑓‘1)) ↔ ∀𝑠 ∈ (0[,]1)((0ℎ𝑠) = (𝐹‘0) ∧ (1ℎ𝑠) = (𝐹‘1)))) |
22 | 14, 21 | rabeqbidv 3195 |
. . . . 5
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → {ℎ ∈ (𝑓(II Htpy 𝐽)𝑔) ∣ ∀𝑠 ∈ (0[,]1)((0ℎ𝑠) = (𝑓‘0) ∧ (1ℎ𝑠) = (𝑓‘1))} = {ℎ ∈ (𝐹(II Htpy 𝐽)𝐺) ∣ ∀𝑠 ∈ (0[,]1)((0ℎ𝑠) = (𝐹‘0) ∧ (1ℎ𝑠) = (𝐹‘1))}) |
23 | 22 | adantl 482 |
. . . 4
⊢ ((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑔 = 𝐺)) → {ℎ ∈ (𝑓(II Htpy 𝐽)𝑔) ∣ ∀𝑠 ∈ (0[,]1)((0ℎ𝑠) = (𝑓‘0) ∧ (1ℎ𝑠) = (𝑓‘1))} = {ℎ ∈ (𝐹(II Htpy 𝐽)𝐺) ∣ ∀𝑠 ∈ (0[,]1)((0ℎ𝑠) = (𝐹‘0) ∧ (1ℎ𝑠) = (𝐹‘1))}) |
24 | | isphtpy.3 |
. . . 4
⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽)) |
25 | | ovex 6678 |
. . . . . 6
⊢ (𝐹(II Htpy 𝐽)𝐺) ∈ V |
26 | 25 | rabex 4813 |
. . . . 5
⊢ {ℎ ∈ (𝐹(II Htpy 𝐽)𝐺) ∣ ∀𝑠 ∈ (0[,]1)((0ℎ𝑠) = (𝐹‘0) ∧ (1ℎ𝑠) = (𝐹‘1))} ∈ V |
27 | 26 | a1i 11 |
. . . 4
⊢ (𝜑 → {ℎ ∈ (𝐹(II Htpy 𝐽)𝐺) ∣ ∀𝑠 ∈ (0[,]1)((0ℎ𝑠) = (𝐹‘0) ∧ (1ℎ𝑠) = (𝐹‘1))} ∈ V) |
28 | 13, 23, 1, 24, 27 | ovmpt2d 6788 |
. . 3
⊢ (𝜑 → (𝐹(PHtpy‘𝐽)𝐺) = {ℎ ∈ (𝐹(II Htpy 𝐽)𝐺) ∣ ∀𝑠 ∈ (0[,]1)((0ℎ𝑠) = (𝐹‘0) ∧ (1ℎ𝑠) = (𝐹‘1))}) |
29 | 28 | eleq2d 2687 |
. 2
⊢ (𝜑 → (𝐻 ∈ (𝐹(PHtpy‘𝐽)𝐺) ↔ 𝐻 ∈ {ℎ ∈ (𝐹(II Htpy 𝐽)𝐺) ∣ ∀𝑠 ∈ (0[,]1)((0ℎ𝑠) = (𝐹‘0) ∧ (1ℎ𝑠) = (𝐹‘1))})) |
30 | | oveq 6656 |
. . . . . 6
⊢ (ℎ = 𝐻 → (0ℎ𝑠) = (0𝐻𝑠)) |
31 | 30 | eqeq1d 2624 |
. . . . 5
⊢ (ℎ = 𝐻 → ((0ℎ𝑠) = (𝐹‘0) ↔ (0𝐻𝑠) = (𝐹‘0))) |
32 | | oveq 6656 |
. . . . . 6
⊢ (ℎ = 𝐻 → (1ℎ𝑠) = (1𝐻𝑠)) |
33 | 32 | eqeq1d 2624 |
. . . . 5
⊢ (ℎ = 𝐻 → ((1ℎ𝑠) = (𝐹‘1) ↔ (1𝐻𝑠) = (𝐹‘1))) |
34 | 31, 33 | anbi12d 747 |
. . . 4
⊢ (ℎ = 𝐻 → (((0ℎ𝑠) = (𝐹‘0) ∧ (1ℎ𝑠) = (𝐹‘1)) ↔ ((0𝐻𝑠) = (𝐹‘0) ∧ (1𝐻𝑠) = (𝐹‘1)))) |
35 | 34 | ralbidv 2986 |
. . 3
⊢ (ℎ = 𝐻 → (∀𝑠 ∈ (0[,]1)((0ℎ𝑠) = (𝐹‘0) ∧ (1ℎ𝑠) = (𝐹‘1)) ↔ ∀𝑠 ∈ (0[,]1)((0𝐻𝑠) = (𝐹‘0) ∧ (1𝐻𝑠) = (𝐹‘1)))) |
36 | 35 | elrab 3363 |
. 2
⊢ (𝐻 ∈ {ℎ ∈ (𝐹(II Htpy 𝐽)𝐺) ∣ ∀𝑠 ∈ (0[,]1)((0ℎ𝑠) = (𝐹‘0) ∧ (1ℎ𝑠) = (𝐹‘1))} ↔ (𝐻 ∈ (𝐹(II Htpy 𝐽)𝐺) ∧ ∀𝑠 ∈ (0[,]1)((0𝐻𝑠) = (𝐹‘0) ∧ (1𝐻𝑠) = (𝐹‘1)))) |
37 | 29, 36 | syl6bb 276 |
1
⊢ (𝜑 → (𝐻 ∈ (𝐹(PHtpy‘𝐽)𝐺) ↔ (𝐻 ∈ (𝐹(II Htpy 𝐽)𝐺) ∧ ∀𝑠 ∈ (0[,]1)((0𝐻𝑠) = (𝐹‘0) ∧ (1𝐻𝑠) = (𝐹‘1))))) |