Step | Hyp | Ref
| Expression |
1 | | vex 3451 |
. . . . . . . 8
β’ π’ β V |
2 | | vex 3451 |
. . . . . . . 8
β’ π£ β V |
3 | 1, 2 | xpex 7691 |
. . . . . . 7
β’ (π’ Γ π£) β V |
4 | 3 | rgen2w 3066 |
. . . . . 6
β’
βπ’ β
π½ βπ£ β πΎ (π’ Γ π£) β V |
5 | | eqid 2733 |
. . . . . . 7
β’ (π’ β π½, π£ β πΎ β¦ (π’ Γ π£)) = (π’ β π½, π£ β πΎ β¦ (π’ Γ π£)) |
6 | | eleq2 2823 |
. . . . . . . 8
β’ (π§ = (π’ Γ π£) β (β¨π
, πβ© β π§ β β¨π
, πβ© β (π’ Γ π£))) |
7 | | sseq2 3974 |
. . . . . . . . 9
β’ (π§ = (π’ Γ π£) β ((π» β β) β π§ β (π» β β) β (π’ Γ π£))) |
8 | 7 | rexbidv 3172 |
. . . . . . . 8
β’ (π§ = (π’ Γ π£) β (ββ β πΏ (π» β β) β π§ β ββ β πΏ (π» β β) β (π’ Γ π£))) |
9 | 6, 8 | imbi12d 345 |
. . . . . . 7
β’ (π§ = (π’ Γ π£) β ((β¨π
, πβ© β π§ β ββ β πΏ (π» β β) β π§) β (β¨π
, πβ© β (π’ Γ π£) β ββ β πΏ (π» β β) β (π’ Γ π£)))) |
10 | 5, 9 | ralrnmpo 7498 |
. . . . . 6
β’
(βπ’ β
π½ βπ£ β πΎ (π’ Γ π£) β V β (βπ§ β ran (π’ β π½, π£ β πΎ β¦ (π’ Γ π£))(β¨π
, πβ© β π§ β ββ β πΏ (π» β β) β π§) β βπ’ β π½ βπ£ β πΎ (β¨π
, πβ© β (π’ Γ π£) β ββ β πΏ (π» β β) β (π’ Γ π£)))) |
11 | 4, 10 | ax-mp 5 |
. . . . 5
β’
(βπ§ β
ran (π’ β π½, π£ β πΎ β¦ (π’ Γ π£))(β¨π
, πβ© β π§ β ββ β πΏ (π» β β) β π§) β βπ’ β π½ βπ£ β πΎ (β¨π
, πβ© β (π’ Γ π£) β ββ β πΏ (π» β β) β (π’ Γ π£))) |
12 | | opelxp 5673 |
. . . . . . . . . . . . . . . 16
β’
(β¨π
, πβ© β (π’ Γ π£) β (π
β π’ β§ π β π£)) |
13 | 12 | biancomi 464 |
. . . . . . . . . . . . . . 15
β’
(β¨π
, πβ© β (π’ Γ π£) β (π β π£ β§ π
β π’)) |
14 | 13 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β (β¨π
, πβ© β (π’ Γ π£) β (π β π£ β§ π
β π’))) |
15 | | r19.40 3119 |
. . . . . . . . . . . . . . . . 17
β’
(ββ β
πΏ (βπ β β (πΉβπ) β π’ β§ βπ β β (πΊβπ) β π£) β (ββ β πΏ βπ β β (πΉβπ) β π’ β§ ββ β πΏ βπ β β (πΊβπ) β π£)) |
16 | | raleq 3308 |
. . . . . . . . . . . . . . . . . . 19
β’ (β = π β (βπ β β (πΉβπ) β π’ β βπ β π (πΉβπ) β π’)) |
17 | 16 | cbvrexvw 3225 |
. . . . . . . . . . . . . . . . . 18
β’
(ββ β
πΏ βπ β β (πΉβπ) β π’ β βπ β πΏ βπ β π (πΉβπ) β π’) |
18 | | raleq 3308 |
. . . . . . . . . . . . . . . . . . 19
β’ (β = π β (βπ β β (πΊβπ) β π£ β βπ β π (πΊβπ) β π£)) |
19 | 18 | cbvrexvw 3225 |
. . . . . . . . . . . . . . . . . 18
β’
(ββ β
πΏ βπ β β (πΊβπ) β π£ β βπ β πΏ βπ β π (πΊβπ) β π£) |
20 | 17, 19 | anbi12i 628 |
. . . . . . . . . . . . . . . . 17
β’
((ββ β
πΏ βπ β β (πΉβπ) β π’ β§ ββ β πΏ βπ β β (πΊβπ) β π£) β (βπ β πΏ βπ β π (πΉβπ) β π’ β§ βπ β πΏ βπ β π (πΊβπ) β π£)) |
21 | 15, 20 | sylib 217 |
. . . . . . . . . . . . . . . 16
β’
(ββ β
πΏ (βπ β β (πΉβπ) β π’ β§ βπ β β (πΊβπ) β π£) β (βπ β πΏ βπ β π (πΉβπ) β π’ β§ βπ β πΏ βπ β π (πΊβπ) β π£)) |
22 | | reeanv 3216 |
. . . . . . . . . . . . . . . . 17
β’
(βπ β
πΏ βπ β πΏ (βπ β π (πΉβπ) β π’ β§ βπ β π (πΊβπ) β π£) β (βπ β πΏ βπ β π (πΉβπ) β π’ β§ βπ β πΏ βπ β π (πΊβπ) β π£)) |
23 | | txflf.l |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β πΏ β (Filβπ)) |
24 | | filin 23228 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((πΏ β (Filβπ) β§ π β πΏ β§ π β πΏ) β (π β© π) β πΏ) |
25 | 24 | 3expb 1121 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((πΏ β (Filβπ) β§ (π β πΏ β§ π β πΏ)) β (π β© π) β πΏ) |
26 | 23, 25 | sylan 581 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ (π β πΏ β§ π β πΏ)) β (π β© π) β πΏ) |
27 | | inss1 4192 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β© π) β π |
28 | | ssralv 4014 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β© π) β π β (βπ β π (πΉβπ) β π’ β βπ β (π β© π)(πΉβπ) β π’)) |
29 | 27, 28 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(βπ β
π (πΉβπ) β π’ β βπ β (π β© π)(πΉβπ) β π’) |
30 | | inss2 4193 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β© π) β π |
31 | | ssralv 4014 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β© π) β π β (βπ β π (πΊβπ) β π£ β βπ β (π β© π)(πΊβπ) β π£)) |
32 | 30, 31 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(βπ β
π (πΊβπ) β π£ β βπ β (π β© π)(πΊβπ) β π£) |
33 | 29, 32 | anim12i 614 |
. . . . . . . . . . . . . . . . . . . 20
β’
((βπ β
π (πΉβπ) β π’ β§ βπ β π (πΊβπ) β π£) β (βπ β (π β© π)(πΉβπ) β π’ β§ βπ β (π β© π)(πΊβπ) β π£)) |
34 | | raleq 3308 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (β = (π β© π) β (βπ β β (πΉβπ) β π’ β βπ β (π β© π)(πΉβπ) β π’)) |
35 | | raleq 3308 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (β = (π β© π) β (βπ β β (πΊβπ) β π£ β βπ β (π β© π)(πΊβπ) β π£)) |
36 | 34, 35 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (β = (π β© π) β ((βπ β β (πΉβπ) β π’ β§ βπ β β (πΊβπ) β π£) β (βπ β (π β© π)(πΉβπ) β π’ β§ βπ β (π β© π)(πΊβπ) β π£))) |
37 | 36 | rspcev 3583 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β© π) β πΏ β§ (βπ β (π β© π)(πΉβπ) β π’ β§ βπ β (π β© π)(πΊβπ) β π£)) β ββ β πΏ (βπ β β (πΉβπ) β π’ β§ βπ β β (πΊβπ) β π£)) |
38 | 26, 33, 37 | syl2an 597 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ (π β πΏ β§ π β πΏ)) β§ (βπ β π (πΉβπ) β π’ β§ βπ β π (πΊβπ) β π£)) β ββ β πΏ (βπ β β (πΉβπ) β π’ β§ βπ β β (πΊβπ) β π£)) |
39 | 38 | ex 414 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π β πΏ β§ π β πΏ)) β ((βπ β π (πΉβπ) β π’ β§ βπ β π (πΊβπ) β π£) β ββ β πΏ (βπ β β (πΉβπ) β π’ β§ βπ β β (πΊβπ) β π£))) |
40 | 39 | rexlimdvva 3202 |
. . . . . . . . . . . . . . . . 17
β’ (π β (βπ β πΏ βπ β πΏ (βπ β π (πΉβπ) β π’ β§ βπ β π (πΊβπ) β π£) β ββ β πΏ (βπ β β (πΉβπ) β π’ β§ βπ β β (πΊβπ) β π£))) |
41 | 22, 40 | biimtrrid 242 |
. . . . . . . . . . . . . . . 16
β’ (π β ((βπ β πΏ βπ β π (πΉβπ) β π’ β§ βπ β πΏ βπ β π (πΊβπ) β π£) β ββ β πΏ (βπ β β (πΉβπ) β π’ β§ βπ β β (πΊβπ) β π£))) |
42 | 21, 41 | impbid2 225 |
. . . . . . . . . . . . . . 15
β’ (π β (ββ β πΏ (βπ β β (πΉβπ) β π’ β§ βπ β β (πΊβπ) β π£) β (βπ β πΏ βπ β π (πΉβπ) β π’ β§ βπ β πΏ βπ β π (πΊβπ) β π£))) |
43 | | df-ima 5650 |
. . . . . . . . . . . . . . . . . . 19
β’ (π» β β) = ran (π» βΎ β) |
44 | | filelss 23226 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((πΏ β (Filβπ) β§ β β πΏ) β β β π) |
45 | 23, 44 | sylan 581 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ β β πΏ) β β β π) |
46 | | txflf.h |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ π» = (π β π β¦ β¨(πΉβπ), (πΊβπ)β©) |
47 | 46 | reseq1i 5937 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π» βΎ β) = ((π β π β¦ β¨(πΉβπ), (πΊβπ)β©) βΎ β) |
48 | | resmpt 5995 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (β β π β ((π β π β¦ β¨(πΉβπ), (πΊβπ)β©) βΎ β) = (π β β β¦ β¨(πΉβπ), (πΊβπ)β©)) |
49 | 47, 48 | eqtrid 2785 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (β β π β (π» βΎ β) = (π β β β¦ β¨(πΉβπ), (πΊβπ)β©)) |
50 | 45, 49 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ β β πΏ) β (π» βΎ β) = (π β β β¦ β¨(πΉβπ), (πΊβπ)β©)) |
51 | 50 | rneqd 5897 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ β β πΏ) β ran (π» βΎ β) = ran (π β β β¦ β¨(πΉβπ), (πΊβπ)β©)) |
52 | 43, 51 | eqtrid 2785 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ β β πΏ) β (π» β β) = ran (π β β β¦ β¨(πΉβπ), (πΊβπ)β©)) |
53 | 52 | sseq1d 3979 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ β β πΏ) β ((π» β β) β (π’ Γ π£) β ran (π β β β¦ β¨(πΉβπ), (πΊβπ)β©) β (π’ Γ π£))) |
54 | | opelxp 5673 |
. . . . . . . . . . . . . . . . . . 19
β’
(β¨(πΉβπ), (πΊβπ)β© β (π’ Γ π£) β ((πΉβπ) β π’ β§ (πΊβπ) β π£)) |
55 | 54 | ralbii 3093 |
. . . . . . . . . . . . . . . . . 18
β’
(βπ β
β β¨(πΉβπ), (πΊβπ)β© β (π’ Γ π£) β βπ β β ((πΉβπ) β π’ β§ (πΊβπ) β π£)) |
56 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β β¦ β¨(πΉβπ), (πΊβπ)β©) = (π β β β¦ β¨(πΉβπ), (πΊβπ)β©) |
57 | 56 | fmpt 7062 |
. . . . . . . . . . . . . . . . . . 19
β’
(βπ β
β β¨(πΉβπ), (πΊβπ)β© β (π’ Γ π£) β (π β β β¦ β¨(πΉβπ), (πΊβπ)β©):ββΆ(π’ Γ π£)) |
58 | | opex 5425 |
. . . . . . . . . . . . . . . . . . . . 21
β’
β¨(πΉβπ), (πΊβπ)β© β V |
59 | 58, 56 | fnmpti 6648 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β β¦ β¨(πΉβπ), (πΊβπ)β©) Fn β |
60 | | df-f 6504 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β β β¦ β¨(πΉβπ), (πΊβπ)β©):ββΆ(π’ Γ π£) β ((π β β β¦ β¨(πΉβπ), (πΊβπ)β©) Fn β β§ ran (π β β β¦ β¨(πΉβπ), (πΊβπ)β©) β (π’ Γ π£))) |
61 | 59, 60 | mpbiran 708 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β β¦ β¨(πΉβπ), (πΊβπ)β©):ββΆ(π’ Γ π£) β ran (π β β β¦ β¨(πΉβπ), (πΊβπ)β©) β (π’ Γ π£)) |
62 | 57, 61 | bitri 275 |
. . . . . . . . . . . . . . . . . 18
β’
(βπ β
β β¨(πΉβπ), (πΊβπ)β© β (π’ Γ π£) β ran (π β β β¦ β¨(πΉβπ), (πΊβπ)β©) β (π’ Γ π£)) |
63 | | r19.26 3111 |
. . . . . . . . . . . . . . . . . 18
β’
(βπ β
β ((πΉβπ) β π’ β§ (πΊβπ) β π£) β (βπ β β (πΉβπ) β π’ β§ βπ β β (πΊβπ) β π£)) |
64 | 55, 62, 63 | 3bitr3i 301 |
. . . . . . . . . . . . . . . . 17
β’ (ran
(π β β β¦ β¨(πΉβπ), (πΊβπ)β©) β (π’ Γ π£) β (βπ β β (πΉβπ) β π’ β§ βπ β β (πΊβπ) β π£)) |
65 | 53, 64 | bitrdi 287 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ β β πΏ) β ((π» β β) β (π’ Γ π£) β (βπ β β (πΉβπ) β π’ β§ βπ β β (πΊβπ) β π£))) |
66 | 65 | rexbidva 3170 |
. . . . . . . . . . . . . . 15
β’ (π β (ββ β πΏ (π» β β) β (π’ Γ π£) β ββ β πΏ (βπ β β (πΉβπ) β π’ β§ βπ β β (πΊβπ) β π£))) |
67 | | txflf.f |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β πΉ:πβΆπ) |
68 | 67 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β πΏ) β πΉ:πβΆπ) |
69 | 68 | ffund 6676 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β πΏ) β Fun πΉ) |
70 | | filelss 23226 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((πΏ β (Filβπ) β§ π β πΏ) β π β π) |
71 | 23, 70 | sylan 581 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β πΏ) β π β π) |
72 | 68 | fdmd 6683 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β πΏ) β dom πΉ = π) |
73 | 71, 72 | sseqtrrd 3989 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β πΏ) β π β dom πΉ) |
74 | | funimass4 6911 |
. . . . . . . . . . . . . . . . . 18
β’ ((Fun
πΉ β§ π β dom πΉ) β ((πΉ β π) β π’ β βπ β π (πΉβπ) β π’)) |
75 | 69, 73, 74 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β πΏ) β ((πΉ β π) β π’ β βπ β π (πΉβπ) β π’)) |
76 | 75 | rexbidva 3170 |
. . . . . . . . . . . . . . . 16
β’ (π β (βπ β πΏ (πΉ β π) β π’ β βπ β πΏ βπ β π (πΉβπ) β π’)) |
77 | | txflf.g |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β πΊ:πβΆπ) |
78 | 77 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β πΏ) β πΊ:πβΆπ) |
79 | 78 | ffund 6676 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β πΏ) β Fun πΊ) |
80 | | filelss 23226 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((πΏ β (Filβπ) β§ π β πΏ) β π β π) |
81 | 23, 80 | sylan 581 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β πΏ) β π β π) |
82 | 78 | fdmd 6683 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β πΏ) β dom πΊ = π) |
83 | 81, 82 | sseqtrrd 3989 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β πΏ) β π β dom πΊ) |
84 | | funimass4 6911 |
. . . . . . . . . . . . . . . . . 18
β’ ((Fun
πΊ β§ π β dom πΊ) β ((πΊ β π) β π£ β βπ β π (πΊβπ) β π£)) |
85 | 79, 83, 84 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β πΏ) β ((πΊ β π) β π£ β βπ β π (πΊβπ) β π£)) |
86 | 85 | rexbidva 3170 |
. . . . . . . . . . . . . . . 16
β’ (π β (βπ β πΏ (πΊ β π) β π£ β βπ β πΏ βπ β π (πΊβπ) β π£)) |
87 | 76, 86 | anbi12d 632 |
. . . . . . . . . . . . . . 15
β’ (π β ((βπ β πΏ (πΉ β π) β π’ β§ βπ β πΏ (πΊ β π) β π£) β (βπ β πΏ βπ β π (πΉβπ) β π’ β§ βπ β πΏ βπ β π (πΊβπ) β π£))) |
88 | 42, 66, 87 | 3bitr4d 311 |
. . . . . . . . . . . . . 14
β’ (π β (ββ β πΏ (π» β β) β (π’ Γ π£) β (βπ β πΏ (πΉ β π) β π’ β§ βπ β πΏ (πΊ β π) β π£))) |
89 | 14, 88 | imbi12d 345 |
. . . . . . . . . . . . 13
β’ (π β ((β¨π
, πβ© β (π’ Γ π£) β ββ β πΏ (π» β β) β (π’ Γ π£)) β ((π β π£ β§ π
β π’) β (βπ β πΏ (πΉ β π) β π’ β§ βπ β πΏ (πΊ β π) β π£)))) |
90 | | impexp 452 |
. . . . . . . . . . . . 13
β’ (((π β π£ β§ π
β π’) β (βπ β πΏ (πΉ β π) β π’ β§ βπ β πΏ (πΊ β π) β π£)) β (π β π£ β (π
β π’ β (βπ β πΏ (πΉ β π) β π’ β§ βπ β πΏ (πΊ β π) β π£)))) |
91 | 89, 90 | bitrdi 287 |
. . . . . . . . . . . 12
β’ (π β ((β¨π
, πβ© β (π’ Γ π£) β ββ β πΏ (π» β β) β (π’ Γ π£)) β (π β π£ β (π
β π’ β (βπ β πΏ (πΉ β π) β π’ β§ βπ β πΏ (πΊ β π) β π£))))) |
92 | 91 | ralbidv 3171 |
. . . . . . . . . . 11
β’ (π β (βπ£ β πΎ (β¨π
, πβ© β (π’ Γ π£) β ββ β πΏ (π» β β) β (π’ Γ π£)) β βπ£ β πΎ (π β π£ β (π
β π’ β (βπ β πΏ (πΉ β π) β π’ β§ βπ β πΏ (πΊ β π) β π£))))) |
93 | | eleq2 2823 |
. . . . . . . . . . . . 13
β’ (π₯ = π£ β (π β π₯ β π β π£)) |
94 | 93 | ralrab 3655 |
. . . . . . . . . . . 12
β’
(βπ£ β
{π₯ β πΎ β£ π β π₯} (π
β π’ β (βπ β πΏ (πΉ β π) β π’ β§ βπ β πΏ (πΊ β π) β π£)) β βπ£ β πΎ (π β π£ β (π
β π’ β (βπ β πΏ (πΉ β π) β π’ β§ βπ β πΏ (πΊ β π) β π£)))) |
95 | | r19.21v 3173 |
. . . . . . . . . . . 12
β’
(βπ£ β
{π₯ β πΎ β£ π β π₯} (π
β π’ β (βπ β πΏ (πΉ β π) β π’ β§ βπ β πΏ (πΊ β π) β π£)) β (π
β π’ β βπ£ β {π₯ β πΎ β£ π β π₯} (βπ β πΏ (πΉ β π) β π’ β§ βπ β πΏ (πΊ β π) β π£))) |
96 | 94, 95 | bitr3i 277 |
. . . . . . . . . . 11
β’
(βπ£ β
πΎ (π β π£ β (π
β π’ β (βπ β πΏ (πΉ β π) β π’ β§ βπ β πΏ (πΊ β π) β π£))) β (π
β π’ β βπ£ β {π₯ β πΎ β£ π β π₯} (βπ β πΏ (πΉ β π) β π’ β§ βπ β πΏ (πΊ β π) β π£))) |
97 | 92, 96 | bitrdi 287 |
. . . . . . . . . 10
β’ (π β (βπ£ β πΎ (β¨π
, πβ© β (π’ Γ π£) β ββ β πΏ (π» β β) β (π’ Γ π£)) β (π
β π’ β βπ£ β {π₯ β πΎ β£ π β π₯} (βπ β πΏ (πΉ β π) β π’ β§ βπ β πΏ (πΊ β π) β π£)))) |
98 | 97 | ralbidv 3171 |
. . . . . . . . 9
β’ (π β (βπ’ β π½ βπ£ β πΎ (β¨π
, πβ© β (π’ Γ π£) β ββ β πΏ (π» β β) β (π’ Γ π£)) β βπ’ β π½ (π
β π’ β βπ£ β {π₯ β πΎ β£ π β π₯} (βπ β πΏ (πΉ β π) β π’ β§ βπ β πΏ (πΊ β π) β π£)))) |
99 | | eleq2 2823 |
. . . . . . . . . 10
β’ (π₯ = π’ β (π
β π₯ β π
β π’)) |
100 | 99 | ralrab 3655 |
. . . . . . . . 9
β’
(βπ’ β
{π₯ β π½ β£ π
β π₯}βπ£ β {π₯ β πΎ β£ π β π₯} (βπ β πΏ (πΉ β π) β π’ β§ βπ β πΏ (πΊ β π) β π£) β βπ’ β π½ (π
β π’ β βπ£ β {π₯ β πΎ β£ π β π₯} (βπ β πΏ (πΉ β π) β π’ β§ βπ β πΏ (πΊ β π) β π£))) |
101 | 98, 100 | bitr4di 289 |
. . . . . . . 8
β’ (π β (βπ’ β π½ βπ£ β πΎ (β¨π
, πβ© β (π’ Γ π£) β ββ β πΏ (π» β β) β (π’ Γ π£)) β βπ’ β {π₯ β π½ β£ π
β π₯}βπ£ β {π₯ β πΎ β£ π β π₯} (βπ β πΏ (πΉ β π) β π’ β§ βπ β πΏ (πΊ β π) β π£))) |
102 | 101 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π
β π β§ π β π)) β (βπ’ β π½ βπ£ β πΎ (β¨π
, πβ© β (π’ Γ π£) β ββ β πΏ (π» β β) β (π’ Γ π£)) β βπ’ β {π₯ β π½ β£ π
β π₯}βπ£ β {π₯ β πΎ β£ π β π₯} (βπ β πΏ (πΉ β π) β π’ β§ βπ β πΏ (πΊ β π) β π£))) |
103 | | txflf.j |
. . . . . . . . . . 11
β’ (π β π½ β (TopOnβπ)) |
104 | | toponmax 22298 |
. . . . . . . . . . 11
β’ (π½ β (TopOnβπ) β π β π½) |
105 | 103, 104 | syl 17 |
. . . . . . . . . 10
β’ (π β π β π½) |
106 | | eleq2 2823 |
. . . . . . . . . . . 12
β’ (π₯ = π β (π
β π₯ β π
β π)) |
107 | 106 | rspcev 3583 |
. . . . . . . . . . 11
β’ ((π β π½ β§ π
β π) β βπ₯ β π½ π
β π₯) |
108 | | rabn0 4349 |
. . . . . . . . . . 11
β’ ({π₯ β π½ β£ π
β π₯} β β
β βπ₯ β π½ π
β π₯) |
109 | 107, 108 | sylibr 233 |
. . . . . . . . . 10
β’ ((π β π½ β§ π
β π) β {π₯ β π½ β£ π
β π₯} β β
) |
110 | 105, 109 | sylan 581 |
. . . . . . . . 9
β’ ((π β§ π
β π) β {π₯ β π½ β£ π
β π₯} β β
) |
111 | | txflf.k |
. . . . . . . . . . 11
β’ (π β πΎ β (TopOnβπ)) |
112 | | toponmax 22298 |
. . . . . . . . . . 11
β’ (πΎ β (TopOnβπ) β π β πΎ) |
113 | 111, 112 | syl 17 |
. . . . . . . . . 10
β’ (π β π β πΎ) |
114 | | eleq2 2823 |
. . . . . . . . . . . 12
β’ (π₯ = π β (π β π₯ β π β π)) |
115 | 114 | rspcev 3583 |
. . . . . . . . . . 11
β’ ((π β πΎ β§ π β π) β βπ₯ β πΎ π β π₯) |
116 | | rabn0 4349 |
. . . . . . . . . . 11
β’ ({π₯ β πΎ β£ π β π₯} β β
β βπ₯ β πΎ π β π₯) |
117 | 115, 116 | sylibr 233 |
. . . . . . . . . 10
β’ ((π β πΎ β§ π β π) β {π₯ β πΎ β£ π β π₯} β β
) |
118 | 113, 117 | sylan 581 |
. . . . . . . . 9
β’ ((π β§ π β π) β {π₯ β πΎ β£ π β π₯} β β
) |
119 | 110, 118 | anim12dan 620 |
. . . . . . . 8
β’ ((π β§ (π
β π β§ π β π)) β ({π₯ β π½ β£ π
β π₯} β β
β§ {π₯ β πΎ β£ π β π₯} β β
)) |
120 | | r19.28zv 4462 |
. . . . . . . . . 10
β’ ({π₯ β πΎ β£ π β π₯} β β
β (βπ£ β {π₯ β πΎ β£ π β π₯} (βπ β πΏ (πΉ β π) β π’ β§ βπ β πΏ (πΊ β π) β π£) β (βπ β πΏ (πΉ β π) β π’ β§ βπ£ β {π₯ β πΎ β£ π β π₯}βπ β πΏ (πΊ β π) β π£))) |
121 | 120 | ralbidv 3171 |
. . . . . . . . 9
β’ ({π₯ β πΎ β£ π β π₯} β β
β (βπ’ β {π₯ β π½ β£ π
β π₯}βπ£ β {π₯ β πΎ β£ π β π₯} (βπ β πΏ (πΉ β π) β π’ β§ βπ β πΏ (πΊ β π) β π£) β βπ’ β {π₯ β π½ β£ π
β π₯} (βπ β πΏ (πΉ β π) β π’ β§ βπ£ β {π₯ β πΎ β£ π β π₯}βπ β πΏ (πΊ β π) β π£))) |
122 | | r19.27zv 4467 |
. . . . . . . . 9
β’ ({π₯ β π½ β£ π
β π₯} β β
β (βπ’ β {π₯ β π½ β£ π
β π₯} (βπ β πΏ (πΉ β π) β π’ β§ βπ£ β {π₯ β πΎ β£ π β π₯}βπ β πΏ (πΊ β π) β π£) β (βπ’ β {π₯ β π½ β£ π
β π₯}βπ β πΏ (πΉ β π) β π’ β§ βπ£ β {π₯ β πΎ β£ π β π₯}βπ β πΏ (πΊ β π) β π£))) |
123 | 121, 122 | sylan9bbr 512 |
. . . . . . . 8
β’ (({π₯ β π½ β£ π
β π₯} β β
β§ {π₯ β πΎ β£ π β π₯} β β
) β (βπ’ β {π₯ β π½ β£ π
β π₯}βπ£ β {π₯ β πΎ β£ π β π₯} (βπ β πΏ (πΉ β π) β π’ β§ βπ β πΏ (πΊ β π) β π£) β (βπ’ β {π₯ β π½ β£ π
β π₯}βπ β πΏ (πΉ β π) β π’ β§ βπ£ β {π₯ β πΎ β£ π β π₯}βπ β πΏ (πΊ β π) β π£))) |
124 | 119, 123 | syl 17 |
. . . . . . 7
β’ ((π β§ (π
β π β§ π β π)) β (βπ’ β {π₯ β π½ β£ π
β π₯}βπ£ β {π₯ β πΎ β£ π β π₯} (βπ β πΏ (πΉ β π) β π’ β§ βπ β πΏ (πΊ β π) β π£) β (βπ’ β {π₯ β π½ β£ π
β π₯}βπ β πΏ (πΉ β π) β π’ β§ βπ£ β {π₯ β πΎ β£ π β π₯}βπ β πΏ (πΊ β π) β π£))) |
125 | 102, 124 | bitrd 279 |
. . . . . 6
β’ ((π β§ (π
β π β§ π β π)) β (βπ’ β π½ βπ£ β πΎ (β¨π
, πβ© β (π’ Γ π£) β ββ β πΏ (π» β β) β (π’ Γ π£)) β (βπ’ β {π₯ β π½ β£ π
β π₯}βπ β πΏ (πΉ β π) β π’ β§ βπ£ β {π₯ β πΎ β£ π β π₯}βπ β πΏ (πΊ β π) β π£))) |
126 | 99 | ralrab 3655 |
. . . . . . 7
β’
(βπ’ β
{π₯ β π½ β£ π
β π₯}βπ β πΏ (πΉ β π) β π’ β βπ’ β π½ (π
β π’ β βπ β πΏ (πΉ β π) β π’)) |
127 | 93 | ralrab 3655 |
. . . . . . 7
β’
(βπ£ β
{π₯ β πΎ β£ π β π₯}βπ β πΏ (πΊ β π) β π£ β βπ£ β πΎ (π β π£ β βπ β πΏ (πΊ β π) β π£)) |
128 | 126, 127 | anbi12i 628 |
. . . . . 6
β’
((βπ’ β
{π₯ β π½ β£ π
β π₯}βπ β πΏ (πΉ β π) β π’ β§ βπ£ β {π₯ β πΎ β£ π β π₯}βπ β πΏ (πΊ β π) β π£) β (βπ’ β π½ (π
β π’ β βπ β πΏ (πΉ β π) β π’) β§ βπ£ β πΎ (π β π£ β βπ β πΏ (πΊ β π) β π£))) |
129 | 125, 128 | bitrdi 287 |
. . . . 5
β’ ((π β§ (π
β π β§ π β π)) β (βπ’ β π½ βπ£ β πΎ (β¨π
, πβ© β (π’ Γ π£) β ββ β πΏ (π» β β) β (π’ Γ π£)) β (βπ’ β π½ (π
β π’ β βπ β πΏ (πΉ β π) β π’) β§ βπ£ β πΎ (π β π£ β βπ β πΏ (πΊ β π) β π£)))) |
130 | 11, 129 | bitrid 283 |
. . . 4
β’ ((π β§ (π
β π β§ π β π)) β (βπ§ β ran (π’ β π½, π£ β πΎ β¦ (π’ Γ π£))(β¨π
, πβ© β π§ β ββ β πΏ (π» β β) β π§) β (βπ’ β π½ (π
β π’ β βπ β πΏ (πΉ β π) β π’) β§ βπ£ β πΎ (π β π£ β βπ β πΏ (πΊ β π) β π£)))) |
131 | 130 | pm5.32da 580 |
. . 3
β’ (π β (((π
β π β§ π β π) β§ βπ§ β ran (π’ β π½, π£ β πΎ β¦ (π’ Γ π£))(β¨π
, πβ© β π§ β ββ β πΏ (π» β β) β π§)) β ((π
β π β§ π β π) β§ (βπ’ β π½ (π
β π’ β βπ β πΏ (πΉ β π) β π’) β§ βπ£ β πΎ (π β π£ β βπ β πΏ (πΊ β π) β π£))))) |
132 | | opelxp 5673 |
. . . 4
β’
(β¨π
, πβ© β (π Γ π) β (π
β π β§ π β π)) |
133 | 132 | anbi1i 625 |
. . 3
β’
((β¨π
, πβ© β (π Γ π) β§ βπ§ β ran (π’ β π½, π£ β πΎ β¦ (π’ Γ π£))(β¨π
, πβ© β π§ β ββ β πΏ (π» β β) β π§)) β ((π
β π β§ π β π) β§ βπ§ β ran (π’ β π½, π£ β πΎ β¦ (π’ Γ π£))(β¨π
, πβ© β π§ β ββ β πΏ (π» β β) β π§))) |
134 | | an4 655 |
. . 3
β’ (((π
β π β§ βπ’ β π½ (π
β π’ β βπ β πΏ (πΉ β π) β π’)) β§ (π β π β§ βπ£ β πΎ (π β π£ β βπ β πΏ (πΊ β π) β π£))) β ((π
β π β§ π β π) β§ (βπ’ β π½ (π
β π’ β βπ β πΏ (πΉ β π) β π’) β§ βπ£ β πΎ (π β π£ β βπ β πΏ (πΊ β π) β π£)))) |
135 | 131, 133,
134 | 3bitr4g 314 |
. 2
β’ (π β ((β¨π
, πβ© β (π Γ π) β§ βπ§ β ran (π’ β π½, π£ β πΎ β¦ (π’ Γ π£))(β¨π
, πβ© β π§ β ββ β πΏ (π» β β) β π§)) β ((π
β π β§ βπ’ β π½ (π
β π’ β βπ β πΏ (πΉ β π) β π’)) β§ (π β π β§ βπ£ β πΎ (π β π£ β βπ β πΏ (πΊ β π) β π£))))) |
136 | | eqid 2733 |
. . . . . . . 8
β’ ran
(π’ β π½, π£ β πΎ β¦ (π’ Γ π£)) = ran (π’ β π½, π£ β πΎ β¦ (π’ Γ π£)) |
137 | 136 | txval 22938 |
. . . . . . 7
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β (π½ Γt πΎ) = (topGenβran (π’ β π½, π£ β πΎ β¦ (π’ Γ π£)))) |
138 | 103, 111,
137 | syl2anc 585 |
. . . . . 6
β’ (π β (π½ Γt πΎ) = (topGenβran (π’ β π½, π£ β πΎ β¦ (π’ Γ π£)))) |
139 | 138 | oveq1d 7376 |
. . . . 5
β’ (π β ((π½ Γt πΎ) fLimf πΏ) = ((topGenβran (π’ β π½, π£ β πΎ β¦ (π’ Γ π£))) fLimf πΏ)) |
140 | 139 | fveq1d 6848 |
. . . 4
β’ (π β (((π½ Γt πΎ) fLimf πΏ)βπ») = (((topGenβran (π’ β π½, π£ β πΎ β¦ (π’ Γ π£))) fLimf πΏ)βπ»)) |
141 | 140 | eleq2d 2820 |
. . 3
β’ (π β (β¨π
, πβ© β (((π½ Γt πΎ) fLimf πΏ)βπ») β β¨π
, πβ© β (((topGenβran (π’ β π½, π£ β πΎ β¦ (π’ Γ π£))) fLimf πΏ)βπ»))) |
142 | | txtopon 22965 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β (π½ Γt πΎ) β (TopOnβ(π Γ π))) |
143 | 103, 111,
142 | syl2anc 585 |
. . . . 5
β’ (π β (π½ Γt πΎ) β (TopOnβ(π Γ π))) |
144 | 138, 143 | eqeltrrd 2835 |
. . . 4
β’ (π β (topGenβran (π’ β π½, π£ β πΎ β¦ (π’ Γ π£))) β (TopOnβ(π Γ π))) |
145 | 67 | ffvelcdmda 7039 |
. . . . . 6
β’ ((π β§ π β π) β (πΉβπ) β π) |
146 | 77 | ffvelcdmda 7039 |
. . . . . 6
β’ ((π β§ π β π) β (πΊβπ) β π) |
147 | 145, 146 | opelxpd 5675 |
. . . . 5
β’ ((π β§ π β π) β β¨(πΉβπ), (πΊβπ)β© β (π Γ π)) |
148 | 147, 46 | fmptd 7066 |
. . . 4
β’ (π β π»:πβΆ(π Γ π)) |
149 | | eqid 2733 |
. . . . 5
β’
(topGenβran (π’
β π½, π£ β πΎ β¦ (π’ Γ π£))) = (topGenβran (π’ β π½, π£ β πΎ β¦ (π’ Γ π£))) |
150 | 149 | flftg 23370 |
. . . 4
β’
(((topGenβran (π’ β π½, π£ β πΎ β¦ (π’ Γ π£))) β (TopOnβ(π Γ π)) β§ πΏ β (Filβπ) β§ π»:πβΆ(π Γ π)) β (β¨π
, πβ© β (((topGenβran (π’ β π½, π£ β πΎ β¦ (π’ Γ π£))) fLimf πΏ)βπ») β (β¨π
, πβ© β (π Γ π) β§ βπ§ β ran (π’ β π½, π£ β πΎ β¦ (π’ Γ π£))(β¨π
, πβ© β π§ β ββ β πΏ (π» β β) β π§)))) |
151 | 144, 23, 148, 150 | syl3anc 1372 |
. . 3
β’ (π β (β¨π
, πβ© β (((topGenβran (π’ β π½, π£ β πΎ β¦ (π’ Γ π£))) fLimf πΏ)βπ») β (β¨π
, πβ© β (π Γ π) β§ βπ§ β ran (π’ β π½, π£ β πΎ β¦ (π’ Γ π£))(β¨π
, πβ© β π§ β ββ β πΏ (π» β β) β π§)))) |
152 | 141, 151 | bitrd 279 |
. 2
β’ (π β (β¨π
, πβ© β (((π½ Γt πΎ) fLimf πΏ)βπ») β (β¨π
, πβ© β (π Γ π) β§ βπ§ β ran (π’ β π½, π£ β πΎ β¦ (π’ Γ π£))(β¨π
, πβ© β π§ β ββ β πΏ (π» β β) β π§)))) |
153 | | isflf 23367 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β (π
β ((π½ fLimf πΏ)βπΉ) β (π
β π β§ βπ’ β π½ (π
β π’ β βπ β πΏ (πΉ β π) β π’)))) |
154 | 103, 23, 67, 153 | syl3anc 1372 |
. . 3
β’ (π β (π
β ((π½ fLimf πΏ)βπΉ) β (π
β π β§ βπ’ β π½ (π
β π’ β βπ β πΏ (πΉ β π) β π’)))) |
155 | | isflf 23367 |
. . . 4
β’ ((πΎ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΊ:πβΆπ) β (π β ((πΎ fLimf πΏ)βπΊ) β (π β π β§ βπ£ β πΎ (π β π£ β βπ β πΏ (πΊ β π) β π£)))) |
156 | 111, 23, 77, 155 | syl3anc 1372 |
. . 3
β’ (π β (π β ((πΎ fLimf πΏ)βπΊ) β (π β π β§ βπ£ β πΎ (π β π£ β βπ β πΏ (πΊ β π) β π£)))) |
157 | 154, 156 | anbi12d 632 |
. 2
β’ (π β ((π
β ((π½ fLimf πΏ)βπΉ) β§ π β ((πΎ fLimf πΏ)βπΊ)) β ((π
β π β§ βπ’ β π½ (π
β π’ β βπ β πΏ (πΉ β π) β π’)) β§ (π β π β§ βπ£ β πΎ (π β π£ β βπ β πΏ (πΊ β π) β π£))))) |
158 | 135, 152,
157 | 3bitr4d 311 |
1
β’ (π β (β¨π
, πβ© β (((π½ Γt πΎ) fLimf πΏ)βπ») β (π
β ((π½ fLimf πΏ)βπΉ) β§ π β ((πΎ fLimf πΏ)βπΊ)))) |