Step | Hyp | Ref
| Expression |
1 | | ctssdclemn0.f |
. . . . . . . . 9
β’ (π β πΉ:πβontoβπ΄) |
2 | 1 | ad2antrr 488 |
. . . . . . . 8
β’ (((π β§ π β Ο) β§ π β π) β πΉ:πβontoβπ΄) |
3 | | fof 5439 |
. . . . . . . 8
β’ (πΉ:πβontoβπ΄ β πΉ:πβΆπ΄) |
4 | 2, 3 | syl 14 |
. . . . . . 7
β’ (((π β§ π β Ο) β§ π β π) β πΉ:πβΆπ΄) |
5 | | simpr 110 |
. . . . . . 7
β’ (((π β§ π β Ο) β§ π β π) β π β π) |
6 | 4, 5 | ffvelcdmd 5653 |
. . . . . 6
β’ (((π β§ π β Ο) β§ π β π) β (πΉβπ) β π΄) |
7 | | djulcl 7050 |
. . . . . 6
β’ ((πΉβπ) β π΄ β (inlβ(πΉβπ)) β (π΄ β 1o)) |
8 | 6, 7 | syl 14 |
. . . . 5
β’ (((π β§ π β Ο) β§ π β π) β (inlβ(πΉβπ)) β (π΄ β 1o)) |
9 | | 0lt1o 6441 |
. . . . . . 7
β’ β
β 1o |
10 | | djurcl 7051 |
. . . . . . 7
β’ (β
β 1o β (inrββ
) β (π΄ β 1o)) |
11 | 9, 10 | ax-mp 5 |
. . . . . 6
β’
(inrββ
) β (π΄ β 1o) |
12 | 11 | a1i 9 |
. . . . 5
β’ (((π β§ π β Ο) β§ Β¬ π β π) β (inrββ
) β (π΄ β
1o)) |
13 | | eleq1 2240 |
. . . . . . 7
β’ (π = π β (π β π β π β π)) |
14 | 13 | dcbid 838 |
. . . . . 6
β’ (π = π β (DECID π β π β DECID π β π)) |
15 | | ctssdclemn0.dc |
. . . . . . 7
β’ (π β βπ β Ο DECID π β π) |
16 | 15 | adantr 276 |
. . . . . 6
β’ ((π β§ π β Ο) β βπ β Ο
DECID π
β π) |
17 | | simpr 110 |
. . . . . 6
β’ ((π β§ π β Ο) β π β Ο) |
18 | 14, 16, 17 | rspcdva 2847 |
. . . . 5
β’ ((π β§ π β Ο) β DECID
π β π) |
19 | 8, 12, 18 | ifcldadc 3564 |
. . . 4
β’ ((π β§ π β Ο) β if(π β π, (inlβ(πΉβπ)), (inrββ
)) β (π΄ β
1o)) |
20 | 19 | fmpttd 5672 |
. . 3
β’ (π β (π β Ο β¦ if(π β π, (inlβ(πΉβπ)),
(inrββ
))):ΟβΆ(π΄ β 1o)) |
21 | 1 | ad3antrrr 492 |
. . . . . . . . 9
β’ ((((π β§ π₯ β (π΄ β 1o)) β§ π§ β π΄) β§ π₯ = (inlβπ§)) β πΉ:πβontoβπ΄) |
22 | | simplr 528 |
. . . . . . . . 9
β’ ((((π β§ π₯ β (π΄ β 1o)) β§ π§ β π΄) β§ π₯ = (inlβπ§)) β π§ β π΄) |
23 | | foelrn 5754 |
. . . . . . . . 9
β’ ((πΉ:πβontoβπ΄ β§ π§ β π΄) β βπ¦ β π π§ = (πΉβπ¦)) |
24 | 21, 22, 23 | syl2anc 411 |
. . . . . . . 8
β’ ((((π β§ π₯ β (π΄ β 1o)) β§ π§ β π΄) β§ π₯ = (inlβπ§)) β βπ¦ β π π§ = (πΉβπ¦)) |
25 | | simplr 528 |
. . . . . . . . . . . 12
β’
((((((π β§ π₯ β (π΄ β 1o)) β§ π§ β π΄) β§ π₯ = (inlβπ§)) β§ π¦ β π) β§ π§ = (πΉβπ¦)) β π¦ β π) |
26 | 25 | iftrued 3542 |
. . . . . . . . . . 11
β’
((((((π β§ π₯ β (π΄ β 1o)) β§ π§ β π΄) β§ π₯ = (inlβπ§)) β§ π¦ β π) β§ π§ = (πΉβπ¦)) β if(π¦ β π, (inlβ(πΉβπ¦)), (inrββ
)) = (inlβ(πΉβπ¦))) |
27 | | eqid 2177 |
. . . . . . . . . . . 12
β’ (π β Ο β¦ if(π β π, (inlβ(πΉβπ)), (inrββ
))) = (π β Ο β¦ if(π β π, (inlβ(πΉβπ)), (inrββ
))) |
28 | | eleq1 2240 |
. . . . . . . . . . . . 13
β’ (π = π¦ β (π β π β π¦ β π)) |
29 | | 2fveq3 5521 |
. . . . . . . . . . . . 13
β’ (π = π¦ β (inlβ(πΉβπ)) = (inlβ(πΉβπ¦))) |
30 | 28, 29 | ifbieq1d 3557 |
. . . . . . . . . . . 12
β’ (π = π¦ β if(π β π, (inlβ(πΉβπ)), (inrββ
)) = if(π¦ β π, (inlβ(πΉβπ¦)), (inrββ
))) |
31 | | ctssdclemn0.ss |
. . . . . . . . . . . . . 14
β’ (π β π β Ο) |
32 | 31 | ad5antr 496 |
. . . . . . . . . . . . 13
β’
((((((π β§ π₯ β (π΄ β 1o)) β§ π§ β π΄) β§ π₯ = (inlβπ§)) β§ π¦ β π) β§ π§ = (πΉβπ¦)) β π β Ο) |
33 | 32, 25 | sseldd 3157 |
. . . . . . . . . . . 12
β’
((((((π β§ π₯ β (π΄ β 1o)) β§ π§ β π΄) β§ π₯ = (inlβπ§)) β§ π¦ β π) β§ π§ = (πΉβπ¦)) β π¦ β Ο) |
34 | 1, 3 | syl 14 |
. . . . . . . . . . . . . . . 16
β’ (π β πΉ:πβΆπ΄) |
35 | 34 | ad5antr 496 |
. . . . . . . . . . . . . . 15
β’
((((((π β§ π₯ β (π΄ β 1o)) β§ π§ β π΄) β§ π₯ = (inlβπ§)) β§ π¦ β π) β§ π§ = (πΉβπ¦)) β πΉ:πβΆπ΄) |
36 | 35, 25 | ffvelcdmd 5653 |
. . . . . . . . . . . . . 14
β’
((((((π β§ π₯ β (π΄ β 1o)) β§ π§ β π΄) β§ π₯ = (inlβπ§)) β§ π¦ β π) β§ π§ = (πΉβπ¦)) β (πΉβπ¦) β π΄) |
37 | | djulcl 7050 |
. . . . . . . . . . . . . 14
β’ ((πΉβπ¦) β π΄ β (inlβ(πΉβπ¦)) β (π΄ β 1o)) |
38 | 36, 37 | syl 14 |
. . . . . . . . . . . . 13
β’
((((((π β§ π₯ β (π΄ β 1o)) β§ π§ β π΄) β§ π₯ = (inlβπ§)) β§ π¦ β π) β§ π§ = (πΉβπ¦)) β (inlβ(πΉβπ¦)) β (π΄ β 1o)) |
39 | 26, 38 | eqeltrd 2254 |
. . . . . . . . . . . 12
β’
((((((π β§ π₯ β (π΄ β 1o)) β§ π§ β π΄) β§ π₯ = (inlβπ§)) β§ π¦ β π) β§ π§ = (πΉβπ¦)) β if(π¦ β π, (inlβ(πΉβπ¦)), (inrββ
)) β (π΄ β
1o)) |
40 | 27, 30, 33, 39 | fvmptd3 5610 |
. . . . . . . . . . 11
β’
((((((π β§ π₯ β (π΄ β 1o)) β§ π§ β π΄) β§ π₯ = (inlβπ§)) β§ π¦ β π) β§ π§ = (πΉβπ¦)) β ((π β Ο β¦ if(π β π, (inlβ(πΉβπ)), (inrββ
)))βπ¦) = if(π¦ β π, (inlβ(πΉβπ¦)), (inrββ
))) |
41 | | simpllr 534 |
. . . . . . . . . . . 12
β’
((((((π β§ π₯ β (π΄ β 1o)) β§ π§ β π΄) β§ π₯ = (inlβπ§)) β§ π¦ β π) β§ π§ = (πΉβπ¦)) β π₯ = (inlβπ§)) |
42 | | simpr 110 |
. . . . . . . . . . . . 13
β’
((((((π β§ π₯ β (π΄ β 1o)) β§ π§ β π΄) β§ π₯ = (inlβπ§)) β§ π¦ β π) β§ π§ = (πΉβπ¦)) β π§ = (πΉβπ¦)) |
43 | 42 | fveq2d 5520 |
. . . . . . . . . . . 12
β’
((((((π β§ π₯ β (π΄ β 1o)) β§ π§ β π΄) β§ π₯ = (inlβπ§)) β§ π¦ β π) β§ π§ = (πΉβπ¦)) β (inlβπ§) = (inlβ(πΉβπ¦))) |
44 | 41, 43 | eqtrd 2210 |
. . . . . . . . . . 11
β’
((((((π β§ π₯ β (π΄ β 1o)) β§ π§ β π΄) β§ π₯ = (inlβπ§)) β§ π¦ β π) β§ π§ = (πΉβπ¦)) β π₯ = (inlβ(πΉβπ¦))) |
45 | 26, 40, 44 | 3eqtr4rd 2221 |
. . . . . . . . . 10
β’
((((((π β§ π₯ β (π΄ β 1o)) β§ π§ β π΄) β§ π₯ = (inlβπ§)) β§ π¦ β π) β§ π§ = (πΉβπ¦)) β π₯ = ((π β Ο β¦ if(π β π, (inlβ(πΉβπ)), (inrββ
)))βπ¦)) |
46 | 45 | ex 115 |
. . . . . . . . 9
β’
(((((π β§ π₯ β (π΄ β 1o)) β§ π§ β π΄) β§ π₯ = (inlβπ§)) β§ π¦ β π) β (π§ = (πΉβπ¦) β π₯ = ((π β Ο β¦ if(π β π, (inlβ(πΉβπ)), (inrββ
)))βπ¦))) |
47 | 46 | reximdva 2579 |
. . . . . . . 8
β’ ((((π β§ π₯ β (π΄ β 1o)) β§ π§ β π΄) β§ π₯ = (inlβπ§)) β (βπ¦ β π π§ = (πΉβπ¦) β βπ¦ β π π₯ = ((π β Ο β¦ if(π β π, (inlβ(πΉβπ)), (inrββ
)))βπ¦))) |
48 | 24, 47 | mpd 13 |
. . . . . . 7
β’ ((((π β§ π₯ β (π΄ β 1o)) β§ π§ β π΄) β§ π₯ = (inlβπ§)) β βπ¦ β π π₯ = ((π β Ο β¦ if(π β π, (inlβ(πΉβπ)), (inrββ
)))βπ¦)) |
49 | | ssrexv 3221 |
. . . . . . . . 9
β’ (π β Ο β
(βπ¦ β π π₯ = ((π β Ο β¦ if(π β π, (inlβ(πΉβπ)), (inrββ
)))βπ¦) β βπ¦ β Ο π₯ = ((π β Ο β¦ if(π β π, (inlβ(πΉβπ)), (inrββ
)))βπ¦))) |
50 | 31, 49 | syl 14 |
. . . . . . . 8
β’ (π β (βπ¦ β π π₯ = ((π β Ο β¦ if(π β π, (inlβ(πΉβπ)), (inrββ
)))βπ¦) β βπ¦ β Ο π₯ = ((π β Ο β¦ if(π β π, (inlβ(πΉβπ)), (inrββ
)))βπ¦))) |
51 | 50 | ad3antrrr 492 |
. . . . . . 7
β’ ((((π β§ π₯ β (π΄ β 1o)) β§ π§ β π΄) β§ π₯ = (inlβπ§)) β (βπ¦ β π π₯ = ((π β Ο β¦ if(π β π, (inlβ(πΉβπ)), (inrββ
)))βπ¦) β βπ¦ β Ο π₯ = ((π β Ο β¦ if(π β π, (inlβ(πΉβπ)), (inrββ
)))βπ¦))) |
52 | 48, 51 | mpd 13 |
. . . . . 6
β’ ((((π β§ π₯ β (π΄ β 1o)) β§ π§ β π΄) β§ π₯ = (inlβπ§)) β βπ¦ β Ο π₯ = ((π β Ο β¦ if(π β π, (inlβ(πΉβπ)), (inrββ
)))βπ¦)) |
53 | 52 | rexlimdva2 2597 |
. . . . 5
β’ ((π β§ π₯ β (π΄ β 1o)) β
(βπ§ β π΄ π₯ = (inlβπ§) β βπ¦ β Ο π₯ = ((π β Ο β¦ if(π β π, (inlβ(πΉβπ)), (inrββ
)))βπ¦))) |
54 | | peano1 4594 |
. . . . . . . 8
β’ β
β Ο |
55 | 54 | a1i 9 |
. . . . . . 7
β’ ((((π β§ π₯ β (π΄ β 1o)) β§ π§ β 1o) β§
π₯ = (inrβπ§)) β β
β
Ο) |
56 | | ctssdclemn0.n0 |
. . . . . . . . . 10
β’ (π β Β¬ β
β π) |
57 | 56 | ad3antrrr 492 |
. . . . . . . . 9
β’ ((((π β§ π₯ β (π΄ β 1o)) β§ π§ β 1o) β§
π₯ = (inrβπ§)) β Β¬ β
β
π) |
58 | 57 | iffalsed 3545 |
. . . . . . . 8
β’ ((((π β§ π₯ β (π΄ β 1o)) β§ π§ β 1o) β§
π₯ = (inrβπ§)) β if(β
β
π, (inlβ(πΉββ
)),
(inrββ
)) = (inrββ
)) |
59 | | eleq1 2240 |
. . . . . . . . . 10
β’ (π = β
β (π β π β β
β π)) |
60 | | 2fveq3 5521 |
. . . . . . . . . 10
β’ (π = β
β
(inlβ(πΉβπ)) = (inlβ(πΉββ
))) |
61 | 59, 60 | ifbieq1d 3557 |
. . . . . . . . 9
β’ (π = β
β if(π β π, (inlβ(πΉβπ)), (inrββ
)) = if(β
β
π, (inlβ(πΉββ
)),
(inrββ
))) |
62 | 58, 11 | eqeltrdi 2268 |
. . . . . . . . 9
β’ ((((π β§ π₯ β (π΄ β 1o)) β§ π§ β 1o) β§
π₯ = (inrβπ§)) β if(β
β
π, (inlβ(πΉββ
)),
(inrββ
)) β (π΄ β 1o)) |
63 | 27, 61, 55, 62 | fvmptd3 5610 |
. . . . . . . 8
β’ ((((π β§ π₯ β (π΄ β 1o)) β§ π§ β 1o) β§
π₯ = (inrβπ§)) β ((π β Ο β¦ if(π β π, (inlβ(πΉβπ)), (inrββ
)))ββ
) =
if(β
β π,
(inlβ(πΉββ
)),
(inrββ
))) |
64 | | simpr 110 |
. . . . . . . . 9
β’ ((((π β§ π₯ β (π΄ β 1o)) β§ π§ β 1o) β§
π₯ = (inrβπ§)) β π₯ = (inrβπ§)) |
65 | | simplr 528 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β (π΄ β 1o)) β§ π§ β 1o) β§
π₯ = (inrβπ§)) β π§ β 1o) |
66 | | el1o 6438 |
. . . . . . . . . . 11
β’ (π§ β 1o β
π§ =
β
) |
67 | 65, 66 | sylib 122 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β (π΄ β 1o)) β§ π§ β 1o) β§
π₯ = (inrβπ§)) β π§ = β
) |
68 | 67 | fveq2d 5520 |
. . . . . . . . 9
β’ ((((π β§ π₯ β (π΄ β 1o)) β§ π§ β 1o) β§
π₯ = (inrβπ§)) β (inrβπ§) =
(inrββ
)) |
69 | 64, 68 | eqtrd 2210 |
. . . . . . . 8
β’ ((((π β§ π₯ β (π΄ β 1o)) β§ π§ β 1o) β§
π₯ = (inrβπ§)) β π₯ = (inrββ
)) |
70 | 58, 63, 69 | 3eqtr4rd 2221 |
. . . . . . 7
β’ ((((π β§ π₯ β (π΄ β 1o)) β§ π§ β 1o) β§
π₯ = (inrβπ§)) β π₯ = ((π β Ο β¦ if(π β π, (inlβ(πΉβπ)),
(inrββ
)))ββ
)) |
71 | | fveq2 5516 |
. . . . . . . 8
β’ (π¦ = β
β ((π β Ο β¦ if(π β π, (inlβ(πΉβπ)), (inrββ
)))βπ¦) = ((π β Ο β¦ if(π β π, (inlβ(πΉβπ)),
(inrββ
)))ββ
)) |
72 | 71 | rspceeqv 2860 |
. . . . . . 7
β’ ((β
β Ο β§ π₯ =
((π β Ο β¦
if(π β π, (inlβ(πΉβπ)), (inrββ
)))ββ
))
β βπ¦ β
Ο π₯ = ((π β Ο β¦ if(π β π, (inlβ(πΉβπ)), (inrββ
)))βπ¦)) |
73 | 55, 70, 72 | syl2anc 411 |
. . . . . 6
β’ ((((π β§ π₯ β (π΄ β 1o)) β§ π§ β 1o) β§
π₯ = (inrβπ§)) β βπ¦ β Ο π₯ = ((π β Ο β¦ if(π β π, (inlβ(πΉβπ)), (inrββ
)))βπ¦)) |
74 | 73 | rexlimdva2 2597 |
. . . . 5
β’ ((π β§ π₯ β (π΄ β 1o)) β
(βπ§ β
1o π₯ =
(inrβπ§) β
βπ¦ β Ο
π₯ = ((π β Ο β¦ if(π β π, (inlβ(πΉβπ)), (inrββ
)))βπ¦))) |
75 | | djur 7068 |
. . . . . . 7
β’ (π₯ β (π΄ β 1o) β
(βπ§ β π΄ π₯ = (inlβπ§) β¨ βπ§ β 1o π₯ = (inrβπ§))) |
76 | 75 | biimpi 120 |
. . . . . 6
β’ (π₯ β (π΄ β 1o) β
(βπ§ β π΄ π₯ = (inlβπ§) β¨ βπ§ β 1o π₯ = (inrβπ§))) |
77 | 76 | adantl 277 |
. . . . 5
β’ ((π β§ π₯ β (π΄ β 1o)) β
(βπ§ β π΄ π₯ = (inlβπ§) β¨ βπ§ β 1o π₯ = (inrβπ§))) |
78 | 53, 74, 77 | mpjaod 718 |
. . . 4
β’ ((π β§ π₯ β (π΄ β 1o)) β
βπ¦ β Ο
π₯ = ((π β Ο β¦ if(π β π, (inlβ(πΉβπ)), (inrββ
)))βπ¦)) |
79 | 78 | ralrimiva 2550 |
. . 3
β’ (π β βπ₯ β (π΄ β 1o)βπ¦ β Ο π₯ = ((π β Ο β¦ if(π β π, (inlβ(πΉβπ)), (inrββ
)))βπ¦)) |
80 | | dffo3 5664 |
. . 3
β’ ((π β Ο β¦ if(π β π, (inlβ(πΉβπ)), (inrββ
))):Οβontoβ(π΄ β 1o) β ((π β Ο β¦ if(π β π, (inlβ(πΉβπ)),
(inrββ
))):ΟβΆ(π΄ β 1o) β§ βπ₯ β (π΄ β 1o)βπ¦ β Ο π₯ = ((π β Ο β¦ if(π β π, (inlβ(πΉβπ)), (inrββ
)))βπ¦))) |
81 | 20, 79, 80 | sylanbrc 417 |
. 2
β’ (π β (π β Ο β¦ if(π β π, (inlβ(πΉβπ)), (inrββ
))):Οβontoβ(π΄ β 1o)) |
82 | | omex 4593 |
. . . 4
β’ Ο
β V |
83 | 82 | mptex 5743 |
. . 3
β’ (π β Ο β¦ if(π β π, (inlβ(πΉβπ)), (inrββ
))) β
V |
84 | | foeq1 5435 |
. . 3
β’ (π = (π β Ο β¦ if(π β π, (inlβ(πΉβπ)), (inrββ
))) β (π:Οβontoβ(π΄ β 1o) β (π β Ο β¦ if(π β π, (inlβ(πΉβπ)), (inrββ
))):Οβontoβ(π΄ β 1o))) |
85 | 83, 84 | spcev 2833 |
. 2
β’ ((π β Ο β¦ if(π β π, (inlβ(πΉβπ)), (inrββ
))):Οβontoβ(π΄ β 1o) β βπ π:Οβontoβ(π΄ β 1o)) |
86 | 81, 85 | syl 14 |
1
β’ (π β βπ π:Οβontoβ(π΄ β 1o)) |