Step | Hyp | Ref
| Expression |
1 | | simprr 772 |
. . . . . . 7
β’ ((π β§ (π’ β π« π½ β§ (ran πΉ βͺ {π΄}) β βͺ
π’)) β (ran πΉ βͺ {π΄}) β βͺ
π’) |
2 | | ssun2 4134 |
. . . . . . . . 9
β’ {π΄} β (ran πΉ βͺ {π΄}) |
3 | | 1stckgen.1 |
. . . . . . . . . . 11
β’ (π β π½ β (TopOnβπ)) |
4 | | 1stckgen.3 |
. . . . . . . . . . 11
β’ (π β πΉ(βπ‘βπ½)π΄) |
5 | | lmcl 22664 |
. . . . . . . . . . 11
β’ ((π½ β (TopOnβπ) β§ πΉ(βπ‘βπ½)π΄) β π΄ β π) |
6 | 3, 4, 5 | syl2anc 585 |
. . . . . . . . . 10
β’ (π β π΄ β π) |
7 | | snssg 4745 |
. . . . . . . . . 10
β’ (π΄ β π β (π΄ β (ran πΉ βͺ {π΄}) β {π΄} β (ran πΉ βͺ {π΄}))) |
8 | 6, 7 | syl 17 |
. . . . . . . . 9
β’ (π β (π΄ β (ran πΉ βͺ {π΄}) β {π΄} β (ran πΉ βͺ {π΄}))) |
9 | 2, 8 | mpbiri 258 |
. . . . . . . 8
β’ (π β π΄ β (ran πΉ βͺ {π΄})) |
10 | 9 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π’ β π« π½ β§ (ran πΉ βͺ {π΄}) β βͺ
π’)) β π΄ β (ran πΉ βͺ {π΄})) |
11 | 1, 10 | sseldd 3946 |
. . . . . 6
β’ ((π β§ (π’ β π« π½ β§ (ran πΉ βͺ {π΄}) β βͺ
π’)) β π΄ β βͺ π’) |
12 | | eluni2 4870 |
. . . . . 6
β’ (π΄ β βͺ π’
β βπ€ β
π’ π΄ β π€) |
13 | 11, 12 | sylib 217 |
. . . . 5
β’ ((π β§ (π’ β π« π½ β§ (ran πΉ βͺ {π΄}) β βͺ
π’)) β βπ€ β π’ π΄ β π€) |
14 | | nnuz 12811 |
. . . . . . 7
β’ β =
(β€β₯β1) |
15 | | simprr 772 |
. . . . . . 7
β’ (((π β§ (π’ β π« π½ β§ (ran πΉ βͺ {π΄}) β βͺ
π’)) β§ (π€ β π’ β§ π΄ β π€)) β π΄ β π€) |
16 | | 1zzd 12539 |
. . . . . . 7
β’ (((π β§ (π’ β π« π½ β§ (ran πΉ βͺ {π΄}) β βͺ
π’)) β§ (π€ β π’ β§ π΄ β π€)) β 1 β β€) |
17 | 4 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ (π’ β π« π½ β§ (ran πΉ βͺ {π΄}) β βͺ
π’)) β§ (π€ β π’ β§ π΄ β π€)) β πΉ(βπ‘βπ½)π΄) |
18 | | simplrl 776 |
. . . . . . . . 9
β’ (((π β§ (π’ β π« π½ β§ (ran πΉ βͺ {π΄}) β βͺ
π’)) β§ (π€ β π’ β§ π΄ β π€)) β π’ β π« π½) |
19 | 18 | elpwid 4570 |
. . . . . . . 8
β’ (((π β§ (π’ β π« π½ β§ (ran πΉ βͺ {π΄}) β βͺ
π’)) β§ (π€ β π’ β§ π΄ β π€)) β π’ β π½) |
20 | | simprl 770 |
. . . . . . . 8
β’ (((π β§ (π’ β π« π½ β§ (ran πΉ βͺ {π΄}) β βͺ
π’)) β§ (π€ β π’ β§ π΄ β π€)) β π€ β π’) |
21 | 19, 20 | sseldd 3946 |
. . . . . . 7
β’ (((π β§ (π’ β π« π½ β§ (ran πΉ βͺ {π΄}) β βͺ
π’)) β§ (π€ β π’ β§ π΄ β π€)) β π€ β π½) |
22 | 14, 15, 16, 17, 21 | lmcvg 22629 |
. . . . . 6
β’ (((π β§ (π’ β π« π½ β§ (ran πΉ βͺ {π΄}) β βͺ
π’)) β§ (π€ β π’ β§ π΄ β π€)) β βπ β β βπ β (β€β₯βπ)(πΉβπ) β π€) |
23 | | imassrn 6025 |
. . . . . . . . . . . . 13
β’ (πΉ β (1...π)) β ran πΉ |
24 | | ssun1 4133 |
. . . . . . . . . . . . 13
β’ ran πΉ β (ran πΉ βͺ {π΄}) |
25 | 23, 24 | sstri 3954 |
. . . . . . . . . . . 12
β’ (πΉ β (1...π)) β (ran πΉ βͺ {π΄}) |
26 | | id 22 |
. . . . . . . . . . . 12
β’ ((ran
πΉ βͺ {π΄}) β βͺ
π’ β (ran πΉ βͺ {π΄}) β βͺ
π’) |
27 | 25, 26 | sstrid 3956 |
. . . . . . . . . . 11
β’ ((ran
πΉ βͺ {π΄}) β βͺ
π’ β (πΉ β (1...π)) β βͺ π’) |
28 | | 1stckgen.2 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β πΉ:ββΆπ) |
29 | 28 | frnd 6677 |
. . . . . . . . . . . . . . . . . 18
β’ (π β ran πΉ β π) |
30 | 23, 29 | sstrid 3956 |
. . . . . . . . . . . . . . . . 17
β’ (π β (πΉ β (1...π)) β π) |
31 | | resttopon 22528 |
. . . . . . . . . . . . . . . . 17
β’ ((π½ β (TopOnβπ) β§ (πΉ β (1...π)) β π) β (π½ βΎt (πΉ β (1...π))) β (TopOnβ(πΉ β (1...π)))) |
32 | 3, 30, 31 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ (π β (π½ βΎt (πΉ β (1...π))) β (TopOnβ(πΉ β (1...π)))) |
33 | | topontop 22278 |
. . . . . . . . . . . . . . . 16
β’ ((π½ βΎt (πΉ β (1...π))) β (TopOnβ(πΉ β (1...π))) β (π½ βΎt (πΉ β (1...π))) β Top) |
34 | 32, 33 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β (π½ βΎt (πΉ β (1...π))) β Top) |
35 | | fzfid 13884 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (1...π) β Fin) |
36 | 28 | ffund 6673 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β Fun πΉ) |
37 | | fz1ssnn 13478 |
. . . . . . . . . . . . . . . . . . . 20
β’
(1...π) β
β |
38 | 28 | fdmd 6680 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β dom πΉ = β) |
39 | 37, 38 | sseqtrrid 3998 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (1...π) β dom πΉ) |
40 | | fores 6767 |
. . . . . . . . . . . . . . . . . . 19
β’ ((Fun
πΉ β§ (1...π) β dom πΉ) β (πΉ βΎ (1...π)):(1...π)βontoβ(πΉ β (1...π))) |
41 | 36, 39, 40 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (πΉ βΎ (1...π)):(1...π)βontoβ(πΉ β (1...π))) |
42 | | fofi 9285 |
. . . . . . . . . . . . . . . . . 18
β’
(((1...π) β Fin
β§ (πΉ βΎ (1...π)):(1...π)βontoβ(πΉ β (1...π))) β (πΉ β (1...π)) β Fin) |
43 | 35, 41, 42 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’ (π β (πΉ β (1...π)) β Fin) |
44 | | pwfi 9125 |
. . . . . . . . . . . . . . . . 17
β’ ((πΉ β (1...π)) β Fin β π« (πΉ β (1...π)) β Fin) |
45 | 43, 44 | sylib 217 |
. . . . . . . . . . . . . . . 16
β’ (π β π« (πΉ β (1...π)) β Fin) |
46 | | restsspw 17318 |
. . . . . . . . . . . . . . . 16
β’ (π½ βΎt (πΉ β (1...π))) β π« (πΉ β (1...π)) |
47 | | ssfi 9120 |
. . . . . . . . . . . . . . . 16
β’
((π« (πΉ
β (1...π)) β Fin
β§ (π½
βΎt (πΉ
β (1...π))) β
π« (πΉ β
(1...π))) β (π½ βΎt (πΉ β (1...π))) β Fin) |
48 | 45, 46, 47 | sylancl 587 |
. . . . . . . . . . . . . . 15
β’ (π β (π½ βΎt (πΉ β (1...π))) β Fin) |
49 | 34, 48 | elind 4155 |
. . . . . . . . . . . . . 14
β’ (π β (π½ βΎt (πΉ β (1...π))) β (Top β© Fin)) |
50 | | fincmp 22760 |
. . . . . . . . . . . . . 14
β’ ((π½ βΎt (πΉ β (1...π))) β (Top β© Fin) β (π½ βΎt (πΉ β (1...π))) β Comp) |
51 | 49, 50 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β (π½ βΎt (πΉ β (1...π))) β Comp) |
52 | | topontop 22278 |
. . . . . . . . . . . . . . 15
β’ (π½ β (TopOnβπ) β π½ β Top) |
53 | 3, 52 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β π½ β Top) |
54 | | toponuni 22279 |
. . . . . . . . . . . . . . . 16
β’ (π½ β (TopOnβπ) β π = βͺ π½) |
55 | 3, 54 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β π = βͺ π½) |
56 | 30, 55 | sseqtrd 3985 |
. . . . . . . . . . . . . 14
β’ (π β (πΉ β (1...π)) β βͺ π½) |
57 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’ βͺ π½ =
βͺ π½ |
58 | 57 | cmpsub 22767 |
. . . . . . . . . . . . . 14
β’ ((π½ β Top β§ (πΉ β (1...π)) β βͺ π½) β ((π½ βΎt (πΉ β (1...π))) β Comp β βπ’ β π« π½((πΉ β (1...π)) β βͺ π’ β βπ β (π« π’ β© Fin)(πΉ β (1...π)) β βͺ π ))) |
59 | 53, 56, 58 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (π β ((π½ βΎt (πΉ β (1...π))) β Comp β βπ’ β π« π½((πΉ β (1...π)) β βͺ π’ β βπ β (π« π’ β© Fin)(πΉ β (1...π)) β βͺ π ))) |
60 | 51, 59 | mpbid 231 |
. . . . . . . . . . . 12
β’ (π β βπ’ β π« π½((πΉ β (1...π)) β βͺ π’ β βπ β (π« π’ β© Fin)(πΉ β (1...π)) β βͺ π )) |
61 | 60 | r19.21bi 3233 |
. . . . . . . . . . 11
β’ ((π β§ π’ β π« π½) β ((πΉ β (1...π)) β βͺ π’ β βπ β (π« π’ β© Fin)(πΉ β (1...π)) β βͺ π )) |
62 | 27, 61 | syl5 34 |
. . . . . . . . . 10
β’ ((π β§ π’ β π« π½) β ((ran πΉ βͺ {π΄}) β βͺ
π’ β βπ β (π« π’ β© Fin)(πΉ β (1...π)) β βͺ π )) |
63 | 62 | impr 456 |
. . . . . . . . 9
β’ ((π β§ (π’ β π« π½ β§ (ran πΉ βͺ {π΄}) β βͺ
π’)) β βπ β (π« π’ β© Fin)(πΉ β (1...π)) β βͺ π ) |
64 | 63 | adantr 482 |
. . . . . . . 8
β’ (((π β§ (π’ β π« π½ β§ (ran πΉ βͺ {π΄}) β βͺ
π’)) β§ ((π€ β π’ β§ π΄ β π€) β§ (π β β β§ βπ β
(β€β₯βπ)(πΉβπ) β π€))) β βπ β (π« π’ β© Fin)(πΉ β (1...π)) β βͺ π ) |
65 | | simprl 770 |
. . . . . . . . . . . . . 14
β’ ((((π β§ (π’ β π« π½ β§ (ran πΉ βͺ {π΄}) β βͺ
π’)) β§ ((π€ β π’ β§ π΄ β π€) β§ (π β β β§ βπ β
(β€β₯βπ)(πΉβπ) β π€))) β§ (π β (π« π’ β© Fin) β§ (πΉ β (1...π)) β βͺ π )) β π β (π« π’ β© Fin)) |
66 | 65 | elin1d 4159 |
. . . . . . . . . . . . 13
β’ ((((π β§ (π’ β π« π½ β§ (ran πΉ βͺ {π΄}) β βͺ
π’)) β§ ((π€ β π’ β§ π΄ β π€) β§ (π β β β§ βπ β
(β€β₯βπ)(πΉβπ) β π€))) β§ (π β (π« π’ β© Fin) β§ (πΉ β (1...π)) β βͺ π )) β π β π« π’) |
67 | 66 | elpwid 4570 |
. . . . . . . . . . . 12
β’ ((((π β§ (π’ β π« π½ β§ (ran πΉ βͺ {π΄}) β βͺ
π’)) β§ ((π€ β π’ β§ π΄ β π€) β§ (π β β β§ βπ β
(β€β₯βπ)(πΉβπ) β π€))) β§ (π β (π« π’ β© Fin) β§ (πΉ β (1...π)) β βͺ π )) β π β π’) |
68 | | simprll 778 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π’ β π« π½ β§ (ran πΉ βͺ {π΄}) β βͺ
π’)) β§ ((π€ β π’ β§ π΄ β π€) β§ (π β β β§ βπ β
(β€β₯βπ)(πΉβπ) β π€))) β π€ β π’) |
69 | 68 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((((π β§ (π’ β π« π½ β§ (ran πΉ βͺ {π΄}) β βͺ
π’)) β§ ((π€ β π’ β§ π΄ β π€) β§ (π β β β§ βπ β
(β€β₯βπ)(πΉβπ) β π€))) β§ (π β (π« π’ β© Fin) β§ (πΉ β (1...π)) β βͺ π )) β π€ β π’) |
70 | 69 | snssd 4770 |
. . . . . . . . . . . 12
β’ ((((π β§ (π’ β π« π½ β§ (ran πΉ βͺ {π΄}) β βͺ
π’)) β§ ((π€ β π’ β§ π΄ β π€) β§ (π β β β§ βπ β
(β€β₯βπ)(πΉβπ) β π€))) β§ (π β (π« π’ β© Fin) β§ (πΉ β (1...π)) β βͺ π )) β {π€} β π’) |
71 | 67, 70 | unssd 4147 |
. . . . . . . . . . 11
β’ ((((π β§ (π’ β π« π½ β§ (ran πΉ βͺ {π΄}) β βͺ
π’)) β§ ((π€ β π’ β§ π΄ β π€) β§ (π β β β§ βπ β
(β€β₯βπ)(πΉβπ) β π€))) β§ (π β (π« π’ β© Fin) β§ (πΉ β (1...π)) β βͺ π )) β (π βͺ {π€}) β π’) |
72 | | vex 3448 |
. . . . . . . . . . . 12
β’ π’ β V |
73 | 72 | elpw2 5303 |
. . . . . . . . . . 11
β’ ((π βͺ {π€}) β π« π’ β (π βͺ {π€}) β π’) |
74 | 71, 73 | sylibr 233 |
. . . . . . . . . 10
β’ ((((π β§ (π’ β π« π½ β§ (ran πΉ βͺ {π΄}) β βͺ
π’)) β§ ((π€ β π’ β§ π΄ β π€) β§ (π β β β§ βπ β
(β€β₯βπ)(πΉβπ) β π€))) β§ (π β (π« π’ β© Fin) β§ (πΉ β (1...π)) β βͺ π )) β (π βͺ {π€}) β π« π’) |
75 | 65 | elin2d 4160 |
. . . . . . . . . . 11
β’ ((((π β§ (π’ β π« π½ β§ (ran πΉ βͺ {π΄}) β βͺ
π’)) β§ ((π€ β π’ β§ π΄ β π€) β§ (π β β β§ βπ β
(β€β₯βπ)(πΉβπ) β π€))) β§ (π β (π« π’ β© Fin) β§ (πΉ β (1...π)) β βͺ π )) β π β Fin) |
76 | | snfi 8991 |
. . . . . . . . . . 11
β’ {π€} β Fin |
77 | | unfi 9119 |
. . . . . . . . . . 11
β’ ((π β Fin β§ {π€} β Fin) β (π βͺ {π€}) β Fin) |
78 | 75, 76, 77 | sylancl 587 |
. . . . . . . . . 10
β’ ((((π β§ (π’ β π« π½ β§ (ran πΉ βͺ {π΄}) β βͺ
π’)) β§ ((π€ β π’ β§ π΄ β π€) β§ (π β β β§ βπ β
(β€β₯βπ)(πΉβπ) β π€))) β§ (π β (π« π’ β© Fin) β§ (πΉ β (1...π)) β βͺ π )) β (π βͺ {π€}) β Fin) |
79 | 74, 78 | elind 4155 |
. . . . . . . . 9
β’ ((((π β§ (π’ β π« π½ β§ (ran πΉ βͺ {π΄}) β βͺ
π’)) β§ ((π€ β π’ β§ π΄ β π€) β§ (π β β β§ βπ β
(β€β₯βπ)(πΉβπ) β π€))) β§ (π β (π« π’ β© Fin) β§ (πΉ β (1...π)) β βͺ π )) β (π βͺ {π€}) β (π« π’ β© Fin)) |
80 | 28 | ffnd 6670 |
. . . . . . . . . . . . 13
β’ (π β πΉ Fn β) |
81 | 80 | ad3antrrr 729 |
. . . . . . . . . . . 12
β’ ((((π β§ (π’ β π« π½ β§ (ran πΉ βͺ {π΄}) β βͺ
π’)) β§ ((π€ β π’ β§ π΄ β π€) β§ (π β β β§ βπ β
(β€β₯βπ)(πΉβπ) β π€))) β§ (π β (π« π’ β© Fin) β§ (πΉ β (1...π)) β βͺ π )) β πΉ Fn β) |
82 | | simprrr 781 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π’ β π« π½ β§ (ran πΉ βͺ {π΄}) β βͺ
π’)) β§ ((π€ β π’ β§ π΄ β π€) β§ (π β β β§ βπ β
(β€β₯βπ)(πΉβπ) β π€))) β βπ β (β€β₯βπ)(πΉβπ) β π€) |
83 | 82 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ (π’ β π« π½ β§ (ran πΉ βͺ {π΄}) β βͺ
π’)) β§ ((π€ β π’ β§ π΄ β π€) β§ (π β β β§ βπ β
(β€β₯βπ)(πΉβπ) β π€))) β§ (π β (π« π’ β© Fin) β§ (πΉ β (1...π)) β βͺ π )) β βπ β
(β€β₯βπ)(πΉβπ) β π€) |
84 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β (πΉβπ) = (πΉβπ)) |
85 | 84 | eleq1d 2819 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β ((πΉβπ) β π€ β (πΉβπ) β π€)) |
86 | 85 | rspccva 3579 |
. . . . . . . . . . . . . . . . 17
β’
((βπ β
(β€β₯βπ)(πΉβπ) β π€ β§ π β (β€β₯βπ)) β (πΉβπ) β π€) |
87 | 83, 86 | sylan 581 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ (π’ β π« π½ β§ (ran πΉ βͺ {π΄}) β βͺ
π’)) β§ ((π€ β π’ β§ π΄ β π€) β§ (π β β β§ βπ β
(β€β₯βπ)(πΉβπ) β π€))) β§ (π β (π« π’ β© Fin) β§ (πΉ β (1...π)) β βͺ π )) β§ π β (β€β₯βπ)) β (πΉβπ) β π€) |
88 | | elun2 4138 |
. . . . . . . . . . . . . . . 16
β’ ((πΉβπ) β π€ β (πΉβπ) β (βͺ π βͺ π€)) |
89 | 87, 88 | syl 17 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ (π’ β π« π½ β§ (ran πΉ βͺ {π΄}) β βͺ
π’)) β§ ((π€ β π’ β§ π΄ β π€) β§ (π β β β§ βπ β
(β€β₯βπ)(πΉβπ) β π€))) β§ (π β (π« π’ β© Fin) β§ (πΉ β (1...π)) β βͺ π )) β§ π β (β€β₯βπ)) β (πΉβπ) β (βͺ π βͺ π€)) |
90 | 89 | adantlr 714 |
. . . . . . . . . . . . . 14
β’
((((((π β§ (π’ β π« π½ β§ (ran πΉ βͺ {π΄}) β βͺ
π’)) β§ ((π€ β π’ β§ π΄ β π€) β§ (π β β β§ βπ β
(β€β₯βπ)(πΉβπ) β π€))) β§ (π β (π« π’ β© Fin) β§ (πΉ β (1...π)) β βͺ π )) β§ π β β) β§ π β (β€β₯βπ)) β (πΉβπ) β (βͺ π βͺ π€)) |
91 | | elnnuz 12812 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β β π β
(β€β₯β1)) |
92 | 91 | anbi1i 625 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§ π β
(β€β₯βπ)) β (π β (β€β₯β1)
β§ π β
(β€β₯βπ))) |
93 | | elfzuzb 13441 |
. . . . . . . . . . . . . . . . 17
β’ (π β (1...π) β (π β (β€β₯β1)
β§ π β
(β€β₯βπ))) |
94 | 92, 93 | bitr4i 278 |
. . . . . . . . . . . . . . . 16
β’ ((π β β β§ π β
(β€β₯βπ)) β π β (1...π)) |
95 | | simprr 772 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ (π’ β π« π½ β§ (ran πΉ βͺ {π΄}) β βͺ
π’)) β§ ((π€ β π’ β§ π΄ β π€) β§ (π β β β§ βπ β
(β€β₯βπ)(πΉβπ) β π€))) β§ (π β (π« π’ β© Fin) β§ (πΉ β (1...π)) β βͺ π )) β (πΉ β (1...π)) β βͺ π ) |
96 | | funimass4 6908 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((Fun
πΉ β§ (1...π) β dom πΉ) β ((πΉ β (1...π)) β βͺ π β βπ β (1...π)(πΉβπ) β βͺ π )) |
97 | 36, 39, 96 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β ((πΉ β (1...π)) β βͺ π β βπ β (1...π)(πΉβπ) β βͺ π )) |
98 | 97 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ (π’ β π« π½ β§ (ran πΉ βͺ {π΄}) β βͺ
π’)) β§ ((π€ β π’ β§ π΄ β π€) β§ (π β β β§ βπ β
(β€β₯βπ)(πΉβπ) β π€))) β§ (π β (π« π’ β© Fin) β§ (πΉ β (1...π)) β βͺ π )) β ((πΉ β (1...π)) β βͺ π β βπ β (1...π)(πΉβπ) β βͺ π )) |
99 | 95, 98 | mpbid 231 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ (π’ β π« π½ β§ (ran πΉ βͺ {π΄}) β βͺ
π’)) β§ ((π€ β π’ β§ π΄ β π€) β§ (π β β β§ βπ β
(β€β₯βπ)(πΉβπ) β π€))) β§ (π β (π« π’ β© Fin) β§ (πΉ β (1...π)) β βͺ π )) β βπ β (1...π)(πΉβπ) β βͺ π ) |
100 | 99 | r19.21bi 3233 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ (π’ β π« π½ β§ (ran πΉ βͺ {π΄}) β βͺ
π’)) β§ ((π€ β π’ β§ π΄ β π€) β§ (π β β β§ βπ β
(β€β₯βπ)(πΉβπ) β π€))) β§ (π β (π« π’ β© Fin) β§ (πΉ β (1...π)) β βͺ π )) β§ π β (1...π)) β (πΉβπ) β βͺ π ) |
101 | | elun1 4137 |
. . . . . . . . . . . . . . . . 17
β’ ((πΉβπ) β βͺ π β (πΉβπ) β (βͺ π βͺ π€)) |
102 | 100, 101 | syl 17 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ (π’ β π« π½ β§ (ran πΉ βͺ {π΄}) β βͺ
π’)) β§ ((π€ β π’ β§ π΄ β π€) β§ (π β β β§ βπ β
(β€β₯βπ)(πΉβπ) β π€))) β§ (π β (π« π’ β© Fin) β§ (πΉ β (1...π)) β βͺ π )) β§ π β (1...π)) β (πΉβπ) β (βͺ π βͺ π€)) |
103 | 94, 102 | sylan2b 595 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ (π’ β π« π½ β§ (ran πΉ βͺ {π΄}) β βͺ
π’)) β§ ((π€ β π’ β§ π΄ β π€) β§ (π β β β§ βπ β
(β€β₯βπ)(πΉβπ) β π€))) β§ (π β (π« π’ β© Fin) β§ (πΉ β (1...π)) β βͺ π )) β§ (π β β β§ π β (β€β₯βπ))) β (πΉβπ) β (βͺ π βͺ π€)) |
104 | 103 | anassrs 469 |
. . . . . . . . . . . . . 14
β’
((((((π β§ (π’ β π« π½ β§ (ran πΉ βͺ {π΄}) β βͺ
π’)) β§ ((π€ β π’ β§ π΄ β π€) β§ (π β β β§ βπ β
(β€β₯βπ)(πΉβπ) β π€))) β§ (π β (π« π’ β© Fin) β§ (πΉ β (1...π)) β βͺ π )) β§ π β β) β§ π β (β€β₯βπ)) β (πΉβπ) β (βͺ π βͺ π€)) |
105 | | simprl 770 |
. . . . . . . . . . . . . . . 16
β’ (((π€ β π’ β§ π΄ β π€) β§ (π β β β§ βπ β
(β€β₯βπ)(πΉβπ) β π€)) β π β β) |
106 | 105 | ad2antlr 726 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (π’ β π« π½ β§ (ran πΉ βͺ {π΄}) β βͺ
π’)) β§ ((π€ β π’ β§ π΄ β π€) β§ (π β β β§ βπ β
(β€β₯βπ)(πΉβπ) β π€))) β§ (π β (π« π’ β© Fin) β§ (πΉ β (1...π)) β βͺ π )) β π β β) |
107 | | nnz 12525 |
. . . . . . . . . . . . . . . 16
β’ (π β β β π β
β€) |
108 | | nnz 12525 |
. . . . . . . . . . . . . . . 16
β’ (π β β β π β
β€) |
109 | | uztric 12792 |
. . . . . . . . . . . . . . . 16
β’ ((π β β€ β§ π β β€) β (π β
(β€β₯βπ) β¨ π β (β€β₯βπ))) |
110 | 107, 108,
109 | syl2an 597 |
. . . . . . . . . . . . . . 15
β’ ((π β β β§ π β β) β (π β
(β€β₯βπ) β¨ π β (β€β₯βπ))) |
111 | 106, 110 | sylan 581 |
. . . . . . . . . . . . . 14
β’
(((((π β§ (π’ β π« π½ β§ (ran πΉ βͺ {π΄}) β βͺ
π’)) β§ ((π€ β π’ β§ π΄ β π€) β§ (π β β β§ βπ β
(β€β₯βπ)(πΉβπ) β π€))) β§ (π β (π« π’ β© Fin) β§ (πΉ β (1...π)) β βͺ π )) β§ π β β) β (π β (β€β₯βπ) β¨ π β (β€β₯βπ))) |
112 | 90, 104, 111 | mpjaodan 958 |
. . . . . . . . . . . . 13
β’
(((((π β§ (π’ β π« π½ β§ (ran πΉ βͺ {π΄}) β βͺ
π’)) β§ ((π€ β π’ β§ π΄ β π€) β§ (π β β β§ βπ β
(β€β₯βπ)(πΉβπ) β π€))) β§ (π β (π« π’ β© Fin) β§ (πΉ β (1...π)) β βͺ π )) β§ π β β) β (πΉβπ) β (βͺ π βͺ π€)) |
113 | 112 | ralrimiva 3140 |
. . . . . . . . . . . 12
β’ ((((π β§ (π’ β π« π½ β§ (ran πΉ βͺ {π΄}) β βͺ
π’)) β§ ((π€ β π’ β§ π΄ β π€) β§ (π β β β§ βπ β
(β€β₯βπ)(πΉβπ) β π€))) β§ (π β (π« π’ β© Fin) β§ (πΉ β (1...π)) β βͺ π )) β βπ β β (πΉβπ) β (βͺ π βͺ π€)) |
114 | | fnfvrnss 7069 |
. . . . . . . . . . . 12
β’ ((πΉ Fn β β§ βπ β β (πΉβπ) β (βͺ π βͺ π€)) β ran πΉ β (βͺ π βͺ π€)) |
115 | 81, 113, 114 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((((π β§ (π’ β π« π½ β§ (ran πΉ βͺ {π΄}) β βͺ
π’)) β§ ((π€ β π’ β§ π΄ β π€) β§ (π β β β§ βπ β
(β€β₯βπ)(πΉβπ) β π€))) β§ (π β (π« π’ β© Fin) β§ (πΉ β (1...π)) β βͺ π )) β ran πΉ β (βͺ π βͺ π€)) |
116 | | elun2 4138 |
. . . . . . . . . . . . . 14
β’ (π΄ β π€ β π΄ β (βͺ π βͺ π€)) |
117 | 116 | ad2antlr 726 |
. . . . . . . . . . . . 13
β’ (((π€ β π’ β§ π΄ β π€) β§ (π β β β§ βπ β
(β€β₯βπ)(πΉβπ) β π€)) β π΄ β (βͺ π βͺ π€)) |
118 | 117 | ad2antlr 726 |
. . . . . . . . . . . 12
β’ ((((π β§ (π’ β π« π½ β§ (ran πΉ βͺ {π΄}) β βͺ
π’)) β§ ((π€ β π’ β§ π΄ β π€) β§ (π β β β§ βπ β
(β€β₯βπ)(πΉβπ) β π€))) β§ (π β (π« π’ β© Fin) β§ (πΉ β (1...π)) β βͺ π )) β π΄ β (βͺ π βͺ π€)) |
119 | 118 | snssd 4770 |
. . . . . . . . . . 11
β’ ((((π β§ (π’ β π« π½ β§ (ran πΉ βͺ {π΄}) β βͺ
π’)) β§ ((π€ β π’ β§ π΄ β π€) β§ (π β β β§ βπ β
(β€β₯βπ)(πΉβπ) β π€))) β§ (π β (π« π’ β© Fin) β§ (πΉ β (1...π)) β βͺ π )) β {π΄} β (βͺ
π βͺ π€)) |
120 | 115, 119 | unssd 4147 |
. . . . . . . . . 10
β’ ((((π β§ (π’ β π« π½ β§ (ran πΉ βͺ {π΄}) β βͺ
π’)) β§ ((π€ β π’ β§ π΄ β π€) β§ (π β β β§ βπ β
(β€β₯βπ)(πΉβπ) β π€))) β§ (π β (π« π’ β© Fin) β§ (πΉ β (1...π)) β βͺ π )) β (ran πΉ βͺ {π΄}) β (βͺ
π βͺ π€)) |
121 | | uniun 4892 |
. . . . . . . . . . 11
β’ βͺ (π
βͺ {π€}) = (βͺ π
βͺ βͺ {π€}) |
122 | | unisnv 4889 |
. . . . . . . . . . . 12
β’ βͺ {π€}
= π€ |
123 | 122 | uneq2i 4121 |
. . . . . . . . . . 11
β’ (βͺ π
βͺ βͺ {π€}) = (βͺ π βͺ π€) |
124 | 121, 123 | eqtri 2761 |
. . . . . . . . . 10
β’ βͺ (π
βͺ {π€}) = (βͺ π
βͺ π€) |
125 | 120, 124 | sseqtrrdi 3996 |
. . . . . . . . 9
β’ ((((π β§ (π’ β π« π½ β§ (ran πΉ βͺ {π΄}) β βͺ
π’)) β§ ((π€ β π’ β§ π΄ β π€) β§ (π β β β§ βπ β
(β€β₯βπ)(πΉβπ) β π€))) β§ (π β (π« π’ β© Fin) β§ (πΉ β (1...π)) β βͺ π )) β (ran πΉ βͺ {π΄}) β βͺ
(π βͺ {π€})) |
126 | | unieq 4877 |
. . . . . . . . . . 11
β’ (π£ = (π βͺ {π€}) β βͺ π£ = βͺ
(π βͺ {π€})) |
127 | 126 | sseq2d 3977 |
. . . . . . . . . 10
β’ (π£ = (π βͺ {π€}) β ((ran πΉ βͺ {π΄}) β βͺ
π£ β (ran πΉ βͺ {π΄}) β βͺ
(π βͺ {π€}))) |
128 | 127 | rspcev 3580 |
. . . . . . . . 9
β’ (((π βͺ {π€}) β (π« π’ β© Fin) β§ (ran πΉ βͺ {π΄}) β βͺ
(π βͺ {π€})) β βπ£ β (π« π’ β© Fin)(ran πΉ βͺ {π΄}) β βͺ
π£) |
129 | 79, 125, 128 | syl2anc 585 |
. . . . . . . 8
β’ ((((π β§ (π’ β π« π½ β§ (ran πΉ βͺ {π΄}) β βͺ
π’)) β§ ((π€ β π’ β§ π΄ β π€) β§ (π β β β§ βπ β
(β€β₯βπ)(πΉβπ) β π€))) β§ (π β (π« π’ β© Fin) β§ (πΉ β (1...π)) β βͺ π )) β βπ£ β (π« π’ β© Fin)(ran πΉ βͺ {π΄}) β βͺ
π£) |
130 | 64, 129 | rexlimddv 3155 |
. . . . . . 7
β’ (((π β§ (π’ β π« π½ β§ (ran πΉ βͺ {π΄}) β βͺ
π’)) β§ ((π€ β π’ β§ π΄ β π€) β§ (π β β β§ βπ β
(β€β₯βπ)(πΉβπ) β π€))) β βπ£ β (π« π’ β© Fin)(ran πΉ βͺ {π΄}) β βͺ
π£) |
131 | 130 | anassrs 469 |
. . . . . 6
β’ ((((π β§ (π’ β π« π½ β§ (ran πΉ βͺ {π΄}) β βͺ
π’)) β§ (π€ β π’ β§ π΄ β π€)) β§ (π β β β§ βπ β
(β€β₯βπ)(πΉβπ) β π€)) β βπ£ β (π« π’ β© Fin)(ran πΉ βͺ {π΄}) β βͺ
π£) |
132 | 22, 131 | rexlimddv 3155 |
. . . . 5
β’ (((π β§ (π’ β π« π½ β§ (ran πΉ βͺ {π΄}) β βͺ
π’)) β§ (π€ β π’ β§ π΄ β π€)) β βπ£ β (π« π’ β© Fin)(ran πΉ βͺ {π΄}) β βͺ
π£) |
133 | 13, 132 | rexlimddv 3155 |
. . . 4
β’ ((π β§ (π’ β π« π½ β§ (ran πΉ βͺ {π΄}) β βͺ
π’)) β βπ£ β (π« π’ β© Fin)(ran πΉ βͺ {π΄}) β βͺ
π£) |
134 | 133 | expr 458 |
. . 3
β’ ((π β§ π’ β π« π½) β ((ran πΉ βͺ {π΄}) β βͺ
π’ β βπ£ β (π« π’ β© Fin)(ran πΉ βͺ {π΄}) β βͺ
π£)) |
135 | 134 | ralrimiva 3140 |
. 2
β’ (π β βπ’ β π« π½((ran πΉ βͺ {π΄}) β βͺ
π’ β βπ£ β (π« π’ β© Fin)(ran πΉ βͺ {π΄}) β βͺ
π£)) |
136 | 6 | snssd 4770 |
. . . . 5
β’ (π β {π΄} β π) |
137 | 29, 136 | unssd 4147 |
. . . 4
β’ (π β (ran πΉ βͺ {π΄}) β π) |
138 | 137, 55 | sseqtrd 3985 |
. . 3
β’ (π β (ran πΉ βͺ {π΄}) β βͺ
π½) |
139 | 57 | cmpsub 22767 |
. . 3
β’ ((π½ β Top β§ (ran πΉ βͺ {π΄}) β βͺ
π½) β ((π½ βΎt (ran πΉ βͺ {π΄})) β Comp β βπ’ β π« π½((ran πΉ βͺ {π΄}) β βͺ
π’ β βπ£ β (π« π’ β© Fin)(ran πΉ βͺ {π΄}) β βͺ
π£))) |
140 | 53, 138, 139 | syl2anc 585 |
. 2
β’ (π β ((π½ βΎt (ran πΉ βͺ {π΄})) β Comp β βπ’ β π« π½((ran πΉ βͺ {π΄}) β βͺ
π’ β βπ£ β (π« π’ β© Fin)(ran πΉ βͺ {π΄}) β βͺ
π£))) |
141 | 135, 140 | mpbird 257 |
1
β’ (π β (π½ βΎt (ran πΉ βͺ {π΄})) β Comp) |