Step | Hyp | Ref
| Expression |
1 | | eliun 4963 |
. . . . 5
β’ (π¦ β βͺ π β Ο (π΄ βm π) β βπ β Ο π¦ β (π΄ βm π)) |
2 | | elmapi 8794 |
. . . . . . . . . 10
β’ (π¦ β (π΄ βm π) β π¦:πβΆπ΄) |
3 | 2 | ad2antll 728 |
. . . . . . . . 9
β’ ((π β§ (π β Ο β§ π¦ β (π΄ βm π))) β π¦:πβΆπ΄) |
4 | 3 | fdmd 6684 |
. . . . . . . 8
β’ ((π β§ (π β Ο β§ π¦ β (π΄ βm π))) β dom π¦ = π) |
5 | | simprl 770 |
. . . . . . . 8
β’ ((π β§ (π β Ο β§ π¦ β (π΄ βm π))) β π β Ο) |
6 | 4, 5 | eqeltrd 2838 |
. . . . . . 7
β’ ((π β§ (π β Ο β§ π¦ β (π΄ βm π))) β dom π¦ β Ο) |
7 | 4 | fveq2d 6851 |
. . . . . . . . 9
β’ ((π β§ (π β Ο β§ π¦ β (π΄ βm π))) β (πΊβdom π¦) = (πΊβπ)) |
8 | 7 | fveq1d 6849 |
. . . . . . . 8
β’ ((π β§ (π β Ο β§ π¦ β (π΄ βm π))) β ((πΊβdom π¦)βπ¦) = ((πΊβπ)βπ¦)) |
9 | | fseqenlem.a |
. . . . . . . . . . . 12
β’ (π β π΄ β π) |
10 | | fseqenlem.b |
. . . . . . . . . . . 12
β’ (π β π΅ β π΄) |
11 | | fseqenlem.f |
. . . . . . . . . . . 12
β’ (π β πΉ:(π΄ Γ π΄)β1-1-ontoβπ΄) |
12 | | fseqenlem.g |
. . . . . . . . . . . 12
β’ πΊ = seqΟ((π β V, π β V β¦ (π₯ β (π΄ βm suc π) β¦ ((πβ(π₯ βΎ π))πΉ(π₯βπ)))), {β¨β
, π΅β©}) |
13 | 9, 10, 11, 12 | fseqenlem1 9967 |
. . . . . . . . . . 11
β’ ((π β§ π β Ο) β (πΊβπ):(π΄ βm π)β1-1βπ΄) |
14 | 13 | adantrr 716 |
. . . . . . . . . 10
β’ ((π β§ (π β Ο β§ π¦ β (π΄ βm π))) β (πΊβπ):(π΄ βm π)β1-1βπ΄) |
15 | | f1f 6743 |
. . . . . . . . . 10
β’ ((πΊβπ):(π΄ βm π)β1-1βπ΄ β (πΊβπ):(π΄ βm π)βΆπ΄) |
16 | 14, 15 | syl 17 |
. . . . . . . . 9
β’ ((π β§ (π β Ο β§ π¦ β (π΄ βm π))) β (πΊβπ):(π΄ βm π)βΆπ΄) |
17 | | simprr 772 |
. . . . . . . . 9
β’ ((π β§ (π β Ο β§ π¦ β (π΄ βm π))) β π¦ β (π΄ βm π)) |
18 | 16, 17 | ffvelcdmd 7041 |
. . . . . . . 8
β’ ((π β§ (π β Ο β§ π¦ β (π΄ βm π))) β ((πΊβπ)βπ¦) β π΄) |
19 | 8, 18 | eqeltrd 2838 |
. . . . . . 7
β’ ((π β§ (π β Ο β§ π¦ β (π΄ βm π))) β ((πΊβdom π¦)βπ¦) β π΄) |
20 | 6, 19 | opelxpd 5676 |
. . . . . 6
β’ ((π β§ (π β Ο β§ π¦ β (π΄ βm π))) β β¨dom π¦, ((πΊβdom π¦)βπ¦)β© β (Ο Γ π΄)) |
21 | 20 | rexlimdvaa 3154 |
. . . . 5
β’ (π β (βπ β Ο π¦ β (π΄ βm π) β β¨dom π¦, ((πΊβdom π¦)βπ¦)β© β (Ο Γ π΄))) |
22 | 1, 21 | biimtrid 241 |
. . . 4
β’ (π β (π¦ β βͺ
π β Ο (π΄ βm π) β β¨dom π¦, ((πΊβdom π¦)βπ¦)β© β (Ο Γ π΄))) |
23 | 22 | imp 408 |
. . 3
β’ ((π β§ π¦ β βͺ
π β Ο (π΄ βm π)) β β¨dom π¦, ((πΊβdom π¦)βπ¦)β© β (Ο Γ π΄)) |
24 | | fseqenlem.k |
. . 3
β’ πΎ = (π¦ β βͺ
π β Ο (π΄ βm π) β¦ β¨dom π¦, ((πΊβdom π¦)βπ¦)β©) |
25 | 23, 24 | fmptd 7067 |
. 2
β’ (π β πΎ:βͺ π β Ο (π΄ βm π)βΆ(Ο Γ π΄)) |
26 | | ffun 6676 |
. . . . . . . . . . . . . . 15
β’ (πΎ:βͺ π β Ο (π΄ βm π)βΆ(Ο Γ π΄) β Fun πΎ) |
27 | | funbrfv2b 6905 |
. . . . . . . . . . . . . . 15
β’ (Fun
πΎ β (π§πΎπ€ β (π§ β dom πΎ β§ (πΎβπ§) = π€))) |
28 | 25, 26, 27 | 3syl 18 |
. . . . . . . . . . . . . 14
β’ (π β (π§πΎπ€ β (π§ β dom πΎ β§ (πΎβπ§) = π€))) |
29 | 28 | simplbda 501 |
. . . . . . . . . . . . 13
β’ ((π β§ π§πΎπ€) β (πΎβπ§) = π€) |
30 | 28 | simprbda 500 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π§πΎπ€) β π§ β dom πΎ) |
31 | 25 | fdmd 6684 |
. . . . . . . . . . . . . . . 16
β’ (π β dom πΎ = βͺ π β Ο (π΄ βm π)) |
32 | 31 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π§πΎπ€) β dom πΎ = βͺ π β Ο (π΄ βm π)) |
33 | 30, 32 | eleqtrd 2840 |
. . . . . . . . . . . . . 14
β’ ((π β§ π§πΎπ€) β π§ β βͺ
π β Ο (π΄ βm π)) |
34 | | dmeq 5864 |
. . . . . . . . . . . . . . . 16
β’ (π¦ = π§ β dom π¦ = dom π§) |
35 | 34 | fveq2d 6851 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ = π§ β (πΊβdom π¦) = (πΊβdom π§)) |
36 | | id 22 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ = π§ β π¦ = π§) |
37 | 35, 36 | fveq12d 6854 |
. . . . . . . . . . . . . . . 16
β’ (π¦ = π§ β ((πΊβdom π¦)βπ¦) = ((πΊβdom π§)βπ§)) |
38 | 34, 37 | opeq12d 4843 |
. . . . . . . . . . . . . . 15
β’ (π¦ = π§ β β¨dom π¦, ((πΊβdom π¦)βπ¦)β© = β¨dom π§, ((πΊβdom π§)βπ§)β©) |
39 | | opex 5426 |
. . . . . . . . . . . . . . 15
β’ β¨dom
π§, ((πΊβdom π§)βπ§)β© β V |
40 | 38, 24, 39 | fvmpt 6953 |
. . . . . . . . . . . . . 14
β’ (π§ β βͺ π β Ο (π΄ βm π) β (πΎβπ§) = β¨dom π§, ((πΊβdom π§)βπ§)β©) |
41 | 33, 40 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β§ π§πΎπ€) β (πΎβπ§) = β¨dom π§, ((πΊβdom π§)βπ§)β©) |
42 | 29, 41 | eqtr3d 2779 |
. . . . . . . . . . . 12
β’ ((π β§ π§πΎπ€) β π€ = β¨dom π§, ((πΊβdom π§)βπ§)β©) |
43 | 42 | fveq2d 6851 |
. . . . . . . . . . 11
β’ ((π β§ π§πΎπ€) β (1st βπ€) = (1st
ββ¨dom π§, ((πΊβdom π§)βπ§)β©)) |
44 | | vex 3452 |
. . . . . . . . . . . . 13
β’ π§ β V |
45 | 44 | dmex 7853 |
. . . . . . . . . . . 12
β’ dom π§ β V |
46 | | fvex 6860 |
. . . . . . . . . . . 12
β’ ((πΊβdom π§)βπ§) β V |
47 | 45, 46 | op1st 7934 |
. . . . . . . . . . 11
β’
(1st ββ¨dom π§, ((πΊβdom π§)βπ§)β©) = dom π§ |
48 | 43, 47 | eqtrdi 2793 |
. . . . . . . . . 10
β’ ((π β§ π§πΎπ€) β (1st βπ€) = dom π§) |
49 | 48 | fveq2d 6851 |
. . . . . . . . 9
β’ ((π β§ π§πΎπ€) β (πΊβ(1st βπ€)) = (πΊβdom π§)) |
50 | 49 | cnveqd 5836 |
. . . . . . . 8
β’ ((π β§ π§πΎπ€) β β‘(πΊβ(1st βπ€)) = β‘(πΊβdom π§)) |
51 | 42 | fveq2d 6851 |
. . . . . . . . 9
β’ ((π β§ π§πΎπ€) β (2nd βπ€) = (2nd
ββ¨dom π§, ((πΊβdom π§)βπ§)β©)) |
52 | 45, 46 | op2nd 7935 |
. . . . . . . . 9
β’
(2nd ββ¨dom π§, ((πΊβdom π§)βπ§)β©) = ((πΊβdom π§)βπ§) |
53 | 51, 52 | eqtrdi 2793 |
. . . . . . . 8
β’ ((π β§ π§πΎπ€) β (2nd βπ€) = ((πΊβdom π§)βπ§)) |
54 | 50, 53 | fveq12d 6854 |
. . . . . . 7
β’ ((π β§ π§πΎπ€) β (β‘(πΊβ(1st βπ€))β(2nd
βπ€)) = (β‘(πΊβdom π§)β((πΊβdom π§)βπ§))) |
55 | | eliun 4963 |
. . . . . . . . . . . . 13
β’ (π§ β βͺ π β Ο (π΄ βm π) β βπ β Ο π§ β (π΄ βm π)) |
56 | | elmapi 8794 |
. . . . . . . . . . . . . . . . . 18
β’ (π§ β (π΄ βm π) β π§:πβΆπ΄) |
57 | 56 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ ((π β Ο β§ π§ β (π΄ βm π)) β π§:πβΆπ΄) |
58 | 57 | fdmd 6684 |
. . . . . . . . . . . . . . . 16
β’ ((π β Ο β§ π§ β (π΄ βm π)) β dom π§ = π) |
59 | | simpl 484 |
. . . . . . . . . . . . . . . 16
β’ ((π β Ο β§ π§ β (π΄ βm π)) β π β Ο) |
60 | 58, 59 | eqeltrd 2838 |
. . . . . . . . . . . . . . 15
β’ ((π β Ο β§ π§ β (π΄ βm π)) β dom π§ β Ο) |
61 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’ ((π β Ο β§ π§ β (π΄ βm π)) β π§ β (π΄ βm π)) |
62 | 58 | oveq2d 7378 |
. . . . . . . . . . . . . . . 16
β’ ((π β Ο β§ π§ β (π΄ βm π)) β (π΄ βm dom π§) = (π΄ βm π)) |
63 | 61, 62 | eleqtrrd 2841 |
. . . . . . . . . . . . . . 15
β’ ((π β Ο β§ π§ β (π΄ βm π)) β π§ β (π΄ βm dom π§)) |
64 | 60, 63 | jca 513 |
. . . . . . . . . . . . . 14
β’ ((π β Ο β§ π§ β (π΄ βm π)) β (dom π§ β Ο β§ π§ β (π΄ βm dom π§))) |
65 | 64 | rexlimiva 3145 |
. . . . . . . . . . . . 13
β’
(βπ β
Ο π§ β (π΄ βm π) β (dom π§ β Ο β§ π§ β (π΄ βm dom π§))) |
66 | 55, 65 | sylbi 216 |
. . . . . . . . . . . 12
β’ (π§ β βͺ π β Ο (π΄ βm π) β (dom π§ β Ο β§ π§ β (π΄ βm dom π§))) |
67 | 33, 66 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ π§πΎπ€) β (dom π§ β Ο β§ π§ β (π΄ βm dom π§))) |
68 | 67 | simpld 496 |
. . . . . . . . . 10
β’ ((π β§ π§πΎπ€) β dom π§ β Ο) |
69 | 9, 10, 11, 12 | fseqenlem1 9967 |
. . . . . . . . . 10
β’ ((π β§ dom π§ β Ο) β (πΊβdom π§):(π΄ βm dom π§)β1-1βπ΄) |
70 | 68, 69 | syldan 592 |
. . . . . . . . 9
β’ ((π β§ π§πΎπ€) β (πΊβdom π§):(π΄ βm dom π§)β1-1βπ΄) |
71 | | f1f1orn 6800 |
. . . . . . . . 9
β’ ((πΊβdom π§):(π΄ βm dom π§)β1-1βπ΄ β (πΊβdom π§):(π΄ βm dom π§)β1-1-ontoβran
(πΊβdom π§)) |
72 | 70, 71 | syl 17 |
. . . . . . . 8
β’ ((π β§ π§πΎπ€) β (πΊβdom π§):(π΄ βm dom π§)β1-1-ontoβran
(πΊβdom π§)) |
73 | 67 | simprd 497 |
. . . . . . . 8
β’ ((π β§ π§πΎπ€) β π§ β (π΄ βm dom π§)) |
74 | | f1ocnvfv1 7227 |
. . . . . . . 8
β’ (((πΊβdom π§):(π΄ βm dom π§)β1-1-ontoβran
(πΊβdom π§) β§ π§ β (π΄ βm dom π§)) β (β‘(πΊβdom π§)β((πΊβdom π§)βπ§)) = π§) |
75 | 72, 73, 74 | syl2anc 585 |
. . . . . . 7
β’ ((π β§ π§πΎπ€) β (β‘(πΊβdom π§)β((πΊβdom π§)βπ§)) = π§) |
76 | 54, 75 | eqtr2d 2778 |
. . . . . 6
β’ ((π β§ π§πΎπ€) β π§ = (β‘(πΊβ(1st βπ€))β(2nd
βπ€))) |
77 | 76 | ex 414 |
. . . . 5
β’ (π β (π§πΎπ€ β π§ = (β‘(πΊβ(1st βπ€))β(2nd
βπ€)))) |
78 | 77 | alrimiv 1931 |
. . . 4
β’ (π β βπ§(π§πΎπ€ β π§ = (β‘(πΊβ(1st βπ€))β(2nd
βπ€)))) |
79 | | mo2icl 3677 |
. . . 4
β’
(βπ§(π§πΎπ€ β π§ = (β‘(πΊβ(1st βπ€))β(2nd
βπ€))) β
β*π§ π§πΎπ€) |
80 | 78, 79 | syl 17 |
. . 3
β’ (π β β*π§ π§πΎπ€) |
81 | 80 | alrimiv 1931 |
. 2
β’ (π β βπ€β*π§ π§πΎπ€) |
82 | | dff12 6742 |
. 2
β’ (πΎ:βͺ π β Ο (π΄ βm π)β1-1β(Ο Γ π΄) β (πΎ:βͺ π β Ο (π΄ βm π)βΆ(Ο Γ π΄) β§ βπ€β*π§ π§πΎπ€)) |
83 | 25, 81, 82 | sylanbrc 584 |
1
β’ (π β πΎ:βͺ π β Ο (π΄ βm π)β1-1β(Ο Γ π΄)) |