Step | Hyp | Ref
| Expression |
1 | | simp-6l 786 |
. . . . . . 7
β’
(((((((π β§ π β (π» β π΄)) β§ π§ β π΄) β§ (π»βπ§) = π) β§ π₯ β π½) β§ π¦ β πΎ) β§ (π§ β (π₯ Γ π¦) β§ (π₯ Γ π¦) β π΄)) β π) |
2 | | simpllr 775 |
. . . . . . 7
β’
(((((((π β§ π β (π» β π΄)) β§ π§ β π΄) β§ (π»βπ§) = π) β§ π₯ β π½) β§ π¦ β πΎ) β§ (π§ β (π₯ Γ π¦) β§ (π₯ Γ π¦) β π΄)) β π₯ β π½) |
3 | | txomap.1 |
. . . . . . 7
β’ ((π β§ π₯ β π½) β (πΉ β π₯) β πΏ) |
4 | 1, 2, 3 | syl2anc 585 |
. . . . . 6
β’
(((((((π β§ π β (π» β π΄)) β§ π§ β π΄) β§ (π»βπ§) = π) β§ π₯ β π½) β§ π¦ β πΎ) β§ (π§ β (π₯ Γ π¦) β§ (π₯ Γ π¦) β π΄)) β (πΉ β π₯) β πΏ) |
5 | | simplr 768 |
. . . . . . 7
β’
(((((((π β§ π β (π» β π΄)) β§ π§ β π΄) β§ (π»βπ§) = π) β§ π₯ β π½) β§ π¦ β πΎ) β§ (π§ β (π₯ Γ π¦) β§ (π₯ Γ π¦) β π΄)) β π¦ β πΎ) |
6 | | txomap.2 |
. . . . . . 7
β’ ((π β§ π¦ β πΎ) β (πΊ β π¦) β π) |
7 | 1, 5, 6 | syl2anc 585 |
. . . . . 6
β’
(((((((π β§ π β (π» β π΄)) β§ π§ β π΄) β§ (π»βπ§) = π) β§ π₯ β π½) β§ π¦ β πΎ) β§ (π§ β (π₯ Γ π¦) β§ (π₯ Γ π¦) β π΄)) β (πΊ β π¦) β π) |
8 | | txomap.h |
. . . . . . . . 9
β’ π» = (π₯ β π, π¦ β π β¦ β¨(πΉβπ₯), (πΊβπ¦)β©) |
9 | | opex 5426 |
. . . . . . . . 9
β’
β¨(πΉβπ₯), (πΊβπ¦)β© β V |
10 | 8, 9 | fnmpoi 8007 |
. . . . . . . 8
β’ π» Fn (π Γ π) |
11 | | txomap.j |
. . . . . . . . . . 11
β’ (π β π½ β (TopOnβπ)) |
12 | 11 | ad6antr 735 |
. . . . . . . . . 10
β’
(((((((π β§ π β (π» β π΄)) β§ π§ β π΄) β§ (π»βπ§) = π) β§ π₯ β π½) β§ π¦ β πΎ) β§ (π§ β (π₯ Γ π¦) β§ (π₯ Γ π¦) β π΄)) β π½ β (TopOnβπ)) |
13 | | toponss 22292 |
. . . . . . . . . 10
β’ ((π½ β (TopOnβπ) β§ π₯ β π½) β π₯ β π) |
14 | 12, 2, 13 | syl2anc 585 |
. . . . . . . . 9
β’
(((((((π β§ π β (π» β π΄)) β§ π§ β π΄) β§ (π»βπ§) = π) β§ π₯ β π½) β§ π¦ β πΎ) β§ (π§ β (π₯ Γ π¦) β§ (π₯ Γ π¦) β π΄)) β π₯ β π) |
15 | | txomap.k |
. . . . . . . . . . 11
β’ (π β πΎ β (TopOnβπ)) |
16 | 15 | ad6antr 735 |
. . . . . . . . . 10
β’
(((((((π β§ π β (π» β π΄)) β§ π§ β π΄) β§ (π»βπ§) = π) β§ π₯ β π½) β§ π¦ β πΎ) β§ (π§ β (π₯ Γ π¦) β§ (π₯ Γ π¦) β π΄)) β πΎ β (TopOnβπ)) |
17 | | toponss 22292 |
. . . . . . . . . 10
β’ ((πΎ β (TopOnβπ) β§ π¦ β πΎ) β π¦ β π) |
18 | 16, 5, 17 | syl2anc 585 |
. . . . . . . . 9
β’
(((((((π β§ π β (π» β π΄)) β§ π§ β π΄) β§ (π»βπ§) = π) β§ π₯ β π½) β§ π¦ β πΎ) β§ (π§ β (π₯ Γ π¦) β§ (π₯ Γ π¦) β π΄)) β π¦ β π) |
19 | | xpss12 5653 |
. . . . . . . . 9
β’ ((π₯ β π β§ π¦ β π) β (π₯ Γ π¦) β (π Γ π)) |
20 | 14, 18, 19 | syl2anc 585 |
. . . . . . . 8
β’
(((((((π β§ π β (π» β π΄)) β§ π§ β π΄) β§ (π»βπ§) = π) β§ π₯ β π½) β§ π¦ β πΎ) β§ (π§ β (π₯ Γ π¦) β§ (π₯ Γ π¦) β π΄)) β (π₯ Γ π¦) β (π Γ π)) |
21 | | simprl 770 |
. . . . . . . 8
β’
(((((((π β§ π β (π» β π΄)) β§ π§ β π΄) β§ (π»βπ§) = π) β§ π₯ β π½) β§ π¦ β πΎ) β§ (π§ β (π₯ Γ π¦) β§ (π₯ Γ π¦) β π΄)) β π§ β (π₯ Γ π¦)) |
22 | | fnfvima 7188 |
. . . . . . . 8
β’ ((π» Fn (π Γ π) β§ (π₯ Γ π¦) β (π Γ π) β§ π§ β (π₯ Γ π¦)) β (π»βπ§) β (π» β (π₯ Γ π¦))) |
23 | 10, 20, 21, 22 | mp3an2i 1467 |
. . . . . . 7
β’
(((((((π β§ π β (π» β π΄)) β§ π§ β π΄) β§ (π»βπ§) = π) β§ π₯ β π½) β§ π¦ β πΎ) β§ (π§ β (π₯ Γ π¦) β§ (π₯ Γ π¦) β π΄)) β (π»βπ§) β (π» β (π₯ Γ π¦))) |
24 | | simp-4r 783 |
. . . . . . 7
β’
(((((((π β§ π β (π» β π΄)) β§ π§ β π΄) β§ (π»βπ§) = π) β§ π₯ β π½) β§ π¦ β πΎ) β§ (π§ β (π₯ Γ π¦) β§ (π₯ Γ π¦) β π΄)) β (π»βπ§) = π) |
25 | | txomap.f |
. . . . . . . . 9
β’ (π β πΉ:πβΆπ) |
26 | | ffn 6673 |
. . . . . . . . 9
β’ (πΉ:πβΆπ β πΉ Fn π) |
27 | 1, 25, 26 | 3syl 18 |
. . . . . . . 8
β’
(((((((π β§ π β (π» β π΄)) β§ π§ β π΄) β§ (π»βπ§) = π) β§ π₯ β π½) β§ π¦ β πΎ) β§ (π§ β (π₯ Γ π¦) β§ (π₯ Γ π¦) β π΄)) β πΉ Fn π) |
28 | | txomap.g |
. . . . . . . . 9
β’ (π β πΊ:πβΆπ) |
29 | | ffn 6673 |
. . . . . . . . 9
β’ (πΊ:πβΆπ β πΊ Fn π) |
30 | 1, 28, 29 | 3syl 18 |
. . . . . . . 8
β’
(((((((π β§ π β (π» β π΄)) β§ π§ β π΄) β§ (π»βπ§) = π) β§ π₯ β π½) β§ π¦ β πΎ) β§ (π§ β (π₯ Γ π¦) β§ (π₯ Γ π¦) β π΄)) β πΊ Fn π) |
31 | 8, 27, 30, 14, 18 | fimaproj 8072 |
. . . . . . 7
β’
(((((((π β§ π β (π» β π΄)) β§ π§ β π΄) β§ (π»βπ§) = π) β§ π₯ β π½) β§ π¦ β πΎ) β§ (π§ β (π₯ Γ π¦) β§ (π₯ Γ π¦) β π΄)) β (π» β (π₯ Γ π¦)) = ((πΉ β π₯) Γ (πΊ β π¦))) |
32 | 23, 24, 31 | 3eltr3d 2852 |
. . . . . 6
β’
(((((((π β§ π β (π» β π΄)) β§ π§ β π΄) β§ (π»βπ§) = π) β§ π₯ β π½) β§ π¦ β πΎ) β§ (π§ β (π₯ Γ π¦) β§ (π₯ Γ π¦) β π΄)) β π β ((πΉ β π₯) Γ (πΊ β π¦))) |
33 | | imass2 6059 |
. . . . . . . 8
β’ ((π₯ Γ π¦) β π΄ β (π» β (π₯ Γ π¦)) β (π» β π΄)) |
34 | 33 | ad2antll 728 |
. . . . . . 7
β’
(((((((π β§ π β (π» β π΄)) β§ π§ β π΄) β§ (π»βπ§) = π) β§ π₯ β π½) β§ π¦ β πΎ) β§ (π§ β (π₯ Γ π¦) β§ (π₯ Γ π¦) β π΄)) β (π» β (π₯ Γ π¦)) β (π» β π΄)) |
35 | 31, 34 | eqsstrrd 3988 |
. . . . . 6
β’
(((((((π β§ π β (π» β π΄)) β§ π§ β π΄) β§ (π»βπ§) = π) β§ π₯ β π½) β§ π¦ β πΎ) β§ (π§ β (π₯ Γ π¦) β§ (π₯ Γ π¦) β π΄)) β ((πΉ β π₯) Γ (πΊ β π¦)) β (π» β π΄)) |
36 | | xpeq1 5652 |
. . . . . . . . 9
β’ (π = (πΉ β π₯) β (π Γ π) = ((πΉ β π₯) Γ π)) |
37 | 36 | eleq2d 2824 |
. . . . . . . 8
β’ (π = (πΉ β π₯) β (π β (π Γ π) β π β ((πΉ β π₯) Γ π))) |
38 | 36 | sseq1d 3980 |
. . . . . . . 8
β’ (π = (πΉ β π₯) β ((π Γ π) β (π» β π΄) β ((πΉ β π₯) Γ π) β (π» β π΄))) |
39 | 37, 38 | anbi12d 632 |
. . . . . . 7
β’ (π = (πΉ β π₯) β ((π β (π Γ π) β§ (π Γ π) β (π» β π΄)) β (π β ((πΉ β π₯) Γ π) β§ ((πΉ β π₯) Γ π) β (π» β π΄)))) |
40 | | xpeq2 5659 |
. . . . . . . . 9
β’ (π = (πΊ β π¦) β ((πΉ β π₯) Γ π) = ((πΉ β π₯) Γ (πΊ β π¦))) |
41 | 40 | eleq2d 2824 |
. . . . . . . 8
β’ (π = (πΊ β π¦) β (π β ((πΉ β π₯) Γ π) β π β ((πΉ β π₯) Γ (πΊ β π¦)))) |
42 | 40 | sseq1d 3980 |
. . . . . . . 8
β’ (π = (πΊ β π¦) β (((πΉ β π₯) Γ π) β (π» β π΄) β ((πΉ β π₯) Γ (πΊ β π¦)) β (π» β π΄))) |
43 | 41, 42 | anbi12d 632 |
. . . . . . 7
β’ (π = (πΊ β π¦) β ((π β ((πΉ β π₯) Γ π) β§ ((πΉ β π₯) Γ π) β (π» β π΄)) β (π β ((πΉ β π₯) Γ (πΊ β π¦)) β§ ((πΉ β π₯) Γ (πΊ β π¦)) β (π» β π΄)))) |
44 | 39, 43 | rspc2ev 3595 |
. . . . . 6
β’ (((πΉ β π₯) β πΏ β§ (πΊ β π¦) β π β§ (π β ((πΉ β π₯) Γ (πΊ β π¦)) β§ ((πΉ β π₯) Γ (πΊ β π¦)) β (π» β π΄))) β βπ β πΏ βπ β π (π β (π Γ π) β§ (π Γ π) β (π» β π΄))) |
45 | 4, 7, 32, 35, 44 | syl112anc 1375 |
. . . . 5
β’
(((((((π β§ π β (π» β π΄)) β§ π§ β π΄) β§ (π»βπ§) = π) β§ π₯ β π½) β§ π¦ β πΎ) β§ (π§ β (π₯ Γ π¦) β§ (π₯ Γ π¦) β π΄)) β βπ β πΏ βπ β π (π β (π Γ π) β§ (π Γ π) β (π» β π΄))) |
46 | | txomap.a |
. . . . . . . 8
β’ (π β π΄ β (π½ Γt πΎ)) |
47 | | eltx 22935 |
. . . . . . . . 9
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β (π΄ β (π½ Γt πΎ) β βπ§ β π΄ βπ₯ β π½ βπ¦ β πΎ (π§ β (π₯ Γ π¦) β§ (π₯ Γ π¦) β π΄))) |
48 | 11, 15, 47 | syl2anc 585 |
. . . . . . . 8
β’ (π β (π΄ β (π½ Γt πΎ) β βπ§ β π΄ βπ₯ β π½ βπ¦ β πΎ (π§ β (π₯ Γ π¦) β§ (π₯ Γ π¦) β π΄))) |
49 | 46, 48 | mpbid 231 |
. . . . . . 7
β’ (π β βπ§ β π΄ βπ₯ β π½ βπ¦ β πΎ (π§ β (π₯ Γ π¦) β§ (π₯ Γ π¦) β π΄)) |
50 | 49 | r19.21bi 3237 |
. . . . . 6
β’ ((π β§ π§ β π΄) β βπ₯ β π½ βπ¦ β πΎ (π§ β (π₯ Γ π¦) β§ (π₯ Γ π¦) β π΄)) |
51 | 50 | ad4ant13 750 |
. . . . 5
β’ ((((π β§ π β (π» β π΄)) β§ π§ β π΄) β§ (π»βπ§) = π) β βπ₯ β π½ βπ¦ β πΎ (π§ β (π₯ Γ π¦) β§ (π₯ Γ π¦) β π΄)) |
52 | 45, 51 | r19.29vva 3208 |
. . . 4
β’ ((((π β§ π β (π» β π΄)) β§ π§ β π΄) β§ (π»βπ§) = π) β βπ β πΏ βπ β π (π β (π Γ π) β§ (π Γ π) β (π» β π΄))) |
53 | 8 | mpofun 7485 |
. . . . . 6
β’ Fun π» |
54 | | fvelima 6913 |
. . . . . 6
β’ ((Fun
π» β§ π β (π» β π΄)) β βπ§ β π΄ (π»βπ§) = π) |
55 | 53, 54 | mpan 689 |
. . . . 5
β’ (π β (π» β π΄) β βπ§ β π΄ (π»βπ§) = π) |
56 | 55 | adantl 483 |
. . . 4
β’ ((π β§ π β (π» β π΄)) β βπ§ β π΄ (π»βπ§) = π) |
57 | 52, 56 | r19.29a 3160 |
. . 3
β’ ((π β§ π β (π» β π΄)) β βπ β πΏ βπ β π (π β (π Γ π) β§ (π Γ π) β (π» β π΄))) |
58 | 57 | ralrimiva 3144 |
. 2
β’ (π β βπ β (π» β π΄)βπ β πΏ βπ β π (π β (π Γ π) β§ (π Γ π) β (π» β π΄))) |
59 | | txomap.l |
. . 3
β’ (π β πΏ β (TopOnβπ)) |
60 | | txomap.m |
. . 3
β’ (π β π β (TopOnβπ)) |
61 | | eltx 22935 |
. . 3
β’ ((πΏ β (TopOnβπ) β§ π β (TopOnβπ)) β ((π» β π΄) β (πΏ Γt π) β βπ β (π» β π΄)βπ β πΏ βπ β π (π β (π Γ π) β§ (π Γ π) β (π» β π΄)))) |
62 | 59, 60, 61 | syl2anc 585 |
. 2
β’ (π β ((π» β π΄) β (πΏ Γt π) β βπ β (π» β π΄)βπ β πΏ βπ β π (π β (π Γ π) β§ (π Γ π) β (π» β π΄)))) |
63 | 58, 62 | mpbird 257 |
1
β’ (π β (π» β π΄) β (πΏ Γt π)) |