Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . . . 6
β’
(TopOpenββfld) =
(TopOpenββfld) |
2 | 1 | addcn 24373 |
. . . . 5
β’ + β
(((TopOpenββfld) Γt
(TopOpenββfld)) Cn
(TopOpenββfld)) |
3 | | ax-resscn 11164 |
. . . . . 6
β’ β
β β |
4 | | xpss12 5691 |
. . . . . 6
β’ ((β
β β β§ β β β) β (β Γ β)
β (β Γ β)) |
5 | 3, 3, 4 | mp2an 691 |
. . . . 5
β’ (β
Γ β) β (β Γ β) |
6 | 1 | cnfldtop 24292 |
. . . . . . 7
β’
(TopOpenββfld) β Top |
7 | 1 | cnfldtopon 24291 |
. . . . . . . 8
β’
(TopOpenββfld) β
(TopOnββ) |
8 | 7 | toponunii 22410 |
. . . . . . 7
β’ β =
βͺ
(TopOpenββfld) |
9 | 6, 6, 8, 8 | txunii 23089 |
. . . . . 6
β’ (β
Γ β) = βͺ
((TopOpenββfld) Γt
(TopOpenββfld)) |
10 | 9 | cnrest 22781 |
. . . . 5
β’ (( +
β (((TopOpenββfld) Γt
(TopOpenββfld)) Cn
(TopOpenββfld)) β§ (β Γ β) β
(β Γ β)) β ( + βΎ (β Γ β)) β
((((TopOpenββfld) Γt
(TopOpenββfld)) βΎt (β Γ
β)) Cn (TopOpenββfld))) |
11 | 2, 5, 10 | mp2an 691 |
. . . 4
β’ ( +
βΎ (β Γ β)) β
((((TopOpenββfld) Γt
(TopOpenββfld)) βΎt (β Γ
β)) Cn (TopOpenββfld)) |
12 | | reex 11198 |
. . . . . . 7
β’ β
β V |
13 | | txrest 23127 |
. . . . . . 7
β’
((((TopOpenββfld) β Top β§
(TopOpenββfld) β Top) β§ (β β V β§
β β V)) β (((TopOpenββfld)
Γt (TopOpenββfld)) βΎt
(β Γ β)) = (((TopOpenββfld)
βΎt β) Γt
((TopOpenββfld) βΎt
β))) |
14 | 6, 6, 12, 12, 13 | mp4an 692 |
. . . . . 6
β’
(((TopOpenββfld) Γt
(TopOpenββfld)) βΎt (β Γ
β)) = (((TopOpenββfld) βΎt
β) Γt ((TopOpenββfld)
βΎt β)) |
15 | | raddcn.1 |
. . . . . . . 8
β’ π½ = (topGenβran
(,)) |
16 | 1 | tgioo2 24311 |
. . . . . . . 8
β’
(topGenβran (,)) = ((TopOpenββfld)
βΎt β) |
17 | 15, 16 | eqtr2i 2762 |
. . . . . . 7
β’
((TopOpenββfld) βΎt β) =
π½ |
18 | 17, 17 | oveq12i 7418 |
. . . . . 6
β’
(((TopOpenββfld) βΎt β)
Γt ((TopOpenββfld) βΎt
β)) = (π½
Γt π½) |
19 | 14, 18 | eqtri 2761 |
. . . . 5
β’
(((TopOpenββfld) Γt
(TopOpenββfld)) βΎt (β Γ
β)) = (π½
Γt π½) |
20 | 19 | oveq1i 7416 |
. . . 4
β’
((((TopOpenββfld) Γt
(TopOpenββfld)) βΎt (β Γ
β)) Cn (TopOpenββfld)) = ((π½ Γt π½) Cn
(TopOpenββfld)) |
21 | 11, 20 | eleqtri 2832 |
. . 3
β’ ( +
βΎ (β Γ β)) β ((π½ Γt π½) Cn
(TopOpenββfld)) |
22 | | ax-addf 11186 |
. . . . . . . . . 10
β’ +
:(β Γ β)βΆβ |
23 | | ffn 6715 |
. . . . . . . . . 10
β’ ( +
:(β Γ β)βΆβ β + Fn (β Γ
β)) |
24 | 22, 23 | ax-mp 5 |
. . . . . . . . 9
β’ + Fn
(β Γ β) |
25 | | fnssres 6671 |
. . . . . . . . 9
β’ (( + Fn
(β Γ β) β§ (β Γ β) β (β
Γ β)) β ( + βΎ (β Γ β)) Fn (β
Γ β)) |
26 | 24, 5, 25 | mp2an 691 |
. . . . . . . 8
β’ ( +
βΎ (β Γ β)) Fn (β Γ
β) |
27 | | fnov 7537 |
. . . . . . . 8
β’ (( +
βΎ (β Γ β)) Fn (β Γ β) β ( +
βΎ (β Γ β)) = (π₯ β β, π¦ β β β¦ (π₯( + βΎ (β Γ β))π¦))) |
28 | 26, 27 | mpbi 229 |
. . . . . . 7
β’ ( +
βΎ (β Γ β)) = (π₯ β β, π¦ β β β¦ (π₯( + βΎ (β Γ β))π¦)) |
29 | | ovres 7570 |
. . . . . . . 8
β’ ((π₯ β β β§ π¦ β β) β (π₯( + βΎ (β Γ
β))π¦) = (π₯ + π¦)) |
30 | 29 | mpoeq3ia 7484 |
. . . . . . 7
β’ (π₯ β β, π¦ β β β¦ (π₯( + βΎ (β Γ
β))π¦)) = (π₯ β β, π¦ β β β¦ (π₯ + π¦)) |
31 | 28, 30 | eqtri 2761 |
. . . . . 6
β’ ( +
βΎ (β Γ β)) = (π₯ β β, π¦ β β β¦ (π₯ + π¦)) |
32 | 31 | rneqi 5935 |
. . . . 5
β’ ran ( +
βΎ (β Γ β)) = ran (π₯ β β, π¦ β β β¦ (π₯ + π¦)) |
33 | | readdcl 11190 |
. . . . . . 7
β’ ((π₯ β β β§ π¦ β β) β (π₯ + π¦) β β) |
34 | 33 | rgen2 3198 |
. . . . . 6
β’
βπ₯ β
β βπ¦ β
β (π₯ + π¦) β
β |
35 | | eqid 2733 |
. . . . . . 7
β’ (π₯ β β, π¦ β β β¦ (π₯ + π¦)) = (π₯ β β, π¦ β β β¦ (π₯ + π¦)) |
36 | 35 | rnmposs 31887 |
. . . . . 6
β’
(βπ₯ β
β βπ¦ β
β (π₯ + π¦) β β β ran
(π₯ β β, π¦ β β β¦ (π₯ + π¦)) β β) |
37 | 34, 36 | ax-mp 5 |
. . . . 5
β’ ran
(π₯ β β, π¦ β β β¦ (π₯ + π¦)) β β |
38 | 32, 37 | eqsstri 4016 |
. . . 4
β’ ran ( +
βΎ (β Γ β)) β β |
39 | | cnrest2 22782 |
. . . 4
β’
(((TopOpenββfld) β (TopOnββ)
β§ ran ( + βΎ (β Γ β)) β β β§ β
β β) β (( + βΎ (β Γ β)) β ((π½ Γt π½) Cn
(TopOpenββfld)) β ( + βΎ (β Γ
β)) β ((π½
Γt π½) Cn
((TopOpenββfld) βΎt
β)))) |
40 | 7, 38, 3, 39 | mp3an 1462 |
. . 3
β’ (( +
βΎ (β Γ β)) β ((π½ Γt π½) Cn (TopOpenββfld))
β ( + βΎ (β Γ β)) β ((π½ Γt π½) Cn ((TopOpenββfld)
βΎt β))) |
41 | 21, 40 | mpbi 229 |
. 2
β’ ( +
βΎ (β Γ β)) β ((π½ Γt π½) Cn ((TopOpenββfld)
βΎt β)) |
42 | 17 | oveq2i 7417 |
. 2
β’ ((π½ Γt π½) Cn
((TopOpenββfld) βΎt β)) = ((π½ Γt π½) Cn π½) |
43 | 41, 31, 42 | 3eltr3i 2846 |
1
β’ (π₯ β β, π¦ β β β¦ (π₯ + π¦)) β ((π½ Γt π½) Cn π½) |