Step | Hyp | Ref
| Expression |
1 | | pwfseqlem5.g |
. 2
β’ (π β πΊ:π« π΄β1-1ββͺ π β Ο (π΄ βm π)) |
2 | | pwfseqlem5.x |
. 2
β’ (π β π β π΄) |
3 | | pwfseqlem5.h |
. 2
β’ (π β π»:Οβ1-1-ontoβπ) |
4 | | pwfseqlem5.ps |
. 2
β’ (π β ((π‘ β π΄ β§ π β (π‘ Γ π‘) β§ π We π‘) β§ Ο βΌ π‘)) |
5 | | vex 3448 |
. . . . . . . . . . 11
β’ π‘ β V |
6 | | simprl3 1221 |
. . . . . . . . . . . 12
β’ ((π β§ ((π‘ β π΄ β§ π β (π‘ Γ π‘) β§ π We π‘) β§ Ο βΌ π‘)) β π We π‘) |
7 | 4, 6 | sylan2b 595 |
. . . . . . . . . . 11
β’ ((π β§ π) β π We π‘) |
8 | | pwfseqlem5.o |
. . . . . . . . . . . 12
β’ π = OrdIso(π, π‘) |
9 | 8 | oiiso 9478 |
. . . . . . . . . . 11
β’ ((π‘ β V β§ π We π‘) β π Isom E , π (dom π, π‘)) |
10 | 5, 7, 9 | sylancr 588 |
. . . . . . . . . 10
β’ ((π β§ π) β π Isom E , π (dom π, π‘)) |
11 | | isof1o 7269 |
. . . . . . . . . 10
β’ (π Isom E , π (dom π, π‘) β π:dom πβ1-1-ontoβπ‘) |
12 | 10, 11 | syl 17 |
. . . . . . . . 9
β’ ((π β§ π) β π:dom πβ1-1-ontoβπ‘) |
13 | | cardom 9927 |
. . . . . . . . . . . 12
β’
(cardβΟ) = Ο |
14 | | simprr 772 |
. . . . . . . . . . . . . . 15
β’ ((π β§ ((π‘ β π΄ β§ π β (π‘ Γ π‘) β§ π We π‘) β§ Ο βΌ π‘)) β Ο βΌ π‘) |
15 | 4, 14 | sylan2b 595 |
. . . . . . . . . . . . . 14
β’ ((π β§ π) β Ο βΌ π‘) |
16 | 8 | oien 9479 |
. . . . . . . . . . . . . . . 16
β’ ((π‘ β V β§ π We π‘) β dom π β π‘) |
17 | 5, 7, 16 | sylancr 588 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π) β dom π β π‘) |
18 | 17 | ensymd 8948 |
. . . . . . . . . . . . . 14
β’ ((π β§ π) β π‘ β dom π) |
19 | | domentr 8956 |
. . . . . . . . . . . . . 14
β’ ((Ο
βΌ π‘ β§ π‘ β dom π) β Ο βΌ dom π) |
20 | 15, 18, 19 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((π β§ π) β Ο βΌ dom π) |
21 | | omelon 9587 |
. . . . . . . . . . . . . . 15
β’ Ο
β On |
22 | | onenon 9890 |
. . . . . . . . . . . . . . 15
β’ (Ο
β On β Ο β dom card) |
23 | 21, 22 | ax-mp 5 |
. . . . . . . . . . . . . 14
β’ Ο
β dom card |
24 | 8 | oion 9477 |
. . . . . . . . . . . . . . . 16
β’ (π‘ β V β dom π β On) |
25 | 24 | elv 3450 |
. . . . . . . . . . . . . . 15
β’ dom π β On |
26 | | onenon 9890 |
. . . . . . . . . . . . . . 15
β’ (dom
π β On β dom
π β dom
card) |
27 | 25, 26 | mp1i 13 |
. . . . . . . . . . . . . 14
β’ ((π β§ π) β dom π β dom card) |
28 | | carddom2 9918 |
. . . . . . . . . . . . . 14
β’ ((Ο
β dom card β§ dom π
β dom card) β ((cardβΟ) β (cardβdom π) β Ο βΌ dom
π)) |
29 | 23, 27, 28 | sylancr 588 |
. . . . . . . . . . . . 13
β’ ((π β§ π) β ((cardβΟ) β
(cardβdom π) β
Ο βΌ dom π)) |
30 | 20, 29 | mpbird 257 |
. . . . . . . . . . . 12
β’ ((π β§ π) β (cardβΟ) β
(cardβdom π)) |
31 | 13, 30 | eqsstrrid 3994 |
. . . . . . . . . . 11
β’ ((π β§ π) β Ο β (cardβdom
π)) |
32 | | cardonle 9898 |
. . . . . . . . . . . 12
β’ (dom
π β On β
(cardβdom π) β
dom π) |
33 | 25, 32 | mp1i 13 |
. . . . . . . . . . 11
β’ ((π β§ π) β (cardβdom π) β dom π) |
34 | 31, 33 | sstrd 3955 |
. . . . . . . . . 10
β’ ((π β§ π) β Ο β dom π) |
35 | | sseq2 3971 |
. . . . . . . . . . . 12
β’ (π = dom π β (Ο β π β Ο β dom π)) |
36 | | fveq2 6843 |
. . . . . . . . . . . . . 14
β’ (π = dom π β (πβπ) = (πβdom π)) |
37 | 36 | f1oeq1d 6780 |
. . . . . . . . . . . . 13
β’ (π = dom π β ((πβπ):(π Γ π)β1-1-ontoβπ β (πβdom π):(π Γ π)β1-1-ontoβπ)) |
38 | | xpeq12 5659 |
. . . . . . . . . . . . . . 15
β’ ((π = dom π β§ π = dom π) β (π Γ π) = (dom π Γ dom π)) |
39 | 38 | anidms 568 |
. . . . . . . . . . . . . 14
β’ (π = dom π β (π Γ π) = (dom π Γ dom π)) |
40 | 39 | f1oeq2d 6781 |
. . . . . . . . . . . . 13
β’ (π = dom π β ((πβdom π):(π Γ π)β1-1-ontoβπ β (πβdom π):(dom π Γ dom π)β1-1-ontoβπ)) |
41 | | f1oeq3 6775 |
. . . . . . . . . . . . 13
β’ (π = dom π β ((πβdom π):(dom π Γ dom π)β1-1-ontoβπ β (πβdom π):(dom π Γ dom π)β1-1-ontoβdom
π)) |
42 | 37, 40, 41 | 3bitrd 305 |
. . . . . . . . . . . 12
β’ (π = dom π β ((πβπ):(π Γ π)β1-1-ontoβπ β (πβdom π):(dom π Γ dom π)β1-1-ontoβdom
π)) |
43 | 35, 42 | imbi12d 345 |
. . . . . . . . . . 11
β’ (π = dom π β ((Ο β π β (πβπ):(π Γ π)β1-1-ontoβπ) β (Ο β dom
π β (πβdom π):(dom π Γ dom π)β1-1-ontoβdom
π))) |
44 | | pwfseqlem5.n |
. . . . . . . . . . . 12
β’ (π β βπ β (harβπ« π΄)(Ο β π β (πβπ):(π Γ π)β1-1-ontoβπ)) |
45 | 44 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π) β βπ β (harβπ« π΄)(Ο β π β (πβπ):(π Γ π)β1-1-ontoβπ)) |
46 | 25 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π β§ π) β dom π β On) |
47 | 1 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π) β πΊ:π« π΄β1-1ββͺ π β Ο (π΄ βm π)) |
48 | | omex 9584 |
. . . . . . . . . . . . . . . . . 18
β’ Ο
β V |
49 | | ovex 7391 |
. . . . . . . . . . . . . . . . . 18
β’ (π΄ βm π) β V |
50 | 48, 49 | iunex 7902 |
. . . . . . . . . . . . . . . . 17
β’ βͺ π β Ο (π΄ βm π) β V |
51 | | f1dmex 7890 |
. . . . . . . . . . . . . . . . 17
β’ ((πΊ:π« π΄β1-1ββͺ π β Ο (π΄ βm π) β§ βͺ π β Ο (π΄ βm π) β V) β π« π΄ β V) |
52 | 47, 50, 51 | sylancl 587 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π) β π« π΄ β V) |
53 | | pwexb 7701 |
. . . . . . . . . . . . . . . 16
β’ (π΄ β V β π« π΄ β V) |
54 | 52, 53 | sylibr 233 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π) β π΄ β V) |
55 | | simprl1 1219 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ ((π‘ β π΄ β§ π β (π‘ Γ π‘) β§ π We π‘) β§ Ο βΌ π‘)) β π‘ β π΄) |
56 | 4, 55 | sylan2b 595 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π) β π‘ β π΄) |
57 | | ssdomg 8943 |
. . . . . . . . . . . . . . 15
β’ (π΄ β V β (π‘ β π΄ β π‘ βΌ π΄)) |
58 | 54, 56, 57 | sylc 65 |
. . . . . . . . . . . . . 14
β’ ((π β§ π) β π‘ βΌ π΄) |
59 | | canth2g 9078 |
. . . . . . . . . . . . . . 15
β’ (π΄ β V β π΄ βΊ π« π΄) |
60 | | sdomdom 8923 |
. . . . . . . . . . . . . . 15
β’ (π΄ βΊ π« π΄ β π΄ βΌ π« π΄) |
61 | 54, 59, 60 | 3syl 18 |
. . . . . . . . . . . . . 14
β’ ((π β§ π) β π΄ βΌ π« π΄) |
62 | | domtr 8950 |
. . . . . . . . . . . . . 14
β’ ((π‘ βΌ π΄ β§ π΄ βΌ π« π΄) β π‘ βΌ π« π΄) |
63 | 58, 61, 62 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((π β§ π) β π‘ βΌ π« π΄) |
64 | | endomtr 8955 |
. . . . . . . . . . . . 13
β’ ((dom
π β π‘ β§ π‘ βΌ π« π΄) β dom π βΌ π« π΄) |
65 | 17, 63, 64 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((π β§ π) β dom π βΌ π« π΄) |
66 | | elharval 9502 |
. . . . . . . . . . . 12
β’ (dom
π β
(harβπ« π΄)
β (dom π β On
β§ dom π βΌ
π« π΄)) |
67 | 46, 65, 66 | sylanbrc 584 |
. . . . . . . . . . 11
β’ ((π β§ π) β dom π β (harβπ« π΄)) |
68 | 43, 45, 67 | rspcdva 3581 |
. . . . . . . . . 10
β’ ((π β§ π) β (Ο β dom π β (πβdom π):(dom π Γ dom π)β1-1-ontoβdom
π)) |
69 | 34, 68 | mpd 15 |
. . . . . . . . 9
β’ ((π β§ π) β (πβdom π):(dom π Γ dom π)β1-1-ontoβdom
π) |
70 | | f1oco 6808 |
. . . . . . . . 9
β’ ((π:dom πβ1-1-ontoβπ‘ β§ (πβdom π):(dom π Γ dom π)β1-1-ontoβdom
π) β (π β (πβdom π)):(dom π Γ dom π)β1-1-ontoβπ‘) |
71 | 12, 69, 70 | syl2anc 585 |
. . . . . . . 8
β’ ((π β§ π) β (π β (πβdom π)):(dom π Γ dom π)β1-1-ontoβπ‘) |
72 | | f1of 6785 |
. . . . . . . . . . . . . . 15
β’ (π:dom πβ1-1-ontoβπ‘ β π:dom πβΆπ‘) |
73 | 12, 72 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β§ π) β π:dom πβΆπ‘) |
74 | 73 | feqmptd 6911 |
. . . . . . . . . . . . 13
β’ ((π β§ π) β π = (π’ β dom π β¦ (πβπ’))) |
75 | 74 | f1oeq1d 6780 |
. . . . . . . . . . . 12
β’ ((π β§ π) β (π:dom πβ1-1-ontoβπ‘ β (π’ β dom π β¦ (πβπ’)):dom πβ1-1-ontoβπ‘)) |
76 | 12, 75 | mpbid 231 |
. . . . . . . . . . 11
β’ ((π β§ π) β (π’ β dom π β¦ (πβπ’)):dom πβ1-1-ontoβπ‘) |
77 | 73 | feqmptd 6911 |
. . . . . . . . . . . . 13
β’ ((π β§ π) β π = (π£ β dom π β¦ (πβπ£))) |
78 | 77 | f1oeq1d 6780 |
. . . . . . . . . . . 12
β’ ((π β§ π) β (π:dom πβ1-1-ontoβπ‘ β (π£ β dom π β¦ (πβπ£)):dom πβ1-1-ontoβπ‘)) |
79 | 12, 78 | mpbid 231 |
. . . . . . . . . . 11
β’ ((π β§ π) β (π£ β dom π β¦ (πβπ£)):dom πβ1-1-ontoβπ‘) |
80 | 76, 79 | xpf1o 9086 |
. . . . . . . . . 10
β’ ((π β§ π) β (π’ β dom π, π£ β dom π β¦ β¨(πβπ’), (πβπ£)β©):(dom π Γ dom π)β1-1-ontoβ(π‘ Γ π‘)) |
81 | | pwfseqlem5.t |
. . . . . . . . . . 11
β’ π = (π’ β dom π, π£ β dom π β¦ β¨(πβπ’), (πβπ£)β©) |
82 | | f1oeq1 6773 |
. . . . . . . . . . 11
β’ (π = (π’ β dom π, π£ β dom π β¦ β¨(πβπ’), (πβπ£)β©) β (π:(dom π Γ dom π)β1-1-ontoβ(π‘ Γ π‘) β (π’ β dom π, π£ β dom π β¦ β¨(πβπ’), (πβπ£)β©):(dom π Γ dom π)β1-1-ontoβ(π‘ Γ π‘))) |
83 | 81, 82 | ax-mp 5 |
. . . . . . . . . 10
β’ (π:(dom π Γ dom π)β1-1-ontoβ(π‘ Γ π‘) β (π’ β dom π, π£ β dom π β¦ β¨(πβπ’), (πβπ£)β©):(dom π Γ dom π)β1-1-ontoβ(π‘ Γ π‘)) |
84 | 80, 83 | sylibr 233 |
. . . . . . . . 9
β’ ((π β§ π) β π:(dom π Γ dom π)β1-1-ontoβ(π‘ Γ π‘)) |
85 | | f1ocnv 6797 |
. . . . . . . . 9
β’ (π:(dom π Γ dom π)β1-1-ontoβ(π‘ Γ π‘) β β‘π:(π‘ Γ π‘)β1-1-ontoβ(dom
π Γ dom π)) |
86 | 84, 85 | syl 17 |
. . . . . . . 8
β’ ((π β§ π) β β‘π:(π‘ Γ π‘)β1-1-ontoβ(dom
π Γ dom π)) |
87 | | f1oco 6808 |
. . . . . . . 8
β’ (((π β (πβdom π)):(dom π Γ dom π)β1-1-ontoβπ‘ β§ β‘π:(π‘ Γ π‘)β1-1-ontoβ(dom
π Γ dom π)) β ((π β (πβdom π)) β β‘π):(π‘ Γ π‘)β1-1-ontoβπ‘) |
88 | 71, 86, 87 | syl2anc 585 |
. . . . . . 7
β’ ((π β§ π) β ((π β (πβdom π)) β β‘π):(π‘ Γ π‘)β1-1-ontoβπ‘) |
89 | | pwfseqlem5.p |
. . . . . . . 8
β’ π = ((π β (πβdom π)) β β‘π) |
90 | | f1oeq1 6773 |
. . . . . . . 8
β’ (π = ((π β (πβdom π)) β β‘π) β (π:(π‘ Γ π‘)β1-1-ontoβπ‘ β ((π β (πβdom π)) β β‘π):(π‘ Γ π‘)β1-1-ontoβπ‘)) |
91 | 89, 90 | ax-mp 5 |
. . . . . . 7
β’ (π:(π‘ Γ π‘)β1-1-ontoβπ‘ β ((π β (πβdom π)) β β‘π):(π‘ Γ π‘)β1-1-ontoβπ‘) |
92 | 88, 91 | sylibr 233 |
. . . . . 6
β’ ((π β§ π) β π:(π‘ Γ π‘)β1-1-ontoβπ‘) |
93 | | f1of1 6784 |
. . . . . 6
β’ (π:(π‘ Γ π‘)β1-1-ontoβπ‘ β π:(π‘ Γ π‘)β1-1βπ‘) |
94 | 92, 93 | syl 17 |
. . . . 5
β’ ((π β§ π) β π:(π‘ Γ π‘)β1-1βπ‘) |
95 | | f1of1 6784 |
. . . . . . . . . . . . 13
β’ (π:dom πβ1-1-ontoβπ‘ β π:dom πβ1-1βπ‘) |
96 | 12, 95 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β§ π) β π:dom πβ1-1βπ‘) |
97 | | f1ssres 6747 |
. . . . . . . . . . . 12
β’ ((π:dom πβ1-1βπ‘ β§ Ο β dom π) β (π βΎ Ο):Οβ1-1βπ‘) |
98 | 96, 34, 97 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((π β§ π) β (π βΎ Ο):Οβ1-1βπ‘) |
99 | | f1f1orn 6796 |
. . . . . . . . . . 11
β’ ((π βΎ
Ο):Οβ1-1βπ‘ β (π βΎ Ο):Οβ1-1-ontoβran (π βΎ Ο)) |
100 | 98, 99 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ π) β (π βΎ Ο):Οβ1-1-ontoβran (π βΎ Ο)) |
101 | 73, 34 | feqresmpt 6912 |
. . . . . . . . . . 11
β’ ((π β§ π) β (π βΎ Ο) = (π₯ β Ο β¦ (πβπ₯))) |
102 | 101 | f1oeq1d 6780 |
. . . . . . . . . 10
β’ ((π β§ π) β ((π βΎ Ο):Οβ1-1-ontoβran (π βΎ Ο) β (π₯ β Ο β¦ (πβπ₯)):Οβ1-1-ontoβran
(π βΎ
Ο))) |
103 | 100, 102 | mpbid 231 |
. . . . . . . . 9
β’ ((π β§ π) β (π₯ β Ο β¦ (πβπ₯)):Οβ1-1-ontoβran
(π βΎ
Ο)) |
104 | | mptresid 6005 |
. . . . . . . . . . 11
β’ ( I
βΎ π‘) = (π¦ β π‘ β¦ π¦) |
105 | 104 | eqcomi 2742 |
. . . . . . . . . 10
β’ (π¦ β π‘ β¦ π¦) = ( I βΎ π‘) |
106 | | f1oi 6823 |
. . . . . . . . . . 11
β’ ( I
βΎ π‘):π‘β1-1-ontoβπ‘ |
107 | | f1oeq1 6773 |
. . . . . . . . . . 11
β’ ((π¦ β π‘ β¦ π¦) = ( I βΎ π‘) β ((π¦ β π‘ β¦ π¦):π‘β1-1-ontoβπ‘ β ( I βΎ π‘):π‘β1-1-ontoβπ‘)) |
108 | 106, 107 | mpbiri 258 |
. . . . . . . . . 10
β’ ((π¦ β π‘ β¦ π¦) = ( I βΎ π‘) β (π¦ β π‘ β¦ π¦):π‘β1-1-ontoβπ‘) |
109 | 105, 108 | mp1i 13 |
. . . . . . . . 9
β’ ((π β§ π) β (π¦ β π‘ β¦ π¦):π‘β1-1-ontoβπ‘) |
110 | 103, 109 | xpf1o 9086 |
. . . . . . . 8
β’ ((π β§ π) β (π₯ β Ο, π¦ β π‘ β¦ β¨(πβπ₯), π¦β©):(Ο Γ π‘)β1-1-ontoβ(ran
(π βΎ Ο) Γ
π‘)) |
111 | | pwfseqlem5.i |
. . . . . . . . 9
β’ πΌ = (π₯ β Ο, π¦ β π‘ β¦ β¨(πβπ₯), π¦β©) |
112 | | f1oeq1 6773 |
. . . . . . . . 9
β’ (πΌ = (π₯ β Ο, π¦ β π‘ β¦ β¨(πβπ₯), π¦β©) β (πΌ:(Ο Γ π‘)β1-1-ontoβ(ran
(π βΎ Ο) Γ
π‘) β (π₯ β Ο, π¦ β π‘ β¦ β¨(πβπ₯), π¦β©):(Ο Γ π‘)β1-1-ontoβ(ran
(π βΎ Ο) Γ
π‘))) |
113 | 111, 112 | ax-mp 5 |
. . . . . . . 8
β’ (πΌ:(Ο Γ π‘)β1-1-ontoβ(ran
(π βΎ Ο) Γ
π‘) β (π₯ β Ο, π¦ β π‘ β¦ β¨(πβπ₯), π¦β©):(Ο Γ π‘)β1-1-ontoβ(ran
(π βΎ Ο) Γ
π‘)) |
114 | 110, 113 | sylibr 233 |
. . . . . . 7
β’ ((π β§ π) β πΌ:(Ο Γ π‘)β1-1-ontoβ(ran
(π βΎ Ο) Γ
π‘)) |
115 | | f1of1 6784 |
. . . . . . 7
β’ (πΌ:(Ο Γ π‘)β1-1-ontoβ(ran
(π βΎ Ο) Γ
π‘) β πΌ:(Ο Γ π‘)β1-1β(ran (π βΎ Ο) Γ π‘)) |
116 | 114, 115 | syl 17 |
. . . . . 6
β’ ((π β§ π) β πΌ:(Ο Γ π‘)β1-1β(ran (π βΎ Ο) Γ π‘)) |
117 | | f1f 6739 |
. . . . . . 7
β’ ((π βΎ
Ο):Οβ1-1βπ‘ β (π βΎ Ο):ΟβΆπ‘) |
118 | | frn 6676 |
. . . . . . 7
β’ ((π βΎ
Ο):ΟβΆπ‘
β ran (π βΎ
Ο) β π‘) |
119 | | xpss1 5653 |
. . . . . . 7
β’ (ran
(π βΎ Ο) β
π‘ β (ran (π βΎ Ο) Γ π‘) β (π‘ Γ π‘)) |
120 | 98, 117, 118, 119 | 4syl 19 |
. . . . . 6
β’ ((π β§ π) β (ran (π βΎ Ο) Γ π‘) β (π‘ Γ π‘)) |
121 | | f1ss 6745 |
. . . . . 6
β’ ((πΌ:(Ο Γ π‘)β1-1β(ran (π βΎ Ο) Γ π‘) β§ (ran (π βΎ Ο) Γ π‘) β (π‘ Γ π‘)) β πΌ:(Ο Γ π‘)β1-1β(π‘ Γ π‘)) |
122 | 116, 120,
121 | syl2anc 585 |
. . . . 5
β’ ((π β§ π) β πΌ:(Ο Γ π‘)β1-1β(π‘ Γ π‘)) |
123 | | f1co 6751 |
. . . . 5
β’ ((π:(π‘ Γ π‘)β1-1βπ‘ β§ πΌ:(Ο Γ π‘)β1-1β(π‘ Γ π‘)) β (π β πΌ):(Ο Γ π‘)β1-1βπ‘) |
124 | 94, 122, 123 | syl2anc 585 |
. . . 4
β’ ((π β§ π) β (π β πΌ):(Ο Γ π‘)β1-1βπ‘) |
125 | 5 | a1i 11 |
. . . . 5
β’ ((π β§ π) β π‘ β V) |
126 | | peano1 7826 |
. . . . . . . 8
β’ β
β Ο |
127 | 126 | a1i 11 |
. . . . . . 7
β’ ((π β§ π) β β
β
Ο) |
128 | 34, 127 | sseldd 3946 |
. . . . . 6
β’ ((π β§ π) β β
β dom π) |
129 | 73, 128 | ffvelcdmd 7037 |
. . . . 5
β’ ((π β§ π) β (πββ
) β π‘) |
130 | | pwfseqlem5.s |
. . . . 5
β’ π = seqΟ((π β V, π β V β¦ (π₯ β (π‘ βm suc π) β¦ ((πβ(π₯ βΎ π))π(π₯βπ)))), {β¨β
, (πββ
)β©}) |
131 | | pwfseqlem5.q |
. . . . 5
β’ π = (π¦ β βͺ
π β Ο (π‘ βm π) β¦ β¨dom π¦, ((πβdom π¦)βπ¦)β©) |
132 | 125, 129,
92, 130, 131 | fseqenlem2 9966 |
. . . 4
β’ ((π β§ π) β π:βͺ π β Ο (π‘ βm π)β1-1β(Ο Γ π‘)) |
133 | | f1co 6751 |
. . . 4
β’ (((π β πΌ):(Ο Γ π‘)β1-1βπ‘ β§ π:βͺ π β Ο (π‘ βm π)β1-1β(Ο Γ π‘)) β ((π β πΌ) β π):βͺ π β Ο (π‘ βm π)β1-1βπ‘) |
134 | 124, 132,
133 | syl2anc 585 |
. . 3
β’ ((π β§ π) β ((π β πΌ) β π):βͺ π β Ο (π‘ βm π)β1-1βπ‘) |
135 | | pwfseqlem5.k |
. . . 4
β’ πΎ = ((π β πΌ) β π) |
136 | | f1eq1 6734 |
. . . 4
β’ (πΎ = ((π β πΌ) β π) β (πΎ:βͺ π β Ο (π‘ βm π)β1-1βπ‘ β ((π β πΌ) β π):βͺ π β Ο (π‘ βm π)β1-1βπ‘)) |
137 | 135, 136 | ax-mp 5 |
. . 3
β’ (πΎ:βͺ π β Ο (π‘ βm π)β1-1βπ‘ β ((π β πΌ) β π):βͺ π β Ο (π‘ βm π)β1-1βπ‘) |
138 | 134, 137 | sylibr 233 |
. 2
β’ ((π β§ π) β πΎ:βͺ π β Ο (π‘ βm π)β1-1βπ‘) |
139 | | eqid 2733 |
. 2
β’ (πΊβ{π β π‘ β£ ((β‘πΎβπ) β ran πΊ β§ Β¬ π β (β‘πΊβ(β‘πΎβπ)))}) = (πΊβ{π β π‘ β£ ((β‘πΎβπ) β ran πΊ β§ Β¬ π β (β‘πΊβ(β‘πΎβπ)))}) |
140 | | eqid 2733 |
. 2
β’ (π‘ β V, π β V β¦ if(π‘ β Fin, (π»β(cardβπ‘)), ((πΊβ{π β π‘ β£ ((β‘πΎβπ) β ran πΊ β§ Β¬ π β (β‘πΊβ(β‘πΎβπ)))})ββ©
{π§ β Ο β£
Β¬ ((πΊβ{π β π‘ β£ ((β‘πΎβπ) β ran πΊ β§ Β¬ π β (β‘πΊβ(β‘πΎβπ)))})βπ§) β π‘}))) = (π‘ β V, π β V β¦ if(π‘ β Fin, (π»β(cardβπ‘)), ((πΊβ{π β π‘ β£ ((β‘πΎβπ) β ran πΊ β§ Β¬ π β (β‘πΊβ(β‘πΎβπ)))})ββ©
{π§ β Ο β£
Β¬ ((πΊβ{π β π‘ β£ ((β‘πΎβπ) β ran πΊ β§ Β¬ π β (β‘πΊβ(β‘πΎβπ)))})βπ§) β π‘}))) |
141 | | eqid 2733 |
. . 3
β’
{β¨π, πβ© β£ ((π β π΄ β§ π β (π Γ π)) β§ (π We π β§ βπ β π [(β‘π β {π}) / π](π(π‘ β V, π β V β¦ if(π‘ β Fin, (π»β(cardβπ‘)), ((πΊβ{π β π‘ β£ ((β‘πΎβπ) β ran πΊ β§ Β¬ π β (β‘πΊβ(β‘πΎβπ)))})ββ©
{π§ β Ο β£
Β¬ ((πΊβ{π β π‘ β£ ((β‘πΎβπ) β ran πΊ β§ Β¬ π β (β‘πΊβ(β‘πΎβπ)))})βπ§) β π‘})))(π β© (π Γ π))) = π))} = {β¨π, πβ© β£ ((π β π΄ β§ π β (π Γ π)) β§ (π We π β§ βπ β π [(β‘π β {π}) / π](π(π‘ β V, π β V β¦ if(π‘ β Fin, (π»β(cardβπ‘)), ((πΊβ{π β π‘ β£ ((β‘πΎβπ) β ran πΊ β§ Β¬ π β (β‘πΊβ(β‘πΎβπ)))})ββ©
{π§ β Ο β£
Β¬ ((πΊβ{π β π‘ β£ ((β‘πΎβπ) β ran πΊ β§ Β¬ π β (β‘πΊβ(β‘πΎβπ)))})βπ§) β π‘})))(π β© (π Γ π))) = π))} |
142 | 141 | fpwwe2cbv 10571 |
. 2
β’
{β¨π, πβ© β£ ((π β π΄ β§ π β (π Γ π)) β§ (π We π β§ βπ β π [(β‘π β {π}) / π](π(π‘ β V, π β V β¦ if(π‘ β Fin, (π»β(cardβπ‘)), ((πΊβ{π β π‘ β£ ((β‘πΎβπ) β ran πΊ β§ Β¬ π β (β‘πΊβ(β‘πΎβπ)))})ββ©
{π§ β Ο β£
Β¬ ((πΊβ{π β π‘ β£ ((β‘πΎβπ) β ran πΊ β§ Β¬ π β (β‘πΊβ(β‘πΎβπ)))})βπ§) β π‘})))(π β© (π Γ π))) = π))} = {β¨π, π β© β£ ((π β π΄ β§ π β (π Γ π)) β§ (π We π β§ βπ β π [(β‘π β {π}) / π€](π€(π‘ β V, π β V β¦ if(π‘ β Fin, (π»β(cardβπ‘)), ((πΊβ{π β π‘ β£ ((β‘πΎβπ) β ran πΊ β§ Β¬ π β (β‘πΊβ(β‘πΎβπ)))})ββ©
{π§ β Ο β£
Β¬ ((πΊβ{π β π‘ β£ ((β‘πΎβπ) β ran πΊ β§ Β¬ π β (β‘πΊβ(β‘πΎβπ)))})βπ§) β π‘})))(π β© (π€ Γ π€))) = π))} |
143 | | eqid 2733 |
. 2
β’ βͺ dom {β¨π, πβ© β£ ((π β π΄ β§ π β (π Γ π)) β§ (π We π β§ βπ β π [(β‘π β {π}) / π](π(π‘ β V, π β V β¦ if(π‘ β Fin, (π»β(cardβπ‘)), ((πΊβ{π β π‘ β£ ((β‘πΎβπ) β ran πΊ β§ Β¬ π β (β‘πΊβ(β‘πΎβπ)))})ββ©
{π§ β Ο β£
Β¬ ((πΊβ{π β π‘ β£ ((β‘πΎβπ) β ran πΊ β§ Β¬ π β (β‘πΊβ(β‘πΎβπ)))})βπ§) β π‘})))(π β© (π Γ π))) = π))} = βͺ dom
{β¨π, πβ© β£ ((π β π΄ β§ π β (π Γ π)) β§ (π We π β§ βπ β π [(β‘π β {π}) / π](π(π‘ β V, π β V β¦ if(π‘ β Fin, (π»β(cardβπ‘)), ((πΊβ{π β π‘ β£ ((β‘πΎβπ) β ran πΊ β§ Β¬ π β (β‘πΊβ(β‘πΎβπ)))})ββ©
{π§ β Ο β£
Β¬ ((πΊβ{π β π‘ β£ ((β‘πΎβπ) β ran πΊ β§ Β¬ π β (β‘πΊβ(β‘πΎβπ)))})βπ§) β π‘})))(π β© (π Γ π))) = π))} |
144 | 1, 2, 3, 4, 138, 139, 140, 142, 143 | pwfseqlem4 10603 |
1
β’ Β¬
π |