Step | Hyp | Ref
| Expression |
1 | | df-htpy 24143 |
. . . . . 6
⊢ Htpy =
(𝑗 ∈ Top, 𝑘 ∈ Top ↦ (𝑓 ∈ (𝑗 Cn 𝑘), 𝑔 ∈ (𝑗 Cn 𝑘) ↦ {ℎ ∈ ((𝑗 ×t II) Cn 𝑘) ∣ ∀𝑠 ∈ ∪ 𝑗((𝑠ℎ0) = (𝑓‘𝑠) ∧ (𝑠ℎ1) = (𝑔‘𝑠))})) |
2 | 1 | a1i 11 |
. . . . 5
⊢ (𝜑 → Htpy = (𝑗 ∈ Top, 𝑘 ∈ Top ↦ (𝑓 ∈ (𝑗 Cn 𝑘), 𝑔 ∈ (𝑗 Cn 𝑘) ↦ {ℎ ∈ ((𝑗 ×t II) Cn 𝑘) ∣ ∀𝑠 ∈ ∪ 𝑗((𝑠ℎ0) = (𝑓‘𝑠) ∧ (𝑠ℎ1) = (𝑔‘𝑠))}))) |
3 | | simprl 768 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑗 = 𝐽 ∧ 𝑘 = 𝐾)) → 𝑗 = 𝐽) |
4 | | simprr 770 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑗 = 𝐽 ∧ 𝑘 = 𝐾)) → 𝑘 = 𝐾) |
5 | 3, 4 | oveq12d 7285 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑗 = 𝐽 ∧ 𝑘 = 𝐾)) → (𝑗 Cn 𝑘) = (𝐽 Cn 𝐾)) |
6 | 3 | oveq1d 7282 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑗 = 𝐽 ∧ 𝑘 = 𝐾)) → (𝑗 ×t II) = (𝐽 ×t II)) |
7 | 6, 4 | oveq12d 7285 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑗 = 𝐽 ∧ 𝑘 = 𝐾)) → ((𝑗 ×t II) Cn 𝑘) = ((𝐽 ×t II) Cn 𝐾)) |
8 | 3 | unieqd 4853 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑗 = 𝐽 ∧ 𝑘 = 𝐾)) → ∪ 𝑗 = ∪
𝐽) |
9 | | ishtpy.1 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |
10 | | toponuni 22073 |
. . . . . . . . . . 11
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽) |
11 | 9, 10 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 = ∪ 𝐽) |
12 | 11 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑗 = 𝐽 ∧ 𝑘 = 𝐾)) → 𝑋 = ∪ 𝐽) |
13 | 8, 12 | eqtr4d 2781 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑗 = 𝐽 ∧ 𝑘 = 𝐾)) → ∪ 𝑗 = 𝑋) |
14 | 13 | raleqdv 3346 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑗 = 𝐽 ∧ 𝑘 = 𝐾)) → (∀𝑠 ∈ ∪ 𝑗((𝑠ℎ0) = (𝑓‘𝑠) ∧ (𝑠ℎ1) = (𝑔‘𝑠)) ↔ ∀𝑠 ∈ 𝑋 ((𝑠ℎ0) = (𝑓‘𝑠) ∧ (𝑠ℎ1) = (𝑔‘𝑠)))) |
15 | 7, 14 | rabeqbidv 3417 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑗 = 𝐽 ∧ 𝑘 = 𝐾)) → {ℎ ∈ ((𝑗 ×t II) Cn 𝑘) ∣ ∀𝑠 ∈ ∪ 𝑗((𝑠ℎ0) = (𝑓‘𝑠) ∧ (𝑠ℎ1) = (𝑔‘𝑠))} = {ℎ ∈ ((𝐽 ×t II) Cn 𝐾) ∣ ∀𝑠 ∈ 𝑋 ((𝑠ℎ0) = (𝑓‘𝑠) ∧ (𝑠ℎ1) = (𝑔‘𝑠))}) |
16 | 5, 5, 15 | mpoeq123dv 7340 |
. . . . 5
⊢ ((𝜑 ∧ (𝑗 = 𝐽 ∧ 𝑘 = 𝐾)) → (𝑓 ∈ (𝑗 Cn 𝑘), 𝑔 ∈ (𝑗 Cn 𝑘) ↦ {ℎ ∈ ((𝑗 ×t II) Cn 𝑘) ∣ ∀𝑠 ∈ ∪ 𝑗((𝑠ℎ0) = (𝑓‘𝑠) ∧ (𝑠ℎ1) = (𝑔‘𝑠))}) = (𝑓 ∈ (𝐽 Cn 𝐾), 𝑔 ∈ (𝐽 Cn 𝐾) ↦ {ℎ ∈ ((𝐽 ×t II) Cn 𝐾) ∣ ∀𝑠 ∈ 𝑋 ((𝑠ℎ0) = (𝑓‘𝑠) ∧ (𝑠ℎ1) = (𝑔‘𝑠))})) |
17 | | topontop 22072 |
. . . . . 6
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top) |
18 | 9, 17 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐽 ∈ Top) |
19 | | ishtpy.3 |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) |
20 | | cntop2 22402 |
. . . . . 6
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐾 ∈ Top) |
21 | 19, 20 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐾 ∈ Top) |
22 | | ovex 7300 |
. . . . . . . . . 10
⊢ ((𝐽 ×t II) Cn
𝐾) ∈
V |
23 | | ssrab2 4012 |
. . . . . . . . . 10
⊢ {ℎ ∈ ((𝐽 ×t II) Cn 𝐾) ∣ ∀𝑠 ∈ 𝑋 ((𝑠ℎ0) = (𝑓‘𝑠) ∧ (𝑠ℎ1) = (𝑔‘𝑠))} ⊆ ((𝐽 ×t II) Cn 𝐾) |
24 | 22, 23 | elpwi2 5268 |
. . . . . . . . 9
⊢ {ℎ ∈ ((𝐽 ×t II) Cn 𝐾) ∣ ∀𝑠 ∈ 𝑋 ((𝑠ℎ0) = (𝑓‘𝑠) ∧ (𝑠ℎ1) = (𝑔‘𝑠))} ∈ 𝒫 ((𝐽 ×t II) Cn 𝐾) |
25 | 24 | rgen2w 3077 |
. . . . . . . 8
⊢
∀𝑓 ∈
(𝐽 Cn 𝐾)∀𝑔 ∈ (𝐽 Cn 𝐾){ℎ ∈ ((𝐽 ×t II) Cn 𝐾) ∣ ∀𝑠 ∈ 𝑋 ((𝑠ℎ0) = (𝑓‘𝑠) ∧ (𝑠ℎ1) = (𝑔‘𝑠))} ∈ 𝒫 ((𝐽 ×t II) Cn 𝐾) |
26 | | eqid 2738 |
. . . . . . . . 9
⊢ (𝑓 ∈ (𝐽 Cn 𝐾), 𝑔 ∈ (𝐽 Cn 𝐾) ↦ {ℎ ∈ ((𝐽 ×t II) Cn 𝐾) ∣ ∀𝑠 ∈ 𝑋 ((𝑠ℎ0) = (𝑓‘𝑠) ∧ (𝑠ℎ1) = (𝑔‘𝑠))}) = (𝑓 ∈ (𝐽 Cn 𝐾), 𝑔 ∈ (𝐽 Cn 𝐾) ↦ {ℎ ∈ ((𝐽 ×t II) Cn 𝐾) ∣ ∀𝑠 ∈ 𝑋 ((𝑠ℎ0) = (𝑓‘𝑠) ∧ (𝑠ℎ1) = (𝑔‘𝑠))}) |
27 | 26 | fmpo 7897 |
. . . . . . . 8
⊢
(∀𝑓 ∈
(𝐽 Cn 𝐾)∀𝑔 ∈ (𝐽 Cn 𝐾){ℎ ∈ ((𝐽 ×t II) Cn 𝐾) ∣ ∀𝑠 ∈ 𝑋 ((𝑠ℎ0) = (𝑓‘𝑠) ∧ (𝑠ℎ1) = (𝑔‘𝑠))} ∈ 𝒫 ((𝐽 ×t II) Cn 𝐾) ↔ (𝑓 ∈ (𝐽 Cn 𝐾), 𝑔 ∈ (𝐽 Cn 𝐾) ↦ {ℎ ∈ ((𝐽 ×t II) Cn 𝐾) ∣ ∀𝑠 ∈ 𝑋 ((𝑠ℎ0) = (𝑓‘𝑠) ∧ (𝑠ℎ1) = (𝑔‘𝑠))}):((𝐽 Cn 𝐾) × (𝐽 Cn 𝐾))⟶𝒫 ((𝐽 ×t II) Cn 𝐾)) |
28 | 25, 27 | mpbi 229 |
. . . . . . 7
⊢ (𝑓 ∈ (𝐽 Cn 𝐾), 𝑔 ∈ (𝐽 Cn 𝐾) ↦ {ℎ ∈ ((𝐽 ×t II) Cn 𝐾) ∣ ∀𝑠 ∈ 𝑋 ((𝑠ℎ0) = (𝑓‘𝑠) ∧ (𝑠ℎ1) = (𝑔‘𝑠))}):((𝐽 Cn 𝐾) × (𝐽 Cn 𝐾))⟶𝒫 ((𝐽 ×t II) Cn 𝐾) |
29 | | ovex 7300 |
. . . . . . . 8
⊢ (𝐽 Cn 𝐾) ∈ V |
30 | 29, 29 | xpex 7593 |
. . . . . . 7
⊢ ((𝐽 Cn 𝐾) × (𝐽 Cn 𝐾)) ∈ V |
31 | 22 | pwex 5301 |
. . . . . . 7
⊢ 𝒫
((𝐽 ×t II)
Cn 𝐾) ∈
V |
32 | | fex2 7770 |
. . . . . . 7
⊢ (((𝑓 ∈ (𝐽 Cn 𝐾), 𝑔 ∈ (𝐽 Cn 𝐾) ↦ {ℎ ∈ ((𝐽 ×t II) Cn 𝐾) ∣ ∀𝑠 ∈ 𝑋 ((𝑠ℎ0) = (𝑓‘𝑠) ∧ (𝑠ℎ1) = (𝑔‘𝑠))}):((𝐽 Cn 𝐾) × (𝐽 Cn 𝐾))⟶𝒫 ((𝐽 ×t II) Cn 𝐾) ∧ ((𝐽 Cn 𝐾) × (𝐽 Cn 𝐾)) ∈ V ∧ 𝒫 ((𝐽 ×t II) Cn
𝐾) ∈ V) → (𝑓 ∈ (𝐽 Cn 𝐾), 𝑔 ∈ (𝐽 Cn 𝐾) ↦ {ℎ ∈ ((𝐽 ×t II) Cn 𝐾) ∣ ∀𝑠 ∈ 𝑋 ((𝑠ℎ0) = (𝑓‘𝑠) ∧ (𝑠ℎ1) = (𝑔‘𝑠))}) ∈ V) |
33 | 28, 30, 31, 32 | mp3an 1460 |
. . . . . 6
⊢ (𝑓 ∈ (𝐽 Cn 𝐾), 𝑔 ∈ (𝐽 Cn 𝐾) ↦ {ℎ ∈ ((𝐽 ×t II) Cn 𝐾) ∣ ∀𝑠 ∈ 𝑋 ((𝑠ℎ0) = (𝑓‘𝑠) ∧ (𝑠ℎ1) = (𝑔‘𝑠))}) ∈ V |
34 | 33 | a1i 11 |
. . . . 5
⊢ (𝜑 → (𝑓 ∈ (𝐽 Cn 𝐾), 𝑔 ∈ (𝐽 Cn 𝐾) ↦ {ℎ ∈ ((𝐽 ×t II) Cn 𝐾) ∣ ∀𝑠 ∈ 𝑋 ((𝑠ℎ0) = (𝑓‘𝑠) ∧ (𝑠ℎ1) = (𝑔‘𝑠))}) ∈ V) |
35 | 2, 16, 18, 21, 34 | ovmpod 7415 |
. . . 4
⊢ (𝜑 → (𝐽 Htpy 𝐾) = (𝑓 ∈ (𝐽 Cn 𝐾), 𝑔 ∈ (𝐽 Cn 𝐾) ↦ {ℎ ∈ ((𝐽 ×t II) Cn 𝐾) ∣ ∀𝑠 ∈ 𝑋 ((𝑠ℎ0) = (𝑓‘𝑠) ∧ (𝑠ℎ1) = (𝑔‘𝑠))})) |
36 | | fveq1 6765 |
. . . . . . . . 9
⊢ (𝑓 = 𝐹 → (𝑓‘𝑠) = (𝐹‘𝑠)) |
37 | 36 | eqeq2d 2749 |
. . . . . . . 8
⊢ (𝑓 = 𝐹 → ((𝑠ℎ0) = (𝑓‘𝑠) ↔ (𝑠ℎ0) = (𝐹‘𝑠))) |
38 | | fveq1 6765 |
. . . . . . . . 9
⊢ (𝑔 = 𝐺 → (𝑔‘𝑠) = (𝐺‘𝑠)) |
39 | 38 | eqeq2d 2749 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → ((𝑠ℎ1) = (𝑔‘𝑠) ↔ (𝑠ℎ1) = (𝐺‘𝑠))) |
40 | 37, 39 | bi2anan9 636 |
. . . . . . 7
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (((𝑠ℎ0) = (𝑓‘𝑠) ∧ (𝑠ℎ1) = (𝑔‘𝑠)) ↔ ((𝑠ℎ0) = (𝐹‘𝑠) ∧ (𝑠ℎ1) = (𝐺‘𝑠)))) |
41 | 40 | adantl 482 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑔 = 𝐺)) → (((𝑠ℎ0) = (𝑓‘𝑠) ∧ (𝑠ℎ1) = (𝑔‘𝑠)) ↔ ((𝑠ℎ0) = (𝐹‘𝑠) ∧ (𝑠ℎ1) = (𝐺‘𝑠)))) |
42 | 41 | ralbidv 3121 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑔 = 𝐺)) → (∀𝑠 ∈ 𝑋 ((𝑠ℎ0) = (𝑓‘𝑠) ∧ (𝑠ℎ1) = (𝑔‘𝑠)) ↔ ∀𝑠 ∈ 𝑋 ((𝑠ℎ0) = (𝐹‘𝑠) ∧ (𝑠ℎ1) = (𝐺‘𝑠)))) |
43 | 42 | rabbidv 3411 |
. . . 4
⊢ ((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑔 = 𝐺)) → {ℎ ∈ ((𝐽 ×t II) Cn 𝐾) ∣ ∀𝑠 ∈ 𝑋 ((𝑠ℎ0) = (𝑓‘𝑠) ∧ (𝑠ℎ1) = (𝑔‘𝑠))} = {ℎ ∈ ((𝐽 ×t II) Cn 𝐾) ∣ ∀𝑠 ∈ 𝑋 ((𝑠ℎ0) = (𝐹‘𝑠) ∧ (𝑠ℎ1) = (𝐺‘𝑠))}) |
44 | | ishtpy.4 |
. . . 4
⊢ (𝜑 → 𝐺 ∈ (𝐽 Cn 𝐾)) |
45 | 22 | rabex 5254 |
. . . . 5
⊢ {ℎ ∈ ((𝐽 ×t II) Cn 𝐾) ∣ ∀𝑠 ∈ 𝑋 ((𝑠ℎ0) = (𝐹‘𝑠) ∧ (𝑠ℎ1) = (𝐺‘𝑠))} ∈ V |
46 | 45 | a1i 11 |
. . . 4
⊢ (𝜑 → {ℎ ∈ ((𝐽 ×t II) Cn 𝐾) ∣ ∀𝑠 ∈ 𝑋 ((𝑠ℎ0) = (𝐹‘𝑠) ∧ (𝑠ℎ1) = (𝐺‘𝑠))} ∈ V) |
47 | 35, 43, 19, 44, 46 | ovmpod 7415 |
. . 3
⊢ (𝜑 → (𝐹(𝐽 Htpy 𝐾)𝐺) = {ℎ ∈ ((𝐽 ×t II) Cn 𝐾) ∣ ∀𝑠 ∈ 𝑋 ((𝑠ℎ0) = (𝐹‘𝑠) ∧ (𝑠ℎ1) = (𝐺‘𝑠))}) |
48 | 47 | eleq2d 2824 |
. 2
⊢ (𝜑 → (𝐻 ∈ (𝐹(𝐽 Htpy 𝐾)𝐺) ↔ 𝐻 ∈ {ℎ ∈ ((𝐽 ×t II) Cn 𝐾) ∣ ∀𝑠 ∈ 𝑋 ((𝑠ℎ0) = (𝐹‘𝑠) ∧ (𝑠ℎ1) = (𝐺‘𝑠))})) |
49 | | oveq 7273 |
. . . . . 6
⊢ (ℎ = 𝐻 → (𝑠ℎ0) = (𝑠𝐻0)) |
50 | 49 | eqeq1d 2740 |
. . . . 5
⊢ (ℎ = 𝐻 → ((𝑠ℎ0) = (𝐹‘𝑠) ↔ (𝑠𝐻0) = (𝐹‘𝑠))) |
51 | | oveq 7273 |
. . . . . 6
⊢ (ℎ = 𝐻 → (𝑠ℎ1) = (𝑠𝐻1)) |
52 | 51 | eqeq1d 2740 |
. . . . 5
⊢ (ℎ = 𝐻 → ((𝑠ℎ1) = (𝐺‘𝑠) ↔ (𝑠𝐻1) = (𝐺‘𝑠))) |
53 | 50, 52 | anbi12d 631 |
. . . 4
⊢ (ℎ = 𝐻 → (((𝑠ℎ0) = (𝐹‘𝑠) ∧ (𝑠ℎ1) = (𝐺‘𝑠)) ↔ ((𝑠𝐻0) = (𝐹‘𝑠) ∧ (𝑠𝐻1) = (𝐺‘𝑠)))) |
54 | 53 | ralbidv 3121 |
. . 3
⊢ (ℎ = 𝐻 → (∀𝑠 ∈ 𝑋 ((𝑠ℎ0) = (𝐹‘𝑠) ∧ (𝑠ℎ1) = (𝐺‘𝑠)) ↔ ∀𝑠 ∈ 𝑋 ((𝑠𝐻0) = (𝐹‘𝑠) ∧ (𝑠𝐻1) = (𝐺‘𝑠)))) |
55 | 54 | elrab 3623 |
. 2
⊢ (𝐻 ∈ {ℎ ∈ ((𝐽 ×t II) Cn 𝐾) ∣ ∀𝑠 ∈ 𝑋 ((𝑠ℎ0) = (𝐹‘𝑠) ∧ (𝑠ℎ1) = (𝐺‘𝑠))} ↔ (𝐻 ∈ ((𝐽 ×t II) Cn 𝐾) ∧ ∀𝑠 ∈ 𝑋 ((𝑠𝐻0) = (𝐹‘𝑠) ∧ (𝑠𝐻1) = (𝐺‘𝑠)))) |
56 | 48, 55 | bitrdi 287 |
1
⊢ (𝜑 → (𝐻 ∈ (𝐹(𝐽 Htpy 𝐾)𝐺) ↔ (𝐻 ∈ ((𝐽 ×t II) Cn 𝐾) ∧ ∀𝑠 ∈ 𝑋 ((𝑠𝐻0) = (𝐹‘𝑠) ∧ (𝑠𝐻1) = (𝐺‘𝑠))))) |