Step | Hyp | Ref
| Expression |
1 | | elfznelfzo 13683 |
. . . . . . 7
β’ ((π β (0...πΎ) β§ Β¬ π β (1..^πΎ)) β (π = 0 β¨ π = πΎ)) |
2 | | fvinim0ffz 13697 |
. . . . . . . . . . . . 13
β’ ((πΉ:(0...πΎ)βΆπ β§ πΎ β β0) β (((πΉ β {0, πΎ}) β© (πΉ β (1..^πΎ))) = β
β ((πΉβ0) β (πΉ β (1..^πΎ)) β§ (πΉβπΎ) β (πΉ β (1..^πΎ))))) |
3 | | df-nel 3047 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΉβ0) β (πΉ β (1..^πΎ)) β Β¬ (πΉβ0) β (πΉ β (1..^πΎ))) |
4 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (0 =
π β (πΉβ0) = (πΉβπ)) |
5 | 4 | eqcoms 2741 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = 0 β (πΉβ0) = (πΉβπ)) |
6 | 5 | eleq1d 2819 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = 0 β ((πΉβ0) β (πΉ β (1..^πΎ)) β (πΉβπ) β (πΉ β (1..^πΎ)))) |
7 | 6 | notbid 318 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = 0 β (Β¬ (πΉβ0) β (πΉ β (1..^πΎ)) β Β¬ (πΉβπ) β (πΉ β (1..^πΎ)))) |
8 | 7 | biimpd 228 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = 0 β (Β¬ (πΉβ0) β (πΉ β (1..^πΎ)) β Β¬ (πΉβπ) β (πΉ β (1..^πΎ)))) |
9 | | ffn 6669 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (πΉ:(0...πΎ)βΆπ β πΉ Fn (0...πΎ)) |
10 | | 1eluzge0 12822 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ 1 β
(β€β₯β0) |
11 | | fzoss1 13605 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (1 β
(β€β₯β0) β (1..^πΎ) β (0..^πΎ)) |
12 | 10, 11 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (πΎ β β0
β (1..^πΎ) β
(0..^πΎ)) |
13 | | fzossfz 13597 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(0..^πΎ) β
(0...πΎ) |
14 | 12, 13 | sstrdi 3957 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (πΎ β β0
β (1..^πΎ) β
(0...πΎ)) |
15 | | fvelimab 6915 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((πΉ Fn (0...πΎ) β§ (1..^πΎ) β (0...πΎ)) β ((πΉβπ) β (πΉ β (1..^πΎ)) β βπ§ β (1..^πΎ)(πΉβπ§) = (πΉβπ))) |
16 | 9, 14, 15 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((πΉ:(0...πΎ)βΆπ β§ πΎ β β0) β ((πΉβπ) β (πΉ β (1..^πΎ)) β βπ§ β (1..^πΎ)(πΉβπ§) = (πΉβπ))) |
17 | 16 | notbid 318 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((πΉ:(0...πΎ)βΆπ β§ πΎ β β0) β (Β¬
(πΉβπ) β (πΉ β (1..^πΎ)) β Β¬ βπ§ β (1..^πΎ)(πΉβπ§) = (πΉβπ))) |
18 | | ralnex 3072 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(βπ§ β
(1..^πΎ) Β¬ (πΉβπ§) = (πΉβπ) β Β¬ βπ§ β (1..^πΎ)(πΉβπ§) = (πΉβπ)) |
19 | | fveqeq2 6852 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π§ = π β ((πΉβπ§) = (πΉβπ) β (πΉβπ) = (πΉβπ))) |
20 | 19 | notbid 318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π§ = π β (Β¬ (πΉβπ§) = (πΉβπ) β Β¬ (πΉβπ) = (πΉβπ))) |
21 | 20 | rspcva 3578 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β (1..^πΎ) β§ βπ§ β (1..^πΎ) Β¬ (πΉβπ§) = (πΉβπ)) β Β¬ (πΉβπ) = (πΉβπ)) |
22 | | pm2.21 123 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (Β¬
(πΉβπ) = (πΉβπ) β ((πΉβπ) = (πΉβπ) β π = π)) |
23 | 22 | a1d 25 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (Β¬
(πΉβπ) = (πΉβπ) β ((πΉβ0) β (πΉβπΎ) β ((πΉβπ) = (πΉβπ) β π = π))) |
24 | 23 | 2a1d 26 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (Β¬
(πΉβπ) = (πΉβπ) β (π β (0...πΎ) β ((πΉ:(0...πΎ)βΆπ β§ πΎ β β0) β ((πΉβ0) β (πΉβπΎ) β ((πΉβπ) = (πΉβπ) β π = π))))) |
25 | 21, 24 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β (1..^πΎ) β§ βπ§ β (1..^πΎ) Β¬ (πΉβπ§) = (πΉβπ)) β (π β (0...πΎ) β ((πΉ:(0...πΎ)βΆπ β§ πΎ β β0) β ((πΉβ0) β (πΉβπΎ) β ((πΉβπ) = (πΉβπ) β π = π))))) |
26 | 25 | expcom 415 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(βπ§ β
(1..^πΎ) Β¬ (πΉβπ§) = (πΉβπ) β (π β (1..^πΎ) β (π β (0...πΎ) β ((πΉ:(0...πΎ)βΆπ β§ πΎ β β0) β ((πΉβ0) β (πΉβπΎ) β ((πΉβπ) = (πΉβπ) β π = π)))))) |
27 | 26 | com24 95 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(βπ§ β
(1..^πΎ) Β¬ (πΉβπ§) = (πΉβπ) β ((πΉ:(0...πΎ)βΆπ β§ πΎ β β0) β (π β (0...πΎ) β (π β (1..^πΎ) β ((πΉβ0) β (πΉβπΎ) β ((πΉβπ) = (πΉβπ) β π = π)))))) |
28 | 18, 27 | sylbir 234 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (Β¬
βπ§ β (1..^πΎ)(πΉβπ§) = (πΉβπ) β ((πΉ:(0...πΎ)βΆπ β§ πΎ β β0) β (π β (0...πΎ) β (π β (1..^πΎ) β ((πΉβ0) β (πΉβπΎ) β ((πΉβπ) = (πΉβπ) β π = π)))))) |
29 | 28 | com12 32 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((πΉ:(0...πΎ)βΆπ β§ πΎ β β0) β (Β¬
βπ§ β (1..^πΎ)(πΉβπ§) = (πΉβπ) β (π β (0...πΎ) β (π β (1..^πΎ) β ((πΉβ0) β (πΉβπΎ) β ((πΉβπ) = (πΉβπ) β π = π)))))) |
30 | 17, 29 | sylbid 239 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((πΉ:(0...πΎ)βΆπ β§ πΎ β β0) β (Β¬
(πΉβπ) β (πΉ β (1..^πΎ)) β (π β (0...πΎ) β (π β (1..^πΎ) β ((πΉβ0) β (πΉβπΎ) β ((πΉβπ) = (πΉβπ) β π = π)))))) |
31 | 30 | com12 32 |
. . . . . . . . . . . . . . . . . . 19
β’ (Β¬
(πΉβπ) β (πΉ β (1..^πΎ)) β ((πΉ:(0...πΎ)βΆπ β§ πΎ β β0) β (π β (0...πΎ) β (π β (1..^πΎ) β ((πΉβ0) β (πΉβπΎ) β ((πΉβπ) = (πΉβπ) β π = π)))))) |
32 | 8, 31 | syl6com 37 |
. . . . . . . . . . . . . . . . . 18
β’ (Β¬
(πΉβ0) β (πΉ β (1..^πΎ)) β (π = 0 β ((πΉ:(0...πΎ)βΆπ β§ πΎ β β0) β (π β (0...πΎ) β (π β (1..^πΎ) β ((πΉβ0) β (πΉβπΎ) β ((πΉβπ) = (πΉβπ) β π = π))))))) |
33 | 3, 32 | sylbi 216 |
. . . . . . . . . . . . . . . . 17
β’ ((πΉβ0) β (πΉ β (1..^πΎ)) β (π = 0 β ((πΉ:(0...πΎ)βΆπ β§ πΎ β β0) β (π β (0...πΎ) β (π β (1..^πΎ) β ((πΉβ0) β (πΉβπΎ) β ((πΉβπ) = (πΉβπ) β π = π))))))) |
34 | 33 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ (((πΉβ0) β (πΉ β (1..^πΎ)) β§ (πΉβπΎ) β (πΉ β (1..^πΎ))) β (π = 0 β ((πΉ:(0...πΎ)βΆπ β§ πΎ β β0) β (π β (0...πΎ) β (π β (1..^πΎ) β ((πΉβ0) β (πΉβπΎ) β ((πΉβπ) = (πΉβπ) β π = π))))))) |
35 | 34 | com12 32 |
. . . . . . . . . . . . . . 15
β’ (π = 0 β (((πΉβ0) β (πΉ β (1..^πΎ)) β§ (πΉβπΎ) β (πΉ β (1..^πΎ))) β ((πΉ:(0...πΎ)βΆπ β§ πΎ β β0) β (π β (0...πΎ) β (π β (1..^πΎ) β ((πΉβ0) β (πΉβπΎ) β ((πΉβπ) = (πΉβπ) β π = π))))))) |
36 | | df-nel 3047 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΉβπΎ) β (πΉ β (1..^πΎ)) β Β¬ (πΉβπΎ) β (πΉ β (1..^πΎ))) |
37 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (πΎ = π β (πΉβπΎ) = (πΉβπ)) |
38 | 37 | eqcoms 2741 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = πΎ β (πΉβπΎ) = (πΉβπ)) |
39 | 38 | eleq1d 2819 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = πΎ β ((πΉβπΎ) β (πΉ β (1..^πΎ)) β (πΉβπ) β (πΉ β (1..^πΎ)))) |
40 | 39 | notbid 318 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = πΎ β (Β¬ (πΉβπΎ) β (πΉ β (1..^πΎ)) β Β¬ (πΉβπ) β (πΉ β (1..^πΎ)))) |
41 | 40 | biimpd 228 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = πΎ β (Β¬ (πΉβπΎ) β (πΉ β (1..^πΎ)) β Β¬ (πΉβπ) β (πΉ β (1..^πΎ)))) |
42 | 41, 31 | syl6com 37 |
. . . . . . . . . . . . . . . . . 18
β’ (Β¬
(πΉβπΎ) β (πΉ β (1..^πΎ)) β (π = πΎ β ((πΉ:(0...πΎ)βΆπ β§ πΎ β β0) β (π β (0...πΎ) β (π β (1..^πΎ) β ((πΉβ0) β (πΉβπΎ) β ((πΉβπ) = (πΉβπ) β π = π))))))) |
43 | 36, 42 | sylbi 216 |
. . . . . . . . . . . . . . . . 17
β’ ((πΉβπΎ) β (πΉ β (1..^πΎ)) β (π = πΎ β ((πΉ:(0...πΎ)βΆπ β§ πΎ β β0) β (π β (0...πΎ) β (π β (1..^πΎ) β ((πΉβ0) β (πΉβπΎ) β ((πΉβπ) = (πΉβπ) β π = π))))))) |
44 | 43 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ (((πΉβ0) β (πΉ β (1..^πΎ)) β§ (πΉβπΎ) β (πΉ β (1..^πΎ))) β (π = πΎ β ((πΉ:(0...πΎ)βΆπ β§ πΎ β β0) β (π β (0...πΎ) β (π β (1..^πΎ) β ((πΉβ0) β (πΉβπΎ) β ((πΉβπ) = (πΉβπ) β π = π))))))) |
45 | 44 | com12 32 |
. . . . . . . . . . . . . . 15
β’ (π = πΎ β (((πΉβ0) β (πΉ β (1..^πΎ)) β§ (πΉβπΎ) β (πΉ β (1..^πΎ))) β ((πΉ:(0...πΎ)βΆπ β§ πΎ β β0) β (π β (0...πΎ) β (π β (1..^πΎ) β ((πΉβ0) β (πΉβπΎ) β ((πΉβπ) = (πΉβπ) β π = π))))))) |
46 | 35, 45 | jaoi 856 |
. . . . . . . . . . . . . 14
β’ ((π = 0 β¨ π = πΎ) β (((πΉβ0) β (πΉ β (1..^πΎ)) β§ (πΉβπΎ) β (πΉ β (1..^πΎ))) β ((πΉ:(0...πΎ)βΆπ β§ πΎ β β0) β (π β (0...πΎ) β (π β (1..^πΎ) β ((πΉβ0) β (πΉβπΎ) β ((πΉβπ) = (πΉβπ) β π = π))))))) |
47 | 46 | com13 88 |
. . . . . . . . . . . . 13
β’ ((πΉ:(0...πΎ)βΆπ β§ πΎ β β0) β (((πΉβ0) β (πΉ β (1..^πΎ)) β§ (πΉβπΎ) β (πΉ β (1..^πΎ))) β ((π = 0 β¨ π = πΎ) β (π β (0...πΎ) β (π β (1..^πΎ) β ((πΉβ0) β (πΉβπΎ) β ((πΉβπ) = (πΉβπ) β π = π))))))) |
48 | 2, 47 | sylbid 239 |
. . . . . . . . . . . 12
β’ ((πΉ:(0...πΎ)βΆπ β§ πΎ β β0) β (((πΉ β {0, πΎ}) β© (πΉ β (1..^πΎ))) = β
β ((π = 0 β¨ π = πΎ) β (π β (0...πΎ) β (π β (1..^πΎ) β ((πΉβ0) β (πΉβπΎ) β ((πΉβπ) = (πΉβπ) β π = π))))))) |
49 | 48 | com14 96 |
. . . . . . . . . . 11
β’ (π β (0...πΎ) β (((πΉ β {0, πΎ}) β© (πΉ β (1..^πΎ))) = β
β ((π = 0 β¨ π = πΎ) β ((πΉ:(0...πΎ)βΆπ β§ πΎ β β0) β (π β (1..^πΎ) β ((πΉβ0) β (πΉβπΎ) β ((πΉβπ) = (πΉβπ) β π = π))))))) |
50 | 49 | com12 32 |
. . . . . . . . . 10
β’ (((πΉ β {0, πΎ}) β© (πΉ β (1..^πΎ))) = β
β (π β (0...πΎ) β ((π = 0 β¨ π = πΎ) β ((πΉ:(0...πΎ)βΆπ β§ πΎ β β0) β (π β (1..^πΎ) β ((πΉβ0) β (πΉβπΎ) β ((πΉβπ) = (πΉβπ) β π = π))))))) |
51 | 50 | com15 101 |
. . . . . . . . 9
β’ (π β (1..^πΎ) β (π β (0...πΎ) β ((π = 0 β¨ π = πΎ) β ((πΉ:(0...πΎ)βΆπ β§ πΎ β β0) β (((πΉ β {0, πΎ}) β© (πΉ β (1..^πΎ))) = β
β ((πΉβ0) β (πΉβπΎ) β ((πΉβπ) = (πΉβπ) β π = π))))))) |
52 | | elfznelfzo 13683 |
. . . . . . . . . . 11
β’ ((π β (0...πΎ) β§ Β¬ π β (1..^πΎ)) β (π = 0 β¨ π = πΎ)) |
53 | | eqtr3 2759 |
. . . . . . . . . . . . . 14
β’ ((π = 0 β§ π = 0) β π = π) |
54 | | 2a1 28 |
. . . . . . . . . . . . . . 15
β’ (π = π β ((πΉβ0) β (πΉβπΎ) β ((πΉβπ) = (πΉβπ) β π = π))) |
55 | 54 | 2a1d 26 |
. . . . . . . . . . . . . 14
β’ (π = π β ((πΉ:(0...πΎ)βΆπ β§ πΎ β β0) β (((πΉ β {0, πΎ}) β© (πΉ β (1..^πΎ))) = β
β ((πΉβ0) β (πΉβπΎ) β ((πΉβπ) = (πΉβπ) β π = π))))) |
56 | 53, 55 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π = 0 β§ π = 0) β ((πΉ:(0...πΎ)βΆπ β§ πΎ β β0) β (((πΉ β {0, πΎ}) β© (πΉ β (1..^πΎ))) = β
β ((πΉβ0) β (πΉβπΎ) β ((πΉβπ) = (πΉβπ) β π = π))))) |
57 | 5 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ ((π = πΎ β§ π = 0) β (πΉβ0) = (πΉβπ)) |
58 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . 18
β’ (πΎ = π β (πΉβπΎ) = (πΉβπ)) |
59 | 58 | eqcoms 2741 |
. . . . . . . . . . . . . . . . 17
β’ (π = πΎ β (πΉβπΎ) = (πΉβπ)) |
60 | 59 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π = πΎ β§ π = 0) β (πΉβπΎ) = (πΉβπ)) |
61 | 57, 60 | neeq12d 3002 |
. . . . . . . . . . . . . . 15
β’ ((π = πΎ β§ π = 0) β ((πΉβ0) β (πΉβπΎ) β (πΉβπ) β (πΉβπ))) |
62 | | df-ne 2941 |
. . . . . . . . . . . . . . . 16
β’ ((πΉβπ) β (πΉβπ) β Β¬ (πΉβπ) = (πΉβπ)) |
63 | | pm2.24 124 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΉβπ) = (πΉβπ) β (Β¬ (πΉβπ) = (πΉβπ) β π = π)) |
64 | 63 | eqcoms 2741 |
. . . . . . . . . . . . . . . . 17
β’ ((πΉβπ) = (πΉβπ) β (Β¬ (πΉβπ) = (πΉβπ) β π = π)) |
65 | 64 | com12 32 |
. . . . . . . . . . . . . . . 16
β’ (Β¬
(πΉβπ) = (πΉβπ) β ((πΉβπ) = (πΉβπ) β π = π)) |
66 | 62, 65 | sylbi 216 |
. . . . . . . . . . . . . . 15
β’ ((πΉβπ) β (πΉβπ) β ((πΉβπ) = (πΉβπ) β π = π)) |
67 | 61, 66 | syl6bi 253 |
. . . . . . . . . . . . . 14
β’ ((π = πΎ β§ π = 0) β ((πΉβ0) β (πΉβπΎ) β ((πΉβπ) = (πΉβπ) β π = π))) |
68 | 67 | 2a1d 26 |
. . . . . . . . . . . . 13
β’ ((π = πΎ β§ π = 0) β ((πΉ:(0...πΎ)βΆπ β§ πΎ β β0) β (((πΉ β {0, πΎ}) β© (πΉ β (1..^πΎ))) = β
β ((πΉβ0) β (πΉβπΎ) β ((πΉβπ) = (πΉβπ) β π = π))))) |
69 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . 18
β’ (0 =
π β (πΉβ0) = (πΉβπ)) |
70 | 69 | eqcoms 2741 |
. . . . . . . . . . . . . . . . 17
β’ (π = 0 β (πΉβ0) = (πΉβπ)) |
71 | 70 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π = 0 β§ π = πΎ) β (πΉβ0) = (πΉβπ)) |
72 | 38 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ ((π = 0 β§ π = πΎ) β (πΉβπΎ) = (πΉβπ)) |
73 | 71, 72 | neeq12d 3002 |
. . . . . . . . . . . . . . 15
β’ ((π = 0 β§ π = πΎ) β ((πΉβ0) β (πΉβπΎ) β (πΉβπ) β (πΉβπ))) |
74 | | df-ne 2941 |
. . . . . . . . . . . . . . . 16
β’ ((πΉβπ) β (πΉβπ) β Β¬ (πΉβπ) = (πΉβπ)) |
75 | 74, 22 | sylbi 216 |
. . . . . . . . . . . . . . 15
β’ ((πΉβπ) β (πΉβπ) β ((πΉβπ) = (πΉβπ) β π = π)) |
76 | 73, 75 | syl6bi 253 |
. . . . . . . . . . . . . 14
β’ ((π = 0 β§ π = πΎ) β ((πΉβ0) β (πΉβπΎ) β ((πΉβπ) = (πΉβπ) β π = π))) |
77 | 76 | 2a1d 26 |
. . . . . . . . . . . . 13
β’ ((π = 0 β§ π = πΎ) β ((πΉ:(0...πΎ)βΆπ β§ πΎ β β0) β (((πΉ β {0, πΎ}) β© (πΉ β (1..^πΎ))) = β
β ((πΉβ0) β (πΉβπΎ) β ((πΉβπ) = (πΉβπ) β π = π))))) |
78 | | eqtr3 2759 |
. . . . . . . . . . . . . 14
β’ ((π = πΎ β§ π = πΎ) β π = π) |
79 | 78, 55 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π = πΎ β§ π = πΎ) β ((πΉ:(0...πΎ)βΆπ β§ πΎ β β0) β (((πΉ β {0, πΎ}) β© (πΉ β (1..^πΎ))) = β
β ((πΉβ0) β (πΉβπΎ) β ((πΉβπ) = (πΉβπ) β π = π))))) |
80 | 56, 68, 77, 79 | ccase 1037 |
. . . . . . . . . . . 12
β’ (((π = 0 β¨ π = πΎ) β§ (π = 0 β¨ π = πΎ)) β ((πΉ:(0...πΎ)βΆπ β§ πΎ β β0) β (((πΉ β {0, πΎ}) β© (πΉ β (1..^πΎ))) = β
β ((πΉβ0) β (πΉβπΎ) β ((πΉβπ) = (πΉβπ) β π = π))))) |
81 | 80 | ex 414 |
. . . . . . . . . . 11
β’ ((π = 0 β¨ π = πΎ) β ((π = 0 β¨ π = πΎ) β ((πΉ:(0...πΎ)βΆπ β§ πΎ β β0) β (((πΉ β {0, πΎ}) β© (πΉ β (1..^πΎ))) = β
β ((πΉβ0) β (πΉβπΎ) β ((πΉβπ) = (πΉβπ) β π = π)))))) |
82 | 52, 81 | syl 17 |
. . . . . . . . . 10
β’ ((π β (0...πΎ) β§ Β¬ π β (1..^πΎ)) β ((π = 0 β¨ π = πΎ) β ((πΉ:(0...πΎ)βΆπ β§ πΎ β β0) β (((πΉ β {0, πΎ}) β© (πΉ β (1..^πΎ))) = β
β ((πΉβ0) β (πΉβπΎ) β ((πΉβπ) = (πΉβπ) β π = π)))))) |
83 | 82 | expcom 415 |
. . . . . . . . 9
β’ (Β¬
π β (1..^πΎ) β (π β (0...πΎ) β ((π = 0 β¨ π = πΎ) β ((πΉ:(0...πΎ)βΆπ β§ πΎ β β0) β (((πΉ β {0, πΎ}) β© (πΉ β (1..^πΎ))) = β
β ((πΉβ0) β (πΉβπΎ) β ((πΉβπ) = (πΉβπ) β π = π))))))) |
84 | 51, 83 | pm2.61i 182 |
. . . . . . . 8
β’ (π β (0...πΎ) β ((π = 0 β¨ π = πΎ) β ((πΉ:(0...πΎ)βΆπ β§ πΎ β β0) β (((πΉ β {0, πΎ}) β© (πΉ β (1..^πΎ))) = β
β ((πΉβ0) β (πΉβπΎ) β ((πΉβπ) = (πΉβπ) β π = π)))))) |
85 | 84 | com12 32 |
. . . . . . 7
β’ ((π = 0 β¨ π = πΎ) β (π β (0...πΎ) β ((πΉ:(0...πΎ)βΆπ β§ πΎ β β0) β (((πΉ β {0, πΎ}) β© (πΉ β (1..^πΎ))) = β
β ((πΉβ0) β (πΉβπΎ) β ((πΉβπ) = (πΉβπ) β π = π)))))) |
86 | 1, 85 | syl 17 |
. . . . . 6
β’ ((π β (0...πΎ) β§ Β¬ π β (1..^πΎ)) β (π β (0...πΎ) β ((πΉ:(0...πΎ)βΆπ β§ πΎ β β0) β (((πΉ β {0, πΎ}) β© (πΉ β (1..^πΎ))) = β
β ((πΉβ0) β (πΉβπΎ) β ((πΉβπ) = (πΉβπ) β π = π)))))) |
87 | 86 | ex 414 |
. . . . 5
β’ (π β (0...πΎ) β (Β¬ π β (1..^πΎ) β (π β (0...πΎ) β ((πΉ:(0...πΎ)βΆπ β§ πΎ β β0) β (((πΉ β {0, πΎ}) β© (πΉ β (1..^πΎ))) = β
β ((πΉβ0) β (πΉβπΎ) β ((πΉβπ) = (πΉβπ) β π = π))))))) |
88 | 87 | com23 86 |
. . . 4
β’ (π β (0...πΎ) β (π β (0...πΎ) β (Β¬ π β (1..^πΎ) β ((πΉ:(0...πΎ)βΆπ β§ πΎ β β0) β (((πΉ β {0, πΎ}) β© (πΉ β (1..^πΎ))) = β
β ((πΉβ0) β (πΉβπΎ) β ((πΉβπ) = (πΉβπ) β π = π))))))) |
89 | 88 | impcom 409 |
. . 3
β’ ((π β (0...πΎ) β§ π β (0...πΎ)) β (Β¬ π β (1..^πΎ) β ((πΉ:(0...πΎ)βΆπ β§ πΎ β β0) β (((πΉ β {0, πΎ}) β© (πΉ β (1..^πΎ))) = β
β ((πΉβ0) β (πΉβπΎ) β ((πΉβπ) = (πΉβπ) β π = π)))))) |
90 | 89 | com12 32 |
. 2
β’ (Β¬
π β (1..^πΎ) β ((π β (0...πΎ) β§ π β (0...πΎ)) β ((πΉ:(0...πΎ)βΆπ β§ πΎ β β0) β (((πΉ β {0, πΎ}) β© (πΉ β (1..^πΎ))) = β
β ((πΉβ0) β (πΉβπΎ) β ((πΉβπ) = (πΉβπ) β π = π)))))) |
91 | 90 | com25 99 |
1
β’ (Β¬
π β (1..^πΎ) β ((πΉβ0) β (πΉβπΎ) β ((πΉ:(0...πΎ)βΆπ β§ πΎ β β0) β (((πΉ β {0, πΎ}) β© (πΉ β (1..^πΎ))) = β
β ((π β (0...πΎ) β§ π β (0...πΎ)) β ((πΉβπ) = (πΉβπ) β π = π)))))) |