Step | Hyp | Ref
| Expression |
1 | | tmdcn2.2 |
. . . . 5
β’ π½ = (TopOpenβπΊ) |
2 | | tmdcn2.1 |
. . . . 5
β’ π΅ = (BaseβπΊ) |
3 | 1, 2 | tmdtopon 23384 |
. . . 4
β’ (πΊ β TopMnd β π½ β (TopOnβπ΅)) |
4 | 3 | ad2antrr 724 |
. . 3
β’ (((πΊ β TopMnd β§ π β π½) β§ (π β π΅ β§ π β π΅ β§ (π + π) β π)) β π½ β (TopOnβπ΅)) |
5 | | eqid 2737 |
. . . . . 6
β’
(+πβπΊ) = (+πβπΊ) |
6 | 1, 5 | tmdcn 23386 |
. . . . 5
β’ (πΊ β TopMnd β
(+πβπΊ) β ((π½ Γt π½) Cn π½)) |
7 | 6 | ad2antrr 724 |
. . . 4
β’ (((πΊ β TopMnd β§ π β π½) β§ (π β π΅ β§ π β π΅ β§ (π + π) β π)) β (+πβπΊ) β ((π½ Γt π½) Cn π½)) |
8 | | simpr1 1194 |
. . . . . 6
β’ (((πΊ β TopMnd β§ π β π½) β§ (π β π΅ β§ π β π΅ β§ (π + π) β π)) β π β π΅) |
9 | | simpr2 1195 |
. . . . . 6
β’ (((πΊ β TopMnd β§ π β π½) β§ (π β π΅ β§ π β π΅ β§ (π + π) β π)) β π β π΅) |
10 | 8, 9 | opelxpd 5669 |
. . . . 5
β’ (((πΊ β TopMnd β§ π β π½) β§ (π β π΅ β§ π β π΅ β§ (π + π) β π)) β β¨π, πβ© β (π΅ Γ π΅)) |
11 | | txtopon 22894 |
. . . . . . 7
β’ ((π½ β (TopOnβπ΅) β§ π½ β (TopOnβπ΅)) β (π½ Γt π½) β (TopOnβ(π΅ Γ π΅))) |
12 | 4, 4, 11 | syl2anc 584 |
. . . . . 6
β’ (((πΊ β TopMnd β§ π β π½) β§ (π β π΅ β§ π β π΅ β§ (π + π) β π)) β (π½ Γt π½) β (TopOnβ(π΅ Γ π΅))) |
13 | | toponuni 22215 |
. . . . . 6
β’ ((π½ Γt π½) β (TopOnβ(π΅ Γ π΅)) β (π΅ Γ π΅) = βͺ (π½ Γt π½)) |
14 | 12, 13 | syl 17 |
. . . . 5
β’ (((πΊ β TopMnd β§ π β π½) β§ (π β π΅ β§ π β π΅ β§ (π + π) β π)) β (π΅ Γ π΅) = βͺ (π½ Γt π½)) |
15 | 10, 14 | eleqtrd 2840 |
. . . 4
β’ (((πΊ β TopMnd β§ π β π½) β§ (π β π΅ β§ π β π΅ β§ (π + π) β π)) β β¨π, πβ© β βͺ
(π½ Γt
π½)) |
16 | | eqid 2737 |
. . . . 5
β’ βͺ (π½
Γt π½) =
βͺ (π½ Γt π½) |
17 | 16 | cncnpi 22581 |
. . . 4
β’
(((+πβπΊ) β ((π½ Γt π½) Cn π½) β§ β¨π, πβ© β βͺ
(π½ Γt
π½)) β
(+πβπΊ) β (((π½ Γt π½) CnP π½)ββ¨π, πβ©)) |
18 | 7, 15, 17 | syl2anc 584 |
. . 3
β’ (((πΊ β TopMnd β§ π β π½) β§ (π β π΅ β§ π β π΅ β§ (π + π) β π)) β (+πβπΊ) β (((π½ Γt π½) CnP π½)ββ¨π, πβ©)) |
19 | | simplr 767 |
. . 3
β’ (((πΊ β TopMnd β§ π β π½) β§ (π β π΅ β§ π β π΅ β§ (π + π) β π)) β π β π½) |
20 | | tmdcn2.3 |
. . . . . 6
β’ + =
(+gβπΊ) |
21 | 2, 20, 5 | plusfval 18464 |
. . . . 5
β’ ((π β π΅ β§ π β π΅) β (π(+πβπΊ)π) = (π + π)) |
22 | 8, 9, 21 | syl2anc 584 |
. . . 4
β’ (((πΊ β TopMnd β§ π β π½) β§ (π β π΅ β§ π β π΅ β§ (π + π) β π)) β (π(+πβπΊ)π) = (π + π)) |
23 | | simpr3 1196 |
. . . 4
β’ (((πΊ β TopMnd β§ π β π½) β§ (π β π΅ β§ π β π΅ β§ (π + π) β π)) β (π + π) β π) |
24 | 22, 23 | eqeltrd 2838 |
. . 3
β’ (((πΊ β TopMnd β§ π β π½) β§ (π β π΅ β§ π β π΅ β§ (π + π) β π)) β (π(+πβπΊ)π) β π) |
25 | 4, 4, 18, 19, 8, 9, 24 | txcnpi 22911 |
. 2
β’ (((πΊ β TopMnd β§ π β π½) β§ (π β π΅ β§ π β π΅ β§ (π + π) β π)) β βπ’ β π½ βπ£ β π½ (π β π’ β§ π β π£ β§ (π’ Γ π£) β (β‘(+πβπΊ) β π))) |
26 | | dfss3 3930 |
. . . . . . 7
β’ ((π’ Γ π£) β (β‘(+πβπΊ) β π) β βπ§ β (π’ Γ π£)π§ β (β‘(+πβπΊ) β π)) |
27 | | eleq1 2825 |
. . . . . . . . 9
β’ (π§ = β¨π₯, π¦β© β (π§ β (β‘(+πβπΊ) β π) β β¨π₯, π¦β© β (β‘(+πβπΊ) β π))) |
28 | 2, 5 | plusffn 18466 |
. . . . . . . . . 10
β’
(+πβπΊ) Fn (π΅ Γ π΅) |
29 | | elpreima 7005 |
. . . . . . . . . 10
β’
((+πβπΊ) Fn (π΅ Γ π΅) β (β¨π₯, π¦β© β (β‘(+πβπΊ) β π) β (β¨π₯, π¦β© β (π΅ Γ π΅) β§ ((+πβπΊ)ββ¨π₯, π¦β©) β π))) |
30 | 28, 29 | ax-mp 5 |
. . . . . . . . 9
β’
(β¨π₯, π¦β© β (β‘(+πβπΊ) β π) β (β¨π₯, π¦β© β (π΅ Γ π΅) β§ ((+πβπΊ)ββ¨π₯, π¦β©) β π)) |
31 | 27, 30 | bitrdi 286 |
. . . . . . . 8
β’ (π§ = β¨π₯, π¦β© β (π§ β (β‘(+πβπΊ) β π) β (β¨π₯, π¦β© β (π΅ Γ π΅) β§ ((+πβπΊ)ββ¨π₯, π¦β©) β π))) |
32 | 31 | ralxp 5795 |
. . . . . . 7
β’
(βπ§ β
(π’ Γ π£)π§ β (β‘(+πβπΊ) β π) β βπ₯ β π’ βπ¦ β π£ (β¨π₯, π¦β© β (π΅ Γ π΅) β§ ((+πβπΊ)ββ¨π₯, π¦β©) β π)) |
33 | 26, 32 | bitri 274 |
. . . . . 6
β’ ((π’ Γ π£) β (β‘(+πβπΊ) β π) β βπ₯ β π’ βπ¦ β π£ (β¨π₯, π¦β© β (π΅ Γ π΅) β§ ((+πβπΊ)ββ¨π₯, π¦β©) β π)) |
34 | | opelxp 5667 |
. . . . . . . . . 10
β’
(β¨π₯, π¦β© β (π΅ Γ π΅) β (π₯ β π΅ β§ π¦ β π΅)) |
35 | | df-ov 7354 |
. . . . . . . . . . 11
β’ (π₯(+πβπΊ)π¦) = ((+πβπΊ)ββ¨π₯, π¦β©) |
36 | 2, 20, 5 | plusfval 18464 |
. . . . . . . . . . 11
β’ ((π₯ β π΅ β§ π¦ β π΅) β (π₯(+πβπΊ)π¦) = (π₯ + π¦)) |
37 | 35, 36 | eqtr3id 2791 |
. . . . . . . . . 10
β’ ((π₯ β π΅ β§ π¦ β π΅) β ((+πβπΊ)ββ¨π₯, π¦β©) = (π₯ + π¦)) |
38 | 34, 37 | sylbi 216 |
. . . . . . . . 9
β’
(β¨π₯, π¦β© β (π΅ Γ π΅) β ((+πβπΊ)ββ¨π₯, π¦β©) = (π₯ + π¦)) |
39 | 38 | eleq1d 2822 |
. . . . . . . 8
β’
(β¨π₯, π¦β© β (π΅ Γ π΅) β
(((+πβπΊ)ββ¨π₯, π¦β©) β π β (π₯ + π¦) β π)) |
40 | 39 | biimpa 477 |
. . . . . . 7
β’
((β¨π₯, π¦β© β (π΅ Γ π΅) β§ ((+πβπΊ)ββ¨π₯, π¦β©) β π) β (π₯ + π¦) β π) |
41 | 40 | 2ralimi 3124 |
. . . . . 6
β’
(βπ₯ β
π’ βπ¦ β π£ (β¨π₯, π¦β© β (π΅ Γ π΅) β§ ((+πβπΊ)ββ¨π₯, π¦β©) β π) β βπ₯ β π’ βπ¦ β π£ (π₯ + π¦) β π) |
42 | 33, 41 | sylbi 216 |
. . . . 5
β’ ((π’ Γ π£) β (β‘(+πβπΊ) β π) β βπ₯ β π’ βπ¦ β π£ (π₯ + π¦) β π) |
43 | 42 | 3anim3i 1154 |
. . . 4
β’ ((π β π’ β§ π β π£ β§ (π’ Γ π£) β (β‘(+πβπΊ) β π)) β (π β π’ β§ π β π£ β§ βπ₯ β π’ βπ¦ β π£ (π₯ + π¦) β π)) |
44 | 43 | reximi 3085 |
. . 3
β’
(βπ£ β
π½ (π β π’ β§ π β π£ β§ (π’ Γ π£) β (β‘(+πβπΊ) β π)) β βπ£ β π½ (π β π’ β§ π β π£ β§ βπ₯ β π’ βπ¦ β π£ (π₯ + π¦) β π)) |
45 | 44 | reximi 3085 |
. 2
β’
(βπ’ β
π½ βπ£ β π½ (π β π’ β§ π β π£ β§ (π’ Γ π£) β (β‘(+πβπΊ) β π)) β βπ’ β π½ βπ£ β π½ (π β π’ β§ π β π£ β§ βπ₯ β π’ βπ¦ β π£ (π₯ + π¦) β π)) |
46 | 25, 45 | syl 17 |
1
β’ (((πΊ β TopMnd β§ π β π½) β§ (π β π΅ β§ π β π΅ β§ (π + π) β π)) β βπ’ β π½ βπ£ β π½ (π β π’ β§ π β π£ β§ βπ₯ β π’ βπ¦ β π£ (π₯ + π¦) β π)) |