Step | Hyp | Ref
| Expression |
1 | | simplr 768 |
. . . 4
β’ (((π β β0
β§ Β¬ π β Fin)
β§ ((1...π) β
π β§ π΄ β (β€β₯βπ))) β Β¬ π β Fin) |
2 | | fzfi 13883 |
. . . 4
β’
(1...π) β
Fin |
3 | | difinf 9263 |
. . . 4
β’ ((Β¬
π β Fin β§
(1...π) β Fin) β
Β¬ (π β (1...π)) β Fin) |
4 | 1, 2, 3 | sylancl 587 |
. . 3
β’ (((π β β0
β§ Β¬ π β Fin)
β§ ((1...π) β
π β§ π΄ β (β€β₯βπ))) β Β¬ (π β (1...π)) β Fin) |
5 | | fzfi 13883 |
. . . 4
β’
(1...π΄) β
Fin |
6 | | diffi 9126 |
. . . 4
β’
((1...π΄) β Fin
β ((1...π΄) β
(1...π)) β
Fin) |
7 | 5, 6 | ax-mp 5 |
. . 3
β’
((1...π΄) β
(1...π)) β
Fin |
8 | | isinffi 9933 |
. . 3
β’ ((Β¬
(π β (1...π)) β Fin β§ ((1...π΄) β (1...π)) β Fin) β βπ π:((1...π΄) β (1...π))β1-1β(π β (1...π))) |
9 | 4, 7, 8 | sylancl 587 |
. 2
β’ (((π β β0
β§ Β¬ π β Fin)
β§ ((1...π) β
π β§ π΄ β (β€β₯βπ))) β βπ π:((1...π΄) β (1...π))β1-1β(π β (1...π))) |
10 | | f1f1orn 6796 |
. . . . . . . 8
β’ (π:((1...π΄) β (1...π))β1-1β(π β (1...π)) β π:((1...π΄) β (1...π))β1-1-ontoβran
π) |
11 | 10 | adantl 483 |
. . . . . . 7
β’ ((((π β β0
β§ Β¬ π β Fin)
β§ ((1...π) β
π β§ π΄ β (β€β₯βπ))) β§ π:((1...π΄) β (1...π))β1-1β(π β (1...π))) β π:((1...π΄) β (1...π))β1-1-ontoβran
π) |
12 | | f1oi 6823 |
. . . . . . . 8
β’ ( I
βΎ (1...π)):(1...π)β1-1-ontoβ(1...π) |
13 | 12 | a1i 11 |
. . . . . . 7
β’ ((((π β β0
β§ Β¬ π β Fin)
β§ ((1...π) β
π β§ π΄ β (β€β₯βπ))) β§ π:((1...π΄) β (1...π))β1-1β(π β (1...π))) β ( I βΎ (1...π)):(1...π)β1-1-ontoβ(1...π)) |
14 | | disjdifr 4433 |
. . . . . . . 8
β’
(((1...π΄) β
(1...π)) β© (1...π)) = β
|
15 | 14 | a1i 11 |
. . . . . . 7
β’ ((((π β β0
β§ Β¬ π β Fin)
β§ ((1...π) β
π β§ π΄ β (β€β₯βπ))) β§ π:((1...π΄) β (1...π))β1-1β(π β (1...π))) β (((1...π΄) β (1...π)) β© (1...π)) = β
) |
16 | | f1f 6739 |
. . . . . . . . . . . 12
β’ (π:((1...π΄) β (1...π))β1-1β(π β (1...π)) β π:((1...π΄) β (1...π))βΆ(π β (1...π))) |
17 | 16 | frnd 6677 |
. . . . . . . . . . 11
β’ (π:((1...π΄) β (1...π))β1-1β(π β (1...π)) β ran π β (π β (1...π))) |
18 | 17 | adantl 483 |
. . . . . . . . . 10
β’ ((((π β β0
β§ Β¬ π β Fin)
β§ ((1...π) β
π β§ π΄ β (β€β₯βπ))) β§ π:((1...π΄) β (1...π))β1-1β(π β (1...π))) β ran π β (π β (1...π))) |
19 | 18 | ssrind 4196 |
. . . . . . . . 9
β’ ((((π β β0
β§ Β¬ π β Fin)
β§ ((1...π) β
π β§ π΄ β (β€β₯βπ))) β§ π:((1...π΄) β (1...π))β1-1β(π β (1...π))) β (ran π β© (1...π)) β ((π β (1...π)) β© (1...π))) |
20 | | disjdifr 4433 |
. . . . . . . . 9
β’ ((π β (1...π)) β© (1...π)) = β
|
21 | 19, 20 | sseqtrdi 3995 |
. . . . . . . 8
β’ ((((π β β0
β§ Β¬ π β Fin)
β§ ((1...π) β
π β§ π΄ β (β€β₯βπ))) β§ π:((1...π΄) β (1...π))β1-1β(π β (1...π))) β (ran π β© (1...π)) β β
) |
22 | | ss0 4359 |
. . . . . . . 8
β’ ((ran
π β© (1...π)) β β
β (ran
π β© (1...π)) = β
) |
23 | 21, 22 | syl 17 |
. . . . . . 7
β’ ((((π β β0
β§ Β¬ π β Fin)
β§ ((1...π) β
π β§ π΄ β (β€β₯βπ))) β§ π:((1...π΄) β (1...π))β1-1β(π β (1...π))) β (ran π β© (1...π)) = β
) |
24 | | f1oun 6804 |
. . . . . . 7
β’ (((π:((1...π΄) β (1...π))β1-1-ontoβran
π β§ ( I βΎ
(1...π)):(1...π)β1-1-ontoβ(1...π)) β§ ((((1...π΄) β (1...π)) β© (1...π)) = β
β§ (ran π β© (1...π)) = β
)) β (π βͺ ( I βΎ (1...π))):(((1...π΄) β (1...π)) βͺ (1...π))β1-1-ontoβ(ran
π βͺ (1...π))) |
25 | 11, 13, 15, 23, 24 | syl22anc 838 |
. . . . . 6
β’ ((((π β β0
β§ Β¬ π β Fin)
β§ ((1...π) β
π β§ π΄ β (β€β₯βπ))) β§ π:((1...π΄) β (1...π))β1-1β(π β (1...π))) β (π βͺ ( I βΎ (1...π))):(((1...π΄) β (1...π)) βͺ (1...π))β1-1-ontoβ(ran
π βͺ (1...π))) |
26 | | f1of1 6784 |
. . . . . 6
β’ ((π βͺ ( I βΎ (1...π))):(((1...π΄) β (1...π)) βͺ (1...π))β1-1-ontoβ(ran
π βͺ (1...π)) β (π βͺ ( I βΎ (1...π))):(((1...π΄) β (1...π)) βͺ (1...π))β1-1β(ran π βͺ (1...π))) |
27 | 25, 26 | syl 17 |
. . . . 5
β’ ((((π β β0
β§ Β¬ π β Fin)
β§ ((1...π) β
π β§ π΄ β (β€β₯βπ))) β§ π:((1...π΄) β (1...π))β1-1β(π β (1...π))) β (π βͺ ( I βΎ (1...π))):(((1...π΄) β (1...π)) βͺ (1...π))β1-1β(ran π βͺ (1...π))) |
28 | | uncom 4114 |
. . . . . . 7
β’
(((1...π΄) β
(1...π)) βͺ (1...π)) = ((1...π) βͺ ((1...π΄) β (1...π))) |
29 | | simplrr 777 |
. . . . . . . . 9
β’ ((((π β β0
β§ Β¬ π β Fin)
β§ ((1...π) β
π β§ π΄ β (β€β₯βπ))) β§ π:((1...π΄) β (1...π))β1-1β(π β (1...π))) β π΄ β (β€β₯βπ)) |
30 | | fzss2 13487 |
. . . . . . . . 9
β’ (π΄ β
(β€β₯βπ) β (1...π) β (1...π΄)) |
31 | 29, 30 | syl 17 |
. . . . . . . 8
β’ ((((π β β0
β§ Β¬ π β Fin)
β§ ((1...π) β
π β§ π΄ β (β€β₯βπ))) β§ π:((1...π΄) β (1...π))β1-1β(π β (1...π))) β (1...π) β (1...π΄)) |
32 | | undif 4442 |
. . . . . . . 8
β’
((1...π) β
(1...π΄) β ((1...π) βͺ ((1...π΄) β (1...π))) = (1...π΄)) |
33 | 31, 32 | sylib 217 |
. . . . . . 7
β’ ((((π β β0
β§ Β¬ π β Fin)
β§ ((1...π) β
π β§ π΄ β (β€β₯βπ))) β§ π:((1...π΄) β (1...π))β1-1β(π β (1...π))) β ((1...π) βͺ ((1...π΄) β (1...π))) = (1...π΄)) |
34 | 28, 33 | eqtrid 2785 |
. . . . . 6
β’ ((((π β β0
β§ Β¬ π β Fin)
β§ ((1...π) β
π β§ π΄ β (β€β₯βπ))) β§ π:((1...π΄) β (1...π))β1-1β(π β (1...π))) β (((1...π΄) β (1...π)) βͺ (1...π)) = (1...π΄)) |
35 | | f1eq2 6735 |
. . . . . 6
β’
((((1...π΄) β
(1...π)) βͺ (1...π)) = (1...π΄) β ((π βͺ ( I βΎ (1...π))):(((1...π΄) β (1...π)) βͺ (1...π))β1-1β(ran π βͺ (1...π)) β (π βͺ ( I βΎ (1...π))):(1...π΄)β1-1β(ran π βͺ (1...π)))) |
36 | 34, 35 | syl 17 |
. . . . 5
β’ ((((π β β0
β§ Β¬ π β Fin)
β§ ((1...π) β
π β§ π΄ β (β€β₯βπ))) β§ π:((1...π΄) β (1...π))β1-1β(π β (1...π))) β ((π βͺ ( I βΎ (1...π))):(((1...π΄) β (1...π)) βͺ (1...π))β1-1β(ran π βͺ (1...π)) β (π βͺ ( I βΎ (1...π))):(1...π΄)β1-1β(ran π βͺ (1...π)))) |
37 | 27, 36 | mpbid 231 |
. . . 4
β’ ((((π β β0
β§ Β¬ π β Fin)
β§ ((1...π) β
π β§ π΄ β (β€β₯βπ))) β§ π:((1...π΄) β (1...π))β1-1β(π β (1...π))) β (π βͺ ( I βΎ (1...π))):(1...π΄)β1-1β(ran π βͺ (1...π))) |
38 | 17 | difss2d 4095 |
. . . . . 6
β’ (π:((1...π΄) β (1...π))β1-1β(π β (1...π)) β ran π β π) |
39 | 38 | adantl 483 |
. . . . 5
β’ ((((π β β0
β§ Β¬ π β Fin)
β§ ((1...π) β
π β§ π΄ β (β€β₯βπ))) β§ π:((1...π΄) β (1...π))β1-1β(π β (1...π))) β ran π β π) |
40 | | simplrl 776 |
. . . . 5
β’ ((((π β β0
β§ Β¬ π β Fin)
β§ ((1...π) β
π β§ π΄ β (β€β₯βπ))) β§ π:((1...π΄) β (1...π))β1-1β(π β (1...π))) β (1...π) β π) |
41 | 39, 40 | unssd 4147 |
. . . 4
β’ ((((π β β0
β§ Β¬ π β Fin)
β§ ((1...π) β
π β§ π΄ β (β€β₯βπ))) β§ π:((1...π΄) β (1...π))β1-1β(π β (1...π))) β (ran π βͺ (1...π)) β π) |
42 | | f1ss 6745 |
. . . 4
β’ (((π βͺ ( I βΎ (1...π))):(1...π΄)β1-1β(ran π βͺ (1...π)) β§ (ran π βͺ (1...π)) β π) β (π βͺ ( I βΎ (1...π))):(1...π΄)β1-1βπ) |
43 | 37, 41, 42 | syl2anc 585 |
. . 3
β’ ((((π β β0
β§ Β¬ π β Fin)
β§ ((1...π) β
π β§ π΄ β (β€β₯βπ))) β§ π:((1...π΄) β (1...π))β1-1β(π β (1...π))) β (π βͺ ( I βΎ (1...π))):(1...π΄)β1-1βπ) |
44 | | resundir 5953 |
. . . 4
β’ ((π βͺ ( I βΎ (1...π))) βΎ (1...π)) = ((π βΎ (1...π)) βͺ (( I βΎ (1...π)) βΎ (1...π))) |
45 | | dmres 5960 |
. . . . . . . 8
β’ dom
(π βΎ (1...π)) = ((1...π) β© dom π) |
46 | | incom 4162 |
. . . . . . . . 9
β’
((1...π) β© dom
π) = (dom π β© (1...π)) |
47 | | f1dm 6743 |
. . . . . . . . . . . 12
β’ (π:((1...π΄) β (1...π))β1-1β(π β (1...π)) β dom π = ((1...π΄) β (1...π))) |
48 | 47 | adantl 483 |
. . . . . . . . . . 11
β’ ((((π β β0
β§ Β¬ π β Fin)
β§ ((1...π) β
π β§ π΄ β (β€β₯βπ))) β§ π:((1...π΄) β (1...π))β1-1β(π β (1...π))) β dom π = ((1...π΄) β (1...π))) |
49 | 48 | ineq1d 4172 |
. . . . . . . . . 10
β’ ((((π β β0
β§ Β¬ π β Fin)
β§ ((1...π) β
π β§ π΄ β (β€β₯βπ))) β§ π:((1...π΄) β (1...π))β1-1β(π β (1...π))) β (dom π β© (1...π)) = (((1...π΄) β (1...π)) β© (1...π))) |
50 | 49, 14 | eqtrdi 2789 |
. . . . . . . . 9
β’ ((((π β β0
β§ Β¬ π β Fin)
β§ ((1...π) β
π β§ π΄ β (β€β₯βπ))) β§ π:((1...π΄) β (1...π))β1-1β(π β (1...π))) β (dom π β© (1...π)) = β
) |
51 | 46, 50 | eqtrid 2785 |
. . . . . . . 8
β’ ((((π β β0
β§ Β¬ π β Fin)
β§ ((1...π) β
π β§ π΄ β (β€β₯βπ))) β§ π:((1...π΄) β (1...π))β1-1β(π β (1...π))) β ((1...π) β© dom π) = β
) |
52 | 45, 51 | eqtrid 2785 |
. . . . . . 7
β’ ((((π β β0
β§ Β¬ π β Fin)
β§ ((1...π) β
π β§ π΄ β (β€β₯βπ))) β§ π:((1...π΄) β (1...π))β1-1β(π β (1...π))) β dom (π βΎ (1...π)) = β
) |
53 | | relres 5967 |
. . . . . . . 8
β’ Rel
(π βΎ (1...π)) |
54 | | reldm0 5884 |
. . . . . . . 8
β’ (Rel
(π βΎ (1...π)) β ((π βΎ (1...π)) = β
β dom (π βΎ (1...π)) = β
)) |
55 | 53, 54 | ax-mp 5 |
. . . . . . 7
β’ ((π βΎ (1...π)) = β
β dom (π βΎ (1...π)) = β
) |
56 | 52, 55 | sylibr 233 |
. . . . . 6
β’ ((((π β β0
β§ Β¬ π β Fin)
β§ ((1...π) β
π β§ π΄ β (β€β₯βπ))) β§ π:((1...π΄) β (1...π))β1-1β(π β (1...π))) β (π βΎ (1...π)) = β
) |
57 | | residm 5971 |
. . . . . . 7
β’ (( I
βΎ (1...π)) βΎ
(1...π)) = ( I βΎ
(1...π)) |
58 | 57 | a1i 11 |
. . . . . 6
β’ ((((π β β0
β§ Β¬ π β Fin)
β§ ((1...π) β
π β§ π΄ β (β€β₯βπ))) β§ π:((1...π΄) β (1...π))β1-1β(π β (1...π))) β (( I βΎ (1...π)) βΎ (1...π)) = ( I βΎ (1...π))) |
59 | 56, 58 | uneq12d 4125 |
. . . . 5
β’ ((((π β β0
β§ Β¬ π β Fin)
β§ ((1...π) β
π β§ π΄ β (β€β₯βπ))) β§ π:((1...π΄) β (1...π))β1-1β(π β (1...π))) β ((π βΎ (1...π)) βͺ (( I βΎ (1...π)) βΎ (1...π))) = (β
βͺ ( I βΎ (1...π)))) |
60 | | uncom 4114 |
. . . . . 6
β’ (β
βͺ ( I βΎ (1...π)))
= (( I βΎ (1...π))
βͺ β
) |
61 | | un0 4351 |
. . . . . 6
β’ (( I
βΎ (1...π)) βͺ
β
) = ( I βΎ (1...π)) |
62 | 60, 61 | eqtri 2761 |
. . . . 5
β’ (β
βͺ ( I βΎ (1...π)))
= ( I βΎ (1...π)) |
63 | 59, 62 | eqtrdi 2789 |
. . . 4
β’ ((((π β β0
β§ Β¬ π β Fin)
β§ ((1...π) β
π β§ π΄ β (β€β₯βπ))) β§ π:((1...π΄) β (1...π))β1-1β(π β (1...π))) β ((π βΎ (1...π)) βͺ (( I βΎ (1...π)) βΎ (1...π))) = ( I βΎ (1...π))) |
64 | 44, 63 | eqtrid 2785 |
. . 3
β’ ((((π β β0
β§ Β¬ π β Fin)
β§ ((1...π) β
π β§ π΄ β (β€β₯βπ))) β§ π:((1...π΄) β (1...π))β1-1β(π β (1...π))) β ((π βͺ ( I βΎ (1...π))) βΎ (1...π)) = ( I βΎ (1...π))) |
65 | | vex 3448 |
. . . . 5
β’ π β V |
66 | | ovex 7391 |
. . . . . 6
β’
(1...π) β
V |
67 | | resiexg 7852 |
. . . . . 6
β’
((1...π) β V
β ( I βΎ (1...π))
β V) |
68 | 66, 67 | ax-mp 5 |
. . . . 5
β’ ( I
βΎ (1...π)) β
V |
69 | 65, 68 | unex 7681 |
. . . 4
β’ (π βͺ ( I βΎ (1...π))) β V |
70 | | f1eq1 6734 |
. . . . 5
β’ (π = (π βͺ ( I βΎ (1...π))) β (π:(1...π΄)β1-1βπ β (π βͺ ( I βΎ (1...π))):(1...π΄)β1-1βπ)) |
71 | | reseq1 5932 |
. . . . . 6
β’ (π = (π βͺ ( I βΎ (1...π))) β (π βΎ (1...π)) = ((π βͺ ( I βΎ (1...π))) βΎ (1...π))) |
72 | 71 | eqeq1d 2735 |
. . . . 5
β’ (π = (π βͺ ( I βΎ (1...π))) β ((π βΎ (1...π)) = ( I βΎ (1...π)) β ((π βͺ ( I βΎ (1...π))) βΎ (1...π)) = ( I βΎ (1...π)))) |
73 | 70, 72 | anbi12d 632 |
. . . 4
β’ (π = (π βͺ ( I βΎ (1...π))) β ((π:(1...π΄)β1-1βπ β§ (π βΎ (1...π)) = ( I βΎ (1...π))) β ((π βͺ ( I βΎ (1...π))):(1...π΄)β1-1βπ β§ ((π βͺ ( I βΎ (1...π))) βΎ (1...π)) = ( I βΎ (1...π))))) |
74 | 69, 73 | spcev 3564 |
. . 3
β’ (((π βͺ ( I βΎ (1...π))):(1...π΄)β1-1βπ β§ ((π βͺ ( I βΎ (1...π))) βΎ (1...π)) = ( I βΎ (1...π))) β βπ(π:(1...π΄)β1-1βπ β§ (π βΎ (1...π)) = ( I βΎ (1...π)))) |
75 | 43, 64, 74 | syl2anc 585 |
. 2
β’ ((((π β β0
β§ Β¬ π β Fin)
β§ ((1...π) β
π β§ π΄ β (β€β₯βπ))) β§ π:((1...π΄) β (1...π))β1-1β(π β (1...π))) β βπ(π:(1...π΄)β1-1βπ β§ (π βΎ (1...π)) = ( I βΎ (1...π)))) |
76 | 9, 75 | exlimddv 1939 |
1
β’ (((π β β0
β§ Β¬ π β Fin)
β§ ((1...π) β
π β§ π΄ β (β€β₯βπ))) β βπ(π:(1...π΄)β1-1βπ β§ (π βΎ (1...π)) = ( I βΎ (1...π)))) |