Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. . . . . . . 8
β’ (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))) = (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))) |
2 | | fvex 6856 |
. . . . . . . 8
β’ (πΉβ(π Β· π)) β V |
3 | 1, 2 | fnmpoi 8003 |
. . . . . . 7
β’ (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))) Fn (πΎ Γ {(πΉβπ)}) |
4 | | fnrel 6605 |
. . . . . . 7
β’ ((π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))) Fn (πΎ Γ {(πΉβπ)}) β Rel (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π)))) |
5 | 3, 4 | ax-mp 5 |
. . . . . 6
β’ Rel
(π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))) |
6 | 5 | rgenw 3069 |
. . . . 5
β’
βπ β
π Rel (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))) |
7 | | reliun 5773 |
. . . . 5
β’ (Rel
βͺ π β π (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))) β βπ β π Rel (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π)))) |
8 | 6, 7 | mpbir 230 |
. . . 4
β’ Rel
βͺ π β π (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))) |
9 | | imasvscaf.u |
. . . . . 6
β’ (π β π = (πΉ βs π
)) |
10 | | imasvscaf.v |
. . . . . 6
β’ (π β π = (Baseβπ
)) |
11 | | imasvscaf.f |
. . . . . 6
β’ (π β πΉ:πβontoβπ΅) |
12 | | imasvscaf.r |
. . . . . 6
β’ (π β π
β π) |
13 | | imasvscaf.g |
. . . . . 6
β’ πΊ = (Scalarβπ
) |
14 | | imasvscaf.k |
. . . . . 6
β’ πΎ = (BaseβπΊ) |
15 | | imasvscaf.q |
. . . . . 6
β’ Β· = (
Β·π βπ
) |
16 | | imasvscaf.s |
. . . . . 6
β’ β = (
Β·π βπ) |
17 | 9, 10, 11, 12, 13, 14, 15, 16 | imasvsca 17403 |
. . . . 5
β’ (π β β = βͺ π β π (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π)))) |
18 | 17 | releqd 5735 |
. . . 4
β’ (π β (Rel β β Rel βͺ π β π (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))))) |
19 | 8, 18 | mpbiri 258 |
. . 3
β’ (π β Rel β ) |
20 | | dffn2 6671 |
. . . . . . . . . . . . 13
β’ ((π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))) Fn (πΎ Γ {(πΉβπ)}) β (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))):(πΎ Γ {(πΉβπ)})βΆV) |
21 | 3, 20 | mpbi 229 |
. . . . . . . . . . . 12
β’ (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))):(πΎ Γ {(πΉβπ)})βΆV |
22 | | fssxp 6697 |
. . . . . . . . . . . 12
β’ ((π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))):(πΎ Γ {(πΉβπ)})βΆV β (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))) β ((πΎ Γ {(πΉβπ)}) Γ V)) |
23 | 21, 22 | ax-mp 5 |
. . . . . . . . . . 11
β’ (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))) β ((πΎ Γ {(πΉβπ)}) Γ V) |
24 | | fof 6757 |
. . . . . . . . . . . . . . 15
β’ (πΉ:πβontoβπ΅ β πΉ:πβΆπ΅) |
25 | 11, 24 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β πΉ:πβΆπ΅) |
26 | 25 | ffvelcdmda 7036 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π) β (πΉβπ) β π΅) |
27 | 26 | snssd 4770 |
. . . . . . . . . . . 12
β’ ((π β§ π β π) β {(πΉβπ)} β π΅) |
28 | | xpss2 5654 |
. . . . . . . . . . . 12
β’ ({(πΉβπ)} β π΅ β (πΎ Γ {(πΉβπ)}) β (πΎ Γ π΅)) |
29 | | xpss1 5653 |
. . . . . . . . . . . 12
β’ ((πΎ Γ {(πΉβπ)}) β (πΎ Γ π΅) β ((πΎ Γ {(πΉβπ)}) Γ V) β ((πΎ Γ π΅) Γ V)) |
30 | 27, 28, 29 | 3syl 18 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β ((πΎ Γ {(πΉβπ)}) Γ V) β ((πΎ Γ π΅) Γ V)) |
31 | 23, 30 | sstrid 3956 |
. . . . . . . . . 10
β’ ((π β§ π β π) β (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))) β ((πΎ Γ π΅) Γ V)) |
32 | 31 | ralrimiva 3144 |
. . . . . . . . 9
β’ (π β βπ β π (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))) β ((πΎ Γ π΅) Γ V)) |
33 | | iunss 5006 |
. . . . . . . . 9
β’ (βͺ π β π (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))) β ((πΎ Γ π΅) Γ V) β βπ β π (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))) β ((πΎ Γ π΅) Γ V)) |
34 | 32, 33 | sylibr 233 |
. . . . . . . 8
β’ (π β βͺ π β π (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))) β ((πΎ Γ π΅) Γ V)) |
35 | 17, 34 | eqsstrd 3983 |
. . . . . . 7
β’ (π β β β ((πΎ Γ π΅) Γ V)) |
36 | | dmss 5859 |
. . . . . . 7
β’ ( β
β ((πΎ Γ π΅) Γ V) β dom β
β dom ((πΎ Γ
π΅) Γ
V)) |
37 | 35, 36 | syl 17 |
. . . . . 6
β’ (π β dom β β dom ((πΎ Γ π΅) Γ V)) |
38 | | vn0 4299 |
. . . . . . 7
β’ V β
β
|
39 | | dmxp 5885 |
. . . . . . 7
β’ (V β
β
β dom ((πΎ
Γ π΅) Γ V) =
(πΎ Γ π΅)) |
40 | 38, 39 | ax-mp 5 |
. . . . . 6
β’ dom
((πΎ Γ π΅) Γ V) = (πΎ Γ π΅) |
41 | 37, 40 | sseqtrdi 3995 |
. . . . 5
β’ (π β dom β β (πΎ Γ π΅)) |
42 | | forn 6760 |
. . . . . . 7
β’ (πΉ:πβontoβπ΅ β ran πΉ = π΅) |
43 | 11, 42 | syl 17 |
. . . . . 6
β’ (π β ran πΉ = π΅) |
44 | 43 | xpeq2d 5664 |
. . . . 5
β’ (π β (πΎ Γ ran πΉ) = (πΎ Γ π΅)) |
45 | 41, 44 | sseqtrrd 3986 |
. . . 4
β’ (π β dom β β (πΎ Γ ran πΉ)) |
46 | | df-br 5107 |
. . . . . . . . . 10
β’
(β¨π, (πΉβπ)β© β π€ β β¨β¨π, (πΉβπ)β©, π€β© β β ) |
47 | 17 | eleq2d 2824 |
. . . . . . . . . . . 12
β’ (π β (β¨β¨π, (πΉβπ)β©, π€β© β β β
β¨β¨π, (πΉβπ)β©, π€β© β βͺ π β π (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))))) |
48 | 47 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ (π β πΎ β§ π β π)) β (β¨β¨π, (πΉβπ)β©, π€β© β β β
β¨β¨π, (πΉβπ)β©, π€β© β βͺ π β π (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))))) |
49 | | eliun 4959 |
. . . . . . . . . . . 12
β’
(β¨β¨π,
(πΉβπ)β©, π€β© β βͺ π β π (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))) β βπ β π β¨β¨π, (πΉβπ)β©, π€β© β (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π)))) |
50 | | df-3an 1090 |
. . . . . . . . . . . . . . 15
β’ ((π β πΎ β§ π β π β§ π β π) β ((π β πΎ β§ π β π) β§ π β π)) |
51 | 1 | mpofun 7481 |
. . . . . . . . . . . . . . . . . . . 20
β’ Fun
(π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))) |
52 | | funopfv 6895 |
. . . . . . . . . . . . . . . . . . . 20
β’ (Fun
(π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))) β (β¨β¨π, (πΉβπ)β©, π€β© β (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))) β ((π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π)))ββ¨π, (πΉβπ)β©) = π€)) |
53 | 51, 52 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
β’
(β¨β¨π,
(πΉβπ)β©, π€β© β (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))) β ((π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π)))ββ¨π, (πΉβπ)β©) = π€) |
54 | | df-ov 7361 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π(π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π)))(πΉβπ)) = ((π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π)))ββ¨π, (πΉβπ)β©) |
55 | | opex 5422 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
β¨π, (πΉβπ)β© β V |
56 | | vex 3450 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ π€ β V |
57 | 55, 56 | opeldm 5864 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(β¨β¨π,
(πΉβπ)β©, π€β© β (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))) β β¨π, (πΉβπ)β© β dom (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π)))) |
58 | 1, 2 | dmmpo 8004 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ dom
(π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))) = (πΎ Γ {(πΉβπ)}) |
59 | 57, 58 | eleqtrdi 2848 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(β¨β¨π,
(πΉβπ)β©, π€β© β (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))) β β¨π, (πΉβπ)β© β (πΎ Γ {(πΉβπ)})) |
60 | | opelxp 5670 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(β¨π, (πΉβπ)β© β (πΎ Γ {(πΉβπ)}) β (π β πΎ β§ (πΉβπ) β {(πΉβπ)})) |
61 | 59, 60 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(β¨β¨π,
(πΉβπ)β©, π€β© β (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))) β (π β πΎ β§ (πΉβπ) β {(πΉβπ)})) |
62 | | fvoveq1 7381 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π§ = π β (πΉβ(π§ Β· π)) = (πΉβ(π Β· π))) |
63 | | eqidd 2738 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π¦ = (πΉβπ) β (πΉβ(π Β· π)) = (πΉβ(π Β· π))) |
64 | | fvoveq1 7381 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = π§ β (πΉβ(π Β· π)) = (πΉβ(π§ Β· π))) |
65 | | eqidd 2738 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π₯ = π¦ β (πΉβ(π§ Β· π)) = (πΉβ(π§ Β· π))) |
66 | 64, 65 | cbvmpov 7453 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))) = (π§ β πΎ, π¦ β {(πΉβπ)} β¦ (πΉβ(π§ Β· π))) |
67 | 62, 63, 66, 2 | ovmpo 7516 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β πΎ β§ (πΉβπ) β {(πΉβπ)}) β (π(π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π)))(πΉβπ)) = (πΉβ(π Β· π))) |
68 | 61, 67 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’
(β¨β¨π,
(πΉβπ)β©, π€β© β (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))) β (π(π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π)))(πΉβπ)) = (πΉβ(π Β· π))) |
69 | 54, 68 | eqtr3id 2791 |
. . . . . . . . . . . . . . . . . . 19
β’
(β¨β¨π,
(πΉβπ)β©, π€β© β (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))) β ((π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π)))ββ¨π, (πΉβπ)β©) = (πΉβ(π Β· π))) |
70 | 53, 69 | eqtr3d 2779 |
. . . . . . . . . . . . . . . . . 18
β’
(β¨β¨π,
(πΉβπ)β©, π€β© β (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))) β π€ = (πΉβ(π Β· π))) |
71 | 70 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π β πΎ β§ π β π β§ π β π)) β§ β¨β¨π, (πΉβπ)β©, π€β© β (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π)))) β π€ = (πΉβ(π Β· π))) |
72 | | imasvscaf.e |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π β πΎ β§ π β π β§ π β π)) β ((πΉβπ) = (πΉβπ) β (πΉβ(π Β· π)) = (πΉβ(π Β· π)))) |
73 | | elsni 4604 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΉβπ) β {(πΉβπ)} β (πΉβπ) = (πΉβπ)) |
74 | 61, 73 | simpl2im 505 |
. . . . . . . . . . . . . . . . . 18
β’
(β¨β¨π,
(πΉβπ)β©, π€β© β (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))) β (πΉβπ) = (πΉβπ)) |
75 | 72, 74 | impel 507 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π β πΎ β§ π β π β§ π β π)) β§ β¨β¨π, (πΉβπ)β©, π€β© β (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π)))) β (πΉβ(π Β· π)) = (πΉβ(π Β· π))) |
76 | 71, 75 | eqtr4d 2780 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β πΎ β§ π β π β§ π β π)) β§ β¨β¨π, (πΉβπ)β©, π€β© β (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π)))) β π€ = (πΉβ(π Β· π))) |
77 | 76 | ex 414 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β πΎ β§ π β π β§ π β π)) β (β¨β¨π, (πΉβπ)β©, π€β© β (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))) β π€ = (πΉβ(π Β· π)))) |
78 | 50, 77 | sylan2br 596 |
. . . . . . . . . . . . . 14
β’ ((π β§ ((π β πΎ β§ π β π) β§ π β π)) β (β¨β¨π, (πΉβπ)β©, π€β© β (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))) β π€ = (πΉβ(π Β· π)))) |
79 | 78 | anassrs 469 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β πΎ β§ π β π)) β§ π β π) β (β¨β¨π, (πΉβπ)β©, π€β© β (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))) β π€ = (πΉβ(π Β· π)))) |
80 | 79 | rexlimdva 3153 |
. . . . . . . . . . . 12
β’ ((π β§ (π β πΎ β§ π β π)) β (βπ β π β¨β¨π, (πΉβπ)β©, π€β© β (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))) β π€ = (πΉβ(π Β· π)))) |
81 | 49, 80 | biimtrid 241 |
. . . . . . . . . . 11
β’ ((π β§ (π β πΎ β§ π β π)) β (β¨β¨π, (πΉβπ)β©, π€β© β βͺ π β π (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))) β π€ = (πΉβ(π Β· π)))) |
82 | 48, 81 | sylbid 239 |
. . . . . . . . . 10
β’ ((π β§ (π β πΎ β§ π β π)) β (β¨β¨π, (πΉβπ)β©, π€β© β β β π€ = (πΉβ(π Β· π)))) |
83 | 46, 82 | biimtrid 241 |
. . . . . . . . 9
β’ ((π β§ (π β πΎ β§ π β π)) β (β¨π, (πΉβπ)β© β π€ β π€ = (πΉβ(π Β· π)))) |
84 | 83 | alrimiv 1931 |
. . . . . . . 8
β’ ((π β§ (π β πΎ β§ π β π)) β βπ€(β¨π, (πΉβπ)β© β π€ β π€ = (πΉβ(π Β· π)))) |
85 | | mo2icl 3673 |
. . . . . . . 8
β’
(βπ€(β¨π, (πΉβπ)β© β π€ β π€ = (πΉβ(π Β· π))) β β*π€β¨π, (πΉβπ)β© β π€) |
86 | 84, 85 | syl 17 |
. . . . . . 7
β’ ((π β§ (π β πΎ β§ π β π)) β β*π€β¨π, (πΉβπ)β© β π€) |
87 | 86 | ralrimivva 3198 |
. . . . . 6
β’ (π β βπ β πΎ βπ β π β*π€β¨π, (πΉβπ)β© β π€) |
88 | | fofn 6759 |
. . . . . . . 8
β’ (πΉ:πβontoβπ΅ β πΉ Fn π) |
89 | | opeq2 4832 |
. . . . . . . . . . 11
β’ (π¦ = (πΉβπ) β β¨π, π¦β© = β¨π, (πΉβπ)β©) |
90 | 89 | breq1d 5116 |
. . . . . . . . . 10
β’ (π¦ = (πΉβπ) β (β¨π, π¦β© β π€ β β¨π, (πΉβπ)β© β π€)) |
91 | 90 | mobidv 2548 |
. . . . . . . . 9
β’ (π¦ = (πΉβπ) β (β*π€β¨π, π¦β© β π€ β β*π€β¨π, (πΉβπ)β© β π€)) |
92 | 91 | ralrn 7039 |
. . . . . . . 8
β’ (πΉ Fn π β (βπ¦ β ran πΉβ*π€β¨π, π¦β© β π€ β βπ β π β*π€β¨π, (πΉβπ)β© β π€)) |
93 | 11, 88, 92 | 3syl 18 |
. . . . . . 7
β’ (π β (βπ¦ β ran πΉβ*π€β¨π, π¦β© β π€ β βπ β π β*π€β¨π, (πΉβπ)β© β π€)) |
94 | 93 | ralbidv 3175 |
. . . . . 6
β’ (π β (βπ β πΎ βπ¦ β ran πΉβ*π€β¨π, π¦β© β π€ β βπ β πΎ βπ β π β*π€β¨π, (πΉβπ)β© β π€)) |
95 | 87, 94 | mpbird 257 |
. . . . 5
β’ (π β βπ β πΎ βπ¦ β ran πΉβ*π€β¨π, π¦β© β π€) |
96 | | breq1 5109 |
. . . . . . 7
β’ (π₯ = β¨π, π¦β© β (π₯ β π€ β β¨π, π¦β© β π€)) |
97 | 96 | mobidv 2548 |
. . . . . 6
β’ (π₯ = β¨π, π¦β© β (β*π€ π₯ β π€ β β*π€β¨π, π¦β© β π€)) |
98 | 97 | ralxp 5798 |
. . . . 5
β’
(βπ₯ β
(πΎ Γ ran πΉ)β*π€ π₯ β π€ β βπ β πΎ βπ¦ β ran πΉβ*π€β¨π, π¦β© β π€) |
99 | 95, 98 | sylibr 233 |
. . . 4
β’ (π β βπ₯ β (πΎ Γ ran πΉ)β*π€ π₯ β π€) |
100 | | ssralv 4011 |
. . . 4
β’ (dom
β
β (πΎ Γ ran
πΉ) β (βπ₯ β (πΎ Γ ran πΉ)β*π€ π₯ β π€ β βπ₯ β dom β β*π€ π₯ β π€)) |
101 | 45, 99, 100 | sylc 65 |
. . 3
β’ (π β βπ₯ β dom β β*π€ π₯ β π€) |
102 | | dffun7 6529 |
. . 3
β’ (Fun
β
β (Rel β β§ βπ₯ β dom β β*π€ π₯ β π€)) |
103 | 19, 101, 102 | sylanbrc 584 |
. 2
β’ (π β Fun β ) |
104 | | eqimss2 4002 |
. . . . . . . . . . . . . . 15
β’ ( β =
βͺ π β π (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))) β βͺ π β π (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))) β β ) |
105 | 17, 104 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β βͺ π β π (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))) β β ) |
106 | | iunss 5006 |
. . . . . . . . . . . . . 14
β’ (βͺ π β π (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))) β β β
βπ β π (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))) β β ) |
107 | 105, 106 | sylib 217 |
. . . . . . . . . . . . 13
β’ (π β βπ β π (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))) β β ) |
108 | 107 | r19.21bi 3235 |
. . . . . . . . . . . 12
β’ ((π β§ π β π) β (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))) β β ) |
109 | 108 | adantrl 715 |
. . . . . . . . . . 11
β’ ((π β§ (π β πΎ β§ π β π)) β (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))) β β ) |
110 | | dmss 5859 |
. . . . . . . . . . 11
β’ ((π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))) β β β dom (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))) β dom β ) |
111 | 109, 110 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ (π β πΎ β§ π β π)) β dom (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π))) β dom β ) |
112 | 58, 111 | eqsstrrid 3994 |
. . . . . . . . 9
β’ ((π β§ (π β πΎ β§ π β π)) β (πΎ Γ {(πΉβπ)}) β dom β ) |
113 | | simprl 770 |
. . . . . . . . . 10
β’ ((π β§ (π β πΎ β§ π β π)) β π β πΎ) |
114 | | fvex 6856 |
. . . . . . . . . . 11
β’ (πΉβπ) β V |
115 | 114 | snid 4623 |
. . . . . . . . . 10
β’ (πΉβπ) β {(πΉβπ)} |
116 | | opelxpi 5671 |
. . . . . . . . . 10
β’ ((π β πΎ β§ (πΉβπ) β {(πΉβπ)}) β β¨π, (πΉβπ)β© β (πΎ Γ {(πΉβπ)})) |
117 | 113, 115,
116 | sylancl 587 |
. . . . . . . . 9
β’ ((π β§ (π β πΎ β§ π β π)) β β¨π, (πΉβπ)β© β (πΎ Γ {(πΉβπ)})) |
118 | 112, 117 | sseldd 3946 |
. . . . . . . 8
β’ ((π β§ (π β πΎ β§ π β π)) β β¨π, (πΉβπ)β© β dom β ) |
119 | 118 | ralrimivva 3198 |
. . . . . . 7
β’ (π β βπ β πΎ βπ β π β¨π, (πΉβπ)β© β dom β ) |
120 | | opeq2 4832 |
. . . . . . . . . . 11
β’ (π¦ = (πΉβπ) β β¨π, π¦β© = β¨π, (πΉβπ)β©) |
121 | 120 | eleq1d 2823 |
. . . . . . . . . 10
β’ (π¦ = (πΉβπ) β (β¨π, π¦β© β dom β β β¨π, (πΉβπ)β© β dom β )) |
122 | 121 | ralrn 7039 |
. . . . . . . . 9
β’ (πΉ Fn π β (βπ¦ β ran πΉβ¨π, π¦β© β dom β β
βπ β π β¨π, (πΉβπ)β© β dom β )) |
123 | 11, 88, 122 | 3syl 18 |
. . . . . . . 8
β’ (π β (βπ¦ β ran πΉβ¨π, π¦β© β dom β β
βπ β π β¨π, (πΉβπ)β© β dom β )) |
124 | 123 | ralbidv 3175 |
. . . . . . 7
β’ (π β (βπ β πΎ βπ¦ β ran πΉβ¨π, π¦β© β dom β β
βπ β πΎ βπ β π β¨π, (πΉβπ)β© β dom β )) |
125 | 119, 124 | mpbird 257 |
. . . . . 6
β’ (π β βπ β πΎ βπ¦ β ran πΉβ¨π, π¦β© β dom β ) |
126 | | eleq1 2826 |
. . . . . . 7
β’ (π₯ = β¨π, π¦β© β (π₯ β dom β β β¨π, π¦β© β dom β )) |
127 | 126 | ralxp 5798 |
. . . . . 6
β’
(βπ₯ β
(πΎ Γ ran πΉ)π₯ β dom β β
βπ β πΎ βπ¦ β ran πΉβ¨π, π¦β© β dom β ) |
128 | 125, 127 | sylibr 233 |
. . . . 5
β’ (π β βπ₯ β (πΎ Γ ran πΉ)π₯ β dom β ) |
129 | | dfss3 3933 |
. . . . 5
β’ ((πΎ Γ ran πΉ) β dom β β
βπ₯ β (πΎ Γ ran πΉ)π₯ β dom β ) |
130 | 128, 129 | sylibr 233 |
. . . 4
β’ (π β (πΎ Γ ran πΉ) β dom β ) |
131 | 44, 130 | eqsstrrd 3984 |
. . 3
β’ (π β (πΎ Γ π΅) β dom β ) |
132 | 41, 131 | eqssd 3962 |
. 2
β’ (π β dom β = (πΎ Γ π΅)) |
133 | | df-fn 6500 |
. 2
β’ ( β Fn
(πΎ Γ π΅) β (Fun β β§ dom β =
(πΎ Γ π΅))) |
134 | 103, 132,
133 | sylanbrc 584 |
1
β’ (π β β Fn (πΎ Γ π΅)) |