Step | Hyp | Ref
| Expression |
1 | | r19.27v 3181 |
. . . . . . . 8
β’
((βπ’ β
π½ (π
β π’ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’) β§ βπ£ β πΎ (π β π£ β βπ β π βπ β (β€β₯βπ)(πΊβπ) β π£)) β βπ’ β π½ ((π
β π’ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’) β§ βπ£ β πΎ (π β π£ β βπ β π βπ β (β€β₯βπ)(πΊβπ) β π£))) |
2 | | r19.28v 3183 |
. . . . . . . . 9
β’ (((π
β π’ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’) β§ βπ£ β πΎ (π β π£ β βπ β π βπ β (β€β₯βπ)(πΊβπ) β π£)) β βπ£ β πΎ ((π
β π’ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’) β§ (π β π£ β βπ β π βπ β (β€β₯βπ)(πΊβπ) β π£))) |
3 | 2 | ralimi 3083 |
. . . . . . . 8
β’
(βπ’ β
π½ ((π
β π’ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’) β§ βπ£ β πΎ (π β π£ β βπ β π βπ β (β€β₯βπ)(πΊβπ) β π£)) β βπ’ β π½ βπ£ β πΎ ((π
β π’ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’) β§ (π β π£ β βπ β π βπ β (β€β₯βπ)(πΊβπ) β π£))) |
4 | 1, 3 | syl 17 |
. . . . . . 7
β’
((βπ’ β
π½ (π
β π’ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’) β§ βπ£ β πΎ (π β π£ β βπ β π βπ β (β€β₯βπ)(πΊβπ) β π£)) β βπ’ β π½ βπ£ β πΎ ((π
β π’ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’) β§ (π β π£ β βπ β π βπ β (β€β₯βπ)(πΊβπ) β π£))) |
5 | | simprl 770 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π€ β (π½ Γt πΎ) β§ β¨π
, πβ© β π€)) β π€ β (π½ Γt πΎ)) |
6 | | txlm.j |
. . . . . . . . . . . . . . . . . 18
β’ (π β π½ β (TopOnβπ)) |
7 | | topontop 22285 |
. . . . . . . . . . . . . . . . . 18
β’ (π½ β (TopOnβπ) β π½ β Top) |
8 | 6, 7 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π β π½ β Top) |
9 | | txlm.k |
. . . . . . . . . . . . . . . . . 18
β’ (π β πΎ β (TopOnβπ)) |
10 | | topontop 22285 |
. . . . . . . . . . . . . . . . . 18
β’ (πΎ β (TopOnβπ) β πΎ β Top) |
11 | 9, 10 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π β πΎ β Top) |
12 | | eqid 2733 |
. . . . . . . . . . . . . . . . . 18
β’ ran
(π’ β π½, π£ β πΎ β¦ (π’ Γ π£)) = ran (π’ β π½, π£ β πΎ β¦ (π’ Γ π£)) |
13 | 12 | txval 22938 |
. . . . . . . . . . . . . . . . 17
β’ ((π½ β Top β§ πΎ β Top) β (π½ Γt πΎ) = (topGenβran (π’ β π½, π£ β πΎ β¦ (π’ Γ π£)))) |
14 | 8, 11, 13 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ (π β (π½ Γt πΎ) = (topGenβran (π’ β π½, π£ β πΎ β¦ (π’ Γ π£)))) |
15 | 14 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π€ β (π½ Γt πΎ) β§ β¨π
, πβ© β π€)) β (π½ Γt πΎ) = (topGenβran (π’ β π½, π£ β πΎ β¦ (π’ Γ π£)))) |
16 | 5, 15 | eleqtrd 2836 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π€ β (π½ Γt πΎ) β§ β¨π
, πβ© β π€)) β π€ β (topGenβran (π’ β π½, π£ β πΎ β¦ (π’ Γ π£)))) |
17 | | simprr 772 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π€ β (π½ Γt πΎ) β§ β¨π
, πβ© β π€)) β β¨π
, πβ© β π€) |
18 | | tg2 22338 |
. . . . . . . . . . . . . 14
β’ ((π€ β (topGenβran (π’ β π½, π£ β πΎ β¦ (π’ Γ π£))) β§ β¨π
, πβ© β π€) β βπ‘ β ran (π’ β π½, π£ β πΎ β¦ (π’ Γ π£))(β¨π
, πβ© β π‘ β§ π‘ β π€)) |
19 | 16, 17, 18 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((π β§ (π€ β (π½ Γt πΎ) β§ β¨π
, πβ© β π€)) β βπ‘ β ran (π’ β π½, π£ β πΎ β¦ (π’ Γ π£))(β¨π
, πβ© β π‘ β§ π‘ β π€)) |
20 | | vex 3451 |
. . . . . . . . . . . . . . . 16
β’ π’ β V |
21 | | vex 3451 |
. . . . . . . . . . . . . . . 16
β’ π£ β V |
22 | 20, 21 | xpex 7691 |
. . . . . . . . . . . . . . 15
β’ (π’ Γ π£) β V |
23 | 22 | rgen2w 3066 |
. . . . . . . . . . . . . 14
β’
βπ’ β
π½ βπ£ β πΎ (π’ Γ π£) β V |
24 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’ (π’ β π½, π£ β πΎ β¦ (π’ Γ π£)) = (π’ β π½, π£ β πΎ β¦ (π’ Γ π£)) |
25 | | eleq2 2823 |
. . . . . . . . . . . . . . . 16
β’ (π‘ = (π’ Γ π£) β (β¨π
, πβ© β π‘ β β¨π
, πβ© β (π’ Γ π£))) |
26 | | sseq1 3973 |
. . . . . . . . . . . . . . . 16
β’ (π‘ = (π’ Γ π£) β (π‘ β π€ β (π’ Γ π£) β π€)) |
27 | 25, 26 | anbi12d 632 |
. . . . . . . . . . . . . . 15
β’ (π‘ = (π’ Γ π£) β ((β¨π
, πβ© β π‘ β§ π‘ β π€) β (β¨π
, πβ© β (π’ Γ π£) β§ (π’ Γ π£) β π€))) |
28 | 24, 27 | rexrnmpo 7499 |
. . . . . . . . . . . . . 14
β’
(βπ’ β
π½ βπ£ β πΎ (π’ Γ π£) β V β (βπ‘ β ran (π’ β π½, π£ β πΎ β¦ (π’ Γ π£))(β¨π
, πβ© β π‘ β§ π‘ β π€) β βπ’ β π½ βπ£ β πΎ (β¨π
, πβ© β (π’ Γ π£) β§ (π’ Γ π£) β π€))) |
29 | 23, 28 | ax-mp 5 |
. . . . . . . . . . . . 13
β’
(βπ‘ β ran
(π’ β π½, π£ β πΎ β¦ (π’ Γ π£))(β¨π
, πβ© β π‘ β§ π‘ β π€) β βπ’ β π½ βπ£ β πΎ (β¨π
, πβ© β (π’ Γ π£) β§ (π’ Γ π£) β π€)) |
30 | 19, 29 | sylib 217 |
. . . . . . . . . . . 12
β’ ((π β§ (π€ β (π½ Γt πΎ) β§ β¨π
, πβ© β π€)) β βπ’ β π½ βπ£ β πΎ (β¨π
, πβ© β (π’ Γ π£) β§ (π’ Γ π£) β π€)) |
31 | 30 | ex 414 |
. . . . . . . . . . 11
β’ (π β ((π€ β (π½ Γt πΎ) β§ β¨π
, πβ© β π€) β βπ’ β π½ βπ£ β πΎ (β¨π
, πβ© β (π’ Γ π£) β§ (π’ Γ π£) β π€))) |
32 | | r19.29 3114 |
. . . . . . . . . . . . 13
β’
((βπ’ β
π½ βπ£ β πΎ ((π
β π’ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’) β§ (π β π£ β βπ β π βπ β (β€β₯βπ)(πΊβπ) β π£)) β§ βπ’ β π½ βπ£ β πΎ (β¨π
, πβ© β (π’ Γ π£) β§ (π’ Γ π£) β π€)) β βπ’ β π½ (βπ£ β πΎ ((π
β π’ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’) β§ (π β π£ β βπ β π βπ β (β€β₯βπ)(πΊβπ) β π£)) β§ βπ£ β πΎ (β¨π
, πβ© β (π’ Γ π£) β§ (π’ Γ π£) β π€))) |
33 | | r19.29 3114 |
. . . . . . . . . . . . . . 15
β’
((βπ£ β
πΎ ((π
β π’ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’) β§ (π β π£ β βπ β π βπ β (β€β₯βπ)(πΊβπ) β π£)) β§ βπ£ β πΎ (β¨π
, πβ© β (π’ Γ π£) β§ (π’ Γ π£) β π€)) β βπ£ β πΎ (((π
β π’ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’) β§ (π β π£ β βπ β π βπ β (β€β₯βπ)(πΊβπ) β π£)) β§ (β¨π
, πβ© β (π’ Γ π£) β§ (π’ Γ π£) β π€))) |
34 | | simprl 770 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π’ β π½) β§ π£ β πΎ) β§ (β¨π
, πβ© β (π’ Γ π£) β§ (π’ Γ π£) β π€)) β β¨π
, πβ© β (π’ Γ π£)) |
35 | | opelxp 5673 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(β¨π
, πβ© β (π’ Γ π£) β (π
β π’ β§ π β π£)) |
36 | 34, 35 | sylib 217 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π’ β π½) β§ π£ β πΎ) β§ (β¨π
, πβ© β (π’ Γ π£) β§ (π’ Γ π£) β π€)) β (π
β π’ β§ π β π£)) |
37 | | pm2.27 42 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π
β π’ β ((π
β π’ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’) β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’)) |
38 | | pm2.27 42 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β π£ β ((π β π£ β βπ β π βπ β (β€β₯βπ)(πΊβπ) β π£) β βπ β π βπ β (β€β₯βπ)(πΊβπ) β π£)) |
39 | 37, 38 | im2anan9 621 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π
β π’ β§ π β π£) β (((π
β π’ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’) β§ (π β π£ β βπ β π βπ β (β€β₯βπ)(πΊβπ) β π£)) β (βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’ β§ βπ β π βπ β (β€β₯βπ)(πΊβπ) β π£))) |
40 | 36, 39 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π’ β π½) β§ π£ β πΎ) β§ (β¨π
, πβ© β (π’ Γ π£) β§ (π’ Γ π£) β π€)) β (((π
β π’ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’) β§ (π β π£ β βπ β π βπ β (β€β₯βπ)(πΊβπ) β π£)) β (βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’ β§ βπ β π βπ β (β€β₯βπ)(πΊβπ) β π£))) |
41 | | txlm.z |
. . . . . . . . . . . . . . . . . . . . 21
β’ π =
(β€β₯βπ) |
42 | 41 | rexanuz2 15243 |
. . . . . . . . . . . . . . . . . . . 20
β’
(βπ β
π βπ β
(β€β₯βπ)((πΉβπ) β π’ β§ (πΊβπ) β π£) β (βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’ β§ βπ β π βπ β (β€β₯βπ)(πΊβπ) β π£)) |
43 | 41 | uztrn2 12790 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β π β§ π β (β€β₯βπ)) β π β π) |
44 | | opelxpi 5674 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((πΉβπ) β π’ β§ (πΊβπ) β π£) β β¨(πΉβπ), (πΊβπ)β© β (π’ Γ π£)) |
45 | | fveq2 6846 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π = π β (πΉβπ) = (πΉβπ)) |
46 | | fveq2 6846 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π = π β (πΊβπ) = (πΊβπ)) |
47 | 45, 46 | opeq12d 4842 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π = π β β¨(πΉβπ), (πΊβπ)β© = β¨(πΉβπ), (πΊβπ)β©) |
48 | | txlm.h |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ π» = (π β π β¦ β¨(πΉβπ), (πΊβπ)β©) |
49 | | opex 5425 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
β¨(πΉβπ), (πΊβπ)β© β V |
50 | 47, 48, 49 | fvmpt 6952 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β π β (π»βπ) = β¨(πΉβπ), (πΊβπ)β©) |
51 | 50 | eleq1d 2819 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β π β ((π»βπ) β (π’ Γ π£) β β¨(πΉβπ), (πΊβπ)β© β (π’ Γ π£))) |
52 | 44, 51 | syl5ibr 246 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β π β (((πΉβπ) β π’ β§ (πΊβπ) β π£) β (π»βπ) β (π’ Γ π£))) |
53 | 52 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((π β§ π’ β π½) β§ π£ β πΎ) β§ (β¨π
, πβ© β (π’ Γ π£) β§ (π’ Γ π£) β π€)) β§ π β π) β (((πΉβπ) β π’ β§ (πΊβπ) β π£) β (π»βπ) β (π’ Γ π£))) |
54 | | simplrr 777 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((((π β§ π’ β π½) β§ π£ β πΎ) β§ (β¨π
, πβ© β (π’ Γ π£) β§ (π’ Γ π£) β π€)) β§ π β π) β (π’ Γ π£) β π€) |
55 | 54 | sseld 3947 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((π β§ π’ β π½) β§ π£ β πΎ) β§ (β¨π
, πβ© β (π’ Γ π£) β§ (π’ Γ π£) β π€)) β§ π β π) β ((π»βπ) β (π’ Γ π£) β (π»βπ) β π€)) |
56 | 53, 55 | syld 47 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((π β§ π’ β π½) β§ π£ β πΎ) β§ (β¨π
, πβ© β (π’ Γ π£) β§ (π’ Γ π£) β π€)) β§ π β π) β (((πΉβπ) β π’ β§ (πΊβπ) β π£) β (π»βπ) β π€)) |
57 | 43, 56 | sylan2 594 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((π β§ π’ β π½) β§ π£ β πΎ) β§ (β¨π
, πβ© β (π’ Γ π£) β§ (π’ Γ π£) β π€)) β§ (π β π β§ π β (β€β₯βπ))) β (((πΉβπ) β π’ β§ (πΊβπ) β π£) β (π»βπ) β π€)) |
58 | 57 | anassrs 469 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((((((π β§ π’ β π½) β§ π£ β πΎ) β§ (β¨π
, πβ© β (π’ Γ π£) β§ (π’ Γ π£) β π€)) β§ π β π) β§ π β (β€β₯βπ)) β (((πΉβπ) β π’ β§ (πΊβπ) β π£) β (π»βπ) β π€)) |
59 | 58 | ralimdva 3161 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π β§ π’ β π½) β§ π£ β πΎ) β§ (β¨π
, πβ© β (π’ Γ π£) β§ (π’ Γ π£) β π€)) β§ π β π) β (βπ β (β€β₯βπ)((πΉβπ) β π’ β§ (πΊβπ) β π£) β βπ β (β€β₯βπ)(π»βπ) β π€)) |
60 | 59 | reximdva 3162 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π’ β π½) β§ π£ β πΎ) β§ (β¨π
, πβ© β (π’ Γ π£) β§ (π’ Γ π£) β π€)) β (βπ β π βπ β (β€β₯βπ)((πΉβπ) β π’ β§ (πΊβπ) β π£) β βπ β π βπ β (β€β₯βπ)(π»βπ) β π€)) |
61 | 42, 60 | biimtrrid 242 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π’ β π½) β§ π£ β πΎ) β§ (β¨π
, πβ© β (π’ Γ π£) β§ (π’ Γ π£) β π€)) β ((βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’ β§ βπ β π βπ β (β€β₯βπ)(πΊβπ) β π£) β βπ β π βπ β (β€β₯βπ)(π»βπ) β π€)) |
62 | 40, 61 | syld 47 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π’ β π½) β§ π£ β πΎ) β§ (β¨π
, πβ© β (π’ Γ π£) β§ (π’ Γ π£) β π€)) β (((π
β π’ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’) β§ (π β π£ β βπ β π βπ β (β€β₯βπ)(πΊβπ) β π£)) β βπ β π βπ β (β€β₯βπ)(π»βπ) β π€)) |
63 | 62 | ex 414 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π’ β π½) β§ π£ β πΎ) β ((β¨π
, πβ© β (π’ Γ π£) β§ (π’ Γ π£) β π€) β (((π
β π’ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’) β§ (π β π£ β βπ β π βπ β (β€β₯βπ)(πΊβπ) β π£)) β βπ β π βπ β (β€β₯βπ)(π»βπ) β π€))) |
64 | 63 | impcomd 413 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π’ β π½) β§ π£ β πΎ) β ((((π
β π’ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’) β§ (π β π£ β βπ β π βπ β (β€β₯βπ)(πΊβπ) β π£)) β§ (β¨π
, πβ© β (π’ Γ π£) β§ (π’ Γ π£) β π€)) β βπ β π βπ β (β€β₯βπ)(π»βπ) β π€)) |
65 | 64 | rexlimdva 3149 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π’ β π½) β (βπ£ β πΎ (((π
β π’ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’) β§ (π β π£ β βπ β π βπ β (β€β₯βπ)(πΊβπ) β π£)) β§ (β¨π
, πβ© β (π’ Γ π£) β§ (π’ Γ π£) β π€)) β βπ β π βπ β (β€β₯βπ)(π»βπ) β π€)) |
66 | 33, 65 | syl5 34 |
. . . . . . . . . . . . . 14
β’ ((π β§ π’ β π½) β ((βπ£ β πΎ ((π
β π’ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’) β§ (π β π£ β βπ β π βπ β (β€β₯βπ)(πΊβπ) β π£)) β§ βπ£ β πΎ (β¨π
, πβ© β (π’ Γ π£) β§ (π’ Γ π£) β π€)) β βπ β π βπ β (β€β₯βπ)(π»βπ) β π€)) |
67 | 66 | rexlimdva 3149 |
. . . . . . . . . . . . 13
β’ (π β (βπ’ β π½ (βπ£ β πΎ ((π
β π’ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’) β§ (π β π£ β βπ β π βπ β (β€β₯βπ)(πΊβπ) β π£)) β§ βπ£ β πΎ (β¨π
, πβ© β (π’ Γ π£) β§ (π’ Γ π£) β π€)) β βπ β π βπ β (β€β₯βπ)(π»βπ) β π€)) |
68 | 32, 67 | syl5 34 |
. . . . . . . . . . . 12
β’ (π β ((βπ’ β π½ βπ£ β πΎ ((π
β π’ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’) β§ (π β π£ β βπ β π βπ β (β€β₯βπ)(πΊβπ) β π£)) β§ βπ’ β π½ βπ£ β πΎ (β¨π
, πβ© β (π’ Γ π£) β§ (π’ Γ π£) β π€)) β βπ β π βπ β (β€β₯βπ)(π»βπ) β π€)) |
69 | 68 | expcomd 418 |
. . . . . . . . . . 11
β’ (π β (βπ’ β π½ βπ£ β πΎ (β¨π
, πβ© β (π’ Γ π£) β§ (π’ Γ π£) β π€) β (βπ’ β π½ βπ£ β πΎ ((π
β π’ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’) β§ (π β π£ β βπ β π βπ β (β€β₯βπ)(πΊβπ) β π£)) β βπ β π βπ β (β€β₯βπ)(π»βπ) β π€))) |
70 | 31, 69 | syld 47 |
. . . . . . . . . 10
β’ (π β ((π€ β (π½ Γt πΎ) β§ β¨π
, πβ© β π€) β (βπ’ β π½ βπ£ β πΎ ((π
β π’ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’) β§ (π β π£ β βπ β π βπ β (β€β₯βπ)(πΊβπ) β π£)) β βπ β π βπ β (β€β₯βπ)(π»βπ) β π€))) |
71 | 70 | expdimp 454 |
. . . . . . . . 9
β’ ((π β§ π€ β (π½ Γt πΎ)) β (β¨π
, πβ© β π€ β (βπ’ β π½ βπ£ β πΎ ((π
β π’ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’) β§ (π β π£ β βπ β π βπ β (β€β₯βπ)(πΊβπ) β π£)) β βπ β π βπ β (β€β₯βπ)(π»βπ) β π€))) |
72 | 71 | com23 86 |
. . . . . . . 8
β’ ((π β§ π€ β (π½ Γt πΎ)) β (βπ’ β π½ βπ£ β πΎ ((π
β π’ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’) β§ (π β π£ β βπ β π βπ β (β€β₯βπ)(πΊβπ) β π£)) β (β¨π
, πβ© β π€ β βπ β π βπ β (β€β₯βπ)(π»βπ) β π€))) |
73 | 72 | ralrimdva 3148 |
. . . . . . 7
β’ (π β (βπ’ β π½ βπ£ β πΎ ((π
β π’ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’) β§ (π β π£ β βπ β π βπ β (β€β₯βπ)(πΊβπ) β π£)) β βπ€ β (π½ Γt πΎ)(β¨π
, πβ© β π€ β βπ β π βπ β (β€β₯βπ)(π»βπ) β π€))) |
74 | 4, 73 | syl5 34 |
. . . . . 6
β’ (π β ((βπ’ β π½ (π
β π’ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’) β§ βπ£ β πΎ (π β π£ β βπ β π βπ β (β€β₯βπ)(πΊβπ) β π£)) β βπ€ β (π½ Γt πΎ)(β¨π
, πβ© β π€ β βπ β π βπ β (β€β₯βπ)(π»βπ) β π€))) |
75 | 74 | adantr 482 |
. . . . 5
β’ ((π β§ (π
β π β§ π β π)) β ((βπ’ β π½ (π
β π’ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’) β§ βπ£ β πΎ (π β π£ β βπ β π βπ β (β€β₯βπ)(πΊβπ) β π£)) β βπ€ β (π½ Γt πΎ)(β¨π
, πβ© β π€ β βπ β π βπ β (β€β₯βπ)(π»βπ) β π€))) |
76 | 8 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ (π β π β§ π’ β π½)) β π½ β Top) |
77 | 11 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ (π β π β§ π’ β π½)) β πΎ β Top) |
78 | | simprr 772 |
. . . . . . . . . . . 12
β’ ((π β§ (π β π β§ π’ β π½)) β π’ β π½) |
79 | | toponmax 22298 |
. . . . . . . . . . . . . 14
β’ (πΎ β (TopOnβπ) β π β πΎ) |
80 | 9, 79 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β π β πΎ) |
81 | 80 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ (π β π β§ π’ β π½)) β π β πΎ) |
82 | | txopn 22976 |
. . . . . . . . . . . 12
β’ (((π½ β Top β§ πΎ β Top) β§ (π’ β π½ β§ π β πΎ)) β (π’ Γ π) β (π½ Γt πΎ)) |
83 | 76, 77, 78, 81, 82 | syl22anc 838 |
. . . . . . . . . . 11
β’ ((π β§ (π β π β§ π’ β π½)) β (π’ Γ π) β (π½ Γt πΎ)) |
84 | | eleq2 2823 |
. . . . . . . . . . . . 13
β’ (π€ = (π’ Γ π) β (β¨π
, πβ© β π€ β β¨π
, πβ© β (π’ Γ π))) |
85 | | eleq2 2823 |
. . . . . . . . . . . . . 14
β’ (π€ = (π’ Γ π) β ((π»βπ) β π€ β (π»βπ) β (π’ Γ π))) |
86 | 85 | rexralbidv 3211 |
. . . . . . . . . . . . 13
β’ (π€ = (π’ Γ π) β (βπ β π βπ β (β€β₯βπ)(π»βπ) β π€ β βπ β π βπ β (β€β₯βπ)(π»βπ) β (π’ Γ π))) |
87 | 84, 86 | imbi12d 345 |
. . . . . . . . . . . 12
β’ (π€ = (π’ Γ π) β ((β¨π
, πβ© β π€ β βπ β π βπ β (β€β₯βπ)(π»βπ) β π€) β (β¨π
, πβ© β (π’ Γ π) β βπ β π βπ β (β€β₯βπ)(π»βπ) β (π’ Γ π)))) |
88 | 87 | rspcv 3579 |
. . . . . . . . . . 11
β’ ((π’ Γ π) β (π½ Γt πΎ) β (βπ€ β (π½ Γt πΎ)(β¨π
, πβ© β π€ β βπ β π βπ β (β€β₯βπ)(π»βπ) β π€) β (β¨π
, πβ© β (π’ Γ π) β βπ β π βπ β (β€β₯βπ)(π»βπ) β (π’ Γ π)))) |
89 | 83, 88 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ (π β π β§ π’ β π½)) β (βπ€ β (π½ Γt πΎ)(β¨π
, πβ© β π€ β βπ β π βπ β (β€β₯βπ)(π»βπ) β π€) β (β¨π
, πβ© β (π’ Γ π) β βπ β π βπ β (β€β₯βπ)(π»βπ) β (π’ Γ π)))) |
90 | | simprl 770 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β π β§ π’ β π½)) β π β π) |
91 | | opelxpi 5674 |
. . . . . . . . . . . . 13
β’ ((π
β π’ β§ π β π) β β¨π
, πβ© β (π’ Γ π)) |
92 | 90, 91 | sylan2 594 |
. . . . . . . . . . . 12
β’ ((π
β π’ β§ (π β§ (π β π β§ π’ β π½))) β β¨π
, πβ© β (π’ Γ π)) |
93 | 92 | expcom 415 |
. . . . . . . . . . 11
β’ ((π β§ (π β π β§ π’ β π½)) β (π
β π’ β β¨π
, πβ© β (π’ Γ π))) |
94 | 50 | eleq1d 2819 |
. . . . . . . . . . . . . . . 16
β’ (π β π β ((π»βπ) β (π’ Γ π) β β¨(πΉβπ), (πΊβπ)β© β (π’ Γ π))) |
95 | | opelxp1 5678 |
. . . . . . . . . . . . . . . 16
β’
(β¨(πΉβπ), (πΊβπ)β© β (π’ Γ π) β (πΉβπ) β π’) |
96 | 94, 95 | syl6bi 253 |
. . . . . . . . . . . . . . 15
β’ (π β π β ((π»βπ) β (π’ Γ π) β (πΉβπ) β π’)) |
97 | 43, 96 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β π β§ π β (β€β₯βπ)) β ((π»βπ) β (π’ Γ π) β (πΉβπ) β π’)) |
98 | 97 | ralimdva 3161 |
. . . . . . . . . . . . 13
β’ (π β π β (βπ β (β€β₯βπ)(π»βπ) β (π’ Γ π) β βπ β (β€β₯βπ)(πΉβπ) β π’)) |
99 | 98 | reximia 3081 |
. . . . . . . . . . . 12
β’
(βπ β
π βπ β
(β€β₯βπ)(π»βπ) β (π’ Γ π) β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’) |
100 | 99 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β§ (π β π β§ π’ β π½)) β (βπ β π βπ β (β€β₯βπ)(π»βπ) β (π’ Γ π) β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’)) |
101 | 93, 100 | imim12d 81 |
. . . . . . . . . 10
β’ ((π β§ (π β π β§ π’ β π½)) β ((β¨π
, πβ© β (π’ Γ π) β βπ β π βπ β (β€β₯βπ)(π»βπ) β (π’ Γ π)) β (π
β π’ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’))) |
102 | 89, 101 | syld 47 |
. . . . . . . . 9
β’ ((π β§ (π β π β§ π’ β π½)) β (βπ€ β (π½ Γt πΎ)(β¨π
, πβ© β π€ β βπ β π βπ β (β€β₯βπ)(π»βπ) β π€) β (π
β π’ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’))) |
103 | 102 | anassrs 469 |
. . . . . . . 8
β’ (((π β§ π β π) β§ π’ β π½) β (βπ€ β (π½ Γt πΎ)(β¨π
, πβ© β π€ β βπ β π βπ β (β€β₯βπ)(π»βπ) β π€) β (π
β π’ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’))) |
104 | 103 | ralrimdva 3148 |
. . . . . . 7
β’ ((π β§ π β π) β (βπ€ β (π½ Γt πΎ)(β¨π
, πβ© β π€ β βπ β π βπ β (β€β₯βπ)(π»βπ) β π€) β βπ’ β π½ (π
β π’ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’))) |
105 | 104 | adantrl 715 |
. . . . . 6
β’ ((π β§ (π
β π β§ π β π)) β (βπ€ β (π½ Γt πΎ)(β¨π
, πβ© β π€ β βπ β π βπ β (β€β₯βπ)(π»βπ) β π€) β βπ’ β π½ (π
β π’ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’))) |
106 | 8 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ (π
β π β§ π£ β πΎ)) β π½ β Top) |
107 | 11 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ (π
β π β§ π£ β πΎ)) β πΎ β Top) |
108 | | toponmax 22298 |
. . . . . . . . . . . . . 14
β’ (π½ β (TopOnβπ) β π β π½) |
109 | 6, 108 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β π β π½) |
110 | 109 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ (π
β π β§ π£ β πΎ)) β π β π½) |
111 | | simprr 772 |
. . . . . . . . . . . 12
β’ ((π β§ (π
β π β§ π£ β πΎ)) β π£ β πΎ) |
112 | | txopn 22976 |
. . . . . . . . . . . 12
β’ (((π½ β Top β§ πΎ β Top) β§ (π β π½ β§ π£ β πΎ)) β (π Γ π£) β (π½ Γt πΎ)) |
113 | 106, 107,
110, 111, 112 | syl22anc 838 |
. . . . . . . . . . 11
β’ ((π β§ (π
β π β§ π£ β πΎ)) β (π Γ π£) β (π½ Γt πΎ)) |
114 | | eleq2 2823 |
. . . . . . . . . . . . 13
β’ (π€ = (π Γ π£) β (β¨π
, πβ© β π€ β β¨π
, πβ© β (π Γ π£))) |
115 | | eleq2 2823 |
. . . . . . . . . . . . . 14
β’ (π€ = (π Γ π£) β ((π»βπ) β π€ β (π»βπ) β (π Γ π£))) |
116 | 115 | rexralbidv 3211 |
. . . . . . . . . . . . 13
β’ (π€ = (π Γ π£) β (βπ β π βπ β (β€β₯βπ)(π»βπ) β π€ β βπ β π βπ β (β€β₯βπ)(π»βπ) β (π Γ π£))) |
117 | 114, 116 | imbi12d 345 |
. . . . . . . . . . . 12
β’ (π€ = (π Γ π£) β ((β¨π
, πβ© β π€ β βπ β π βπ β (β€β₯βπ)(π»βπ) β π€) β (β¨π
, πβ© β (π Γ π£) β βπ β π βπ β (β€β₯βπ)(π»βπ) β (π Γ π£)))) |
118 | 117 | rspcv 3579 |
. . . . . . . . . . 11
β’ ((π Γ π£) β (π½ Γt πΎ) β (βπ€ β (π½ Γt πΎ)(β¨π
, πβ© β π€ β βπ β π βπ β (β€β₯βπ)(π»βπ) β π€) β (β¨π
, πβ© β (π Γ π£) β βπ β π βπ β (β€β₯βπ)(π»βπ) β (π Γ π£)))) |
119 | 113, 118 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ (π
β π β§ π£ β πΎ)) β (βπ€ β (π½ Γt πΎ)(β¨π
, πβ© β π€ β βπ β π βπ β (β€β₯βπ)(π»βπ) β π€) β (β¨π
, πβ© β (π Γ π£) β βπ β π βπ β (β€β₯βπ)(π»βπ) β (π Γ π£)))) |
120 | | opelxpi 5674 |
. . . . . . . . . . . . 13
β’ ((π
β π β§ π β π£) β β¨π
, πβ© β (π Γ π£)) |
121 | 120 | ex 414 |
. . . . . . . . . . . 12
β’ (π
β π β (π β π£ β β¨π
, πβ© β (π Γ π£))) |
122 | 121 | ad2antrl 727 |
. . . . . . . . . . 11
β’ ((π β§ (π
β π β§ π£ β πΎ)) β (π β π£ β β¨π
, πβ© β (π Γ π£))) |
123 | 50 | eleq1d 2819 |
. . . . . . . . . . . . . . . 16
β’ (π β π β ((π»βπ) β (π Γ π£) β β¨(πΉβπ), (πΊβπ)β© β (π Γ π£))) |
124 | | opelxp2 5679 |
. . . . . . . . . . . . . . . 16
β’
(β¨(πΉβπ), (πΊβπ)β© β (π Γ π£) β (πΊβπ) β π£) |
125 | 123, 124 | syl6bi 253 |
. . . . . . . . . . . . . . 15
β’ (π β π β ((π»βπ) β (π Γ π£) β (πΊβπ) β π£)) |
126 | 43, 125 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β π β§ π β (β€β₯βπ)) β ((π»βπ) β (π Γ π£) β (πΊβπ) β π£)) |
127 | 126 | ralimdva 3161 |
. . . . . . . . . . . . 13
β’ (π β π β (βπ β (β€β₯βπ)(π»βπ) β (π Γ π£) β βπ β (β€β₯βπ)(πΊβπ) β π£)) |
128 | 127 | reximia 3081 |
. . . . . . . . . . . 12
β’
(βπ β
π βπ β
(β€β₯βπ)(π»βπ) β (π Γ π£) β βπ β π βπ β (β€β₯βπ)(πΊβπ) β π£) |
129 | 128 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β§ (π
β π β§ π£ β πΎ)) β (βπ β π βπ β (β€β₯βπ)(π»βπ) β (π Γ π£) β βπ β π βπ β (β€β₯βπ)(πΊβπ) β π£)) |
130 | 122, 129 | imim12d 81 |
. . . . . . . . . 10
β’ ((π β§ (π
β π β§ π£ β πΎ)) β ((β¨π
, πβ© β (π Γ π£) β βπ β π βπ β (β€β₯βπ)(π»βπ) β (π Γ π£)) β (π β π£ β βπ β π βπ β (β€β₯βπ)(πΊβπ) β π£))) |
131 | 119, 130 | syld 47 |
. . . . . . . . 9
β’ ((π β§ (π
β π β§ π£ β πΎ)) β (βπ€ β (π½ Γt πΎ)(β¨π
, πβ© β π€ β βπ β π βπ β (β€β₯βπ)(π»βπ) β π€) β (π β π£ β βπ β π βπ β (β€β₯βπ)(πΊβπ) β π£))) |
132 | 131 | anassrs 469 |
. . . . . . . 8
β’ (((π β§ π
β π) β§ π£ β πΎ) β (βπ€ β (π½ Γt πΎ)(β¨π
, πβ© β π€ β βπ β π βπ β (β€β₯βπ)(π»βπ) β π€) β (π β π£ β βπ β π βπ β (β€β₯βπ)(πΊβπ) β π£))) |
133 | 132 | ralrimdva 3148 |
. . . . . . 7
β’ ((π β§ π
β π) β (βπ€ β (π½ Γt πΎ)(β¨π
, πβ© β π€ β βπ β π βπ β (β€β₯βπ)(π»βπ) β π€) β βπ£ β πΎ (π β π£ β βπ β π βπ β (β€β₯βπ)(πΊβπ) β π£))) |
134 | 133 | adantrr 716 |
. . . . . 6
β’ ((π β§ (π
β π β§ π β π)) β (βπ€ β (π½ Γt πΎ)(β¨π
, πβ© β π€ β βπ β π βπ β (β€β₯βπ)(π»βπ) β π€) β βπ£ β πΎ (π β π£ β βπ β π βπ β (β€β₯βπ)(πΊβπ) β π£))) |
135 | 105, 134 | jcad 514 |
. . . . 5
β’ ((π β§ (π
β π β§ π β π)) β (βπ€ β (π½ Γt πΎ)(β¨π
, πβ© β π€ β βπ β π βπ β (β€β₯βπ)(π»βπ) β π€) β (βπ’ β π½ (π
β π’ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’) β§ βπ£ β πΎ (π β π£ β βπ β π βπ β (β€β₯βπ)(πΊβπ) β π£)))) |
136 | 75, 135 | impbid 211 |
. . . 4
β’ ((π β§ (π
β π β§ π β π)) β ((βπ’ β π½ (π
β π’ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’) β§ βπ£ β πΎ (π β π£ β βπ β π βπ β (β€β₯βπ)(πΊβπ) β π£)) β βπ€ β (π½ Γt πΎ)(β¨π
, πβ© β π€ β βπ β π βπ β (β€β₯βπ)(π»βπ) β π€))) |
137 | 136 | pm5.32da 580 |
. . 3
β’ (π β (((π
β π β§ π β π) β§ (βπ’ β π½ (π
β π’ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’) β§ βπ£ β πΎ (π β π£ β βπ β π βπ β (β€β₯βπ)(πΊβπ) β π£))) β ((π
β π β§ π β π) β§ βπ€ β (π½ Γt πΎ)(β¨π
, πβ© β π€ β βπ β π βπ β (β€β₯βπ)(π»βπ) β π€)))) |
138 | | opelxp 5673 |
. . . 4
β’
(β¨π
, πβ© β (π Γ π) β (π
β π β§ π β π)) |
139 | 138 | anbi1i 625 |
. . 3
β’
((β¨π
, πβ© β (π Γ π) β§ βπ€ β (π½ Γt πΎ)(β¨π
, πβ© β π€ β βπ β π βπ β (β€β₯βπ)(π»βπ) β π€)) β ((π
β π β§ π β π) β§ βπ€ β (π½ Γt πΎ)(β¨π
, πβ© β π€ β βπ β π βπ β (β€β₯βπ)(π»βπ) β π€))) |
140 | 137, 139 | bitr4di 289 |
. 2
β’ (π β (((π
β π β§ π β π) β§ (βπ’ β π½ (π
β π’ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’) β§ βπ£ β πΎ (π β π£ β βπ β π βπ β (β€β₯βπ)(πΊβπ) β π£))) β (β¨π
, πβ© β (π Γ π) β§ βπ€ β (π½ Γt πΎ)(β¨π
, πβ© β π€ β βπ β π βπ β (β€β₯βπ)(π»βπ) β π€)))) |
141 | | txlm.m |
. . . . 5
β’ (π β π β β€) |
142 | | txlm.f |
. . . . 5
β’ (π β πΉ:πβΆπ) |
143 | | eqidd 2734 |
. . . . 5
β’ ((π β§ π β π) β (πΉβπ) = (πΉβπ)) |
144 | 6, 41, 141, 142, 143 | lmbrf 22634 |
. . . 4
β’ (π β (πΉ(βπ‘βπ½)π
β (π
β π β§ βπ’ β π½ (π
β π’ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’)))) |
145 | | txlm.g |
. . . . 5
β’ (π β πΊ:πβΆπ) |
146 | | eqidd 2734 |
. . . . 5
β’ ((π β§ π β π) β (πΊβπ) = (πΊβπ)) |
147 | 9, 41, 141, 145, 146 | lmbrf 22634 |
. . . 4
β’ (π β (πΊ(βπ‘βπΎ)π β (π β π β§ βπ£ β πΎ (π β π£ β βπ β π βπ β (β€β₯βπ)(πΊβπ) β π£)))) |
148 | 144, 147 | anbi12d 632 |
. . 3
β’ (π β ((πΉ(βπ‘βπ½)π
β§ πΊ(βπ‘βπΎ)π) β ((π
β π β§ βπ’ β π½ (π
β π’ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’)) β§ (π β π β§ βπ£ β πΎ (π β π£ β βπ β π βπ β (β€β₯βπ)(πΊβπ) β π£))))) |
149 | | an4 655 |
. . 3
β’ (((π
β π β§ βπ’ β π½ (π
β π’ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’)) β§ (π β π β§ βπ£ β πΎ (π β π£ β βπ β π βπ β (β€β₯βπ)(πΊβπ) β π£))) β ((π
β π β§ π β π) β§ (βπ’ β π½ (π
β π’ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’) β§ βπ£ β πΎ (π β π£ β βπ β π βπ β (β€β₯βπ)(πΊβπ) β π£)))) |
150 | 148, 149 | bitrdi 287 |
. 2
β’ (π β ((πΉ(βπ‘βπ½)π
β§ πΊ(βπ‘βπΎ)π) β ((π
β π β§ π β π) β§ (βπ’ β π½ (π
β π’ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’) β§ βπ£ β πΎ (π β π£ β βπ β π βπ β (β€β₯βπ)(πΊβπ) β π£))))) |
151 | | txtopon 22965 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β (π½ Γt πΎ) β (TopOnβ(π Γ π))) |
152 | 6, 9, 151 | syl2anc 585 |
. . 3
β’ (π β (π½ Γt πΎ) β (TopOnβ(π Γ π))) |
153 | 142 | ffvelcdmda 7039 |
. . . . 5
β’ ((π β§ π β π) β (πΉβπ) β π) |
154 | 145 | ffvelcdmda 7039 |
. . . . 5
β’ ((π β§ π β π) β (πΊβπ) β π) |
155 | 153, 154 | opelxpd 5675 |
. . . 4
β’ ((π β§ π β π) β β¨(πΉβπ), (πΊβπ)β© β (π Γ π)) |
156 | 155, 48 | fmptd 7066 |
. . 3
β’ (π β π»:πβΆ(π Γ π)) |
157 | | eqidd 2734 |
. . 3
β’ ((π β§ π β π) β (π»βπ) = (π»βπ)) |
158 | 152, 41, 141, 156, 157 | lmbrf 22634 |
. 2
β’ (π β (π»(βπ‘β(π½ Γt πΎ))β¨π
, πβ© β (β¨π
, πβ© β (π Γ π) β§ βπ€ β (π½ Γt πΎ)(β¨π
, πβ© β π€ β βπ β π βπ β (β€β₯βπ)(π»βπ) β π€)))) |
159 | 140, 150,
158 | 3bitr4d 311 |
1
β’ (π β ((πΉ(βπ‘βπ½)π
β§ πΊ(βπ‘βπΎ)π) β π»(βπ‘β(π½ Γt πΎ))β¨π
, πβ©)) |