Step | Hyp | Ref
| Expression |
1 | | 0lt1o 6440 |
. . . . . . . . . 10
β’ β
β 1o |
2 | | djurcl 7050 |
. . . . . . . . . 10
β’ (β
β 1o β (inrββ
) β (π΄ β 1o)) |
3 | 1, 2 | ax-mp 5 |
. . . . . . . . 9
β’
(inrββ
) β (π΄ β 1o) |
4 | 3 | a1i 9 |
. . . . . . . 8
β’
((((βπ₯ π₯ β π΄ β§ π:Οβontoβπ΄) β§ π β Ο) β§ π = β
) β (inrββ
) β
(π΄ β
1o)) |
5 | | simpllr 534 |
. . . . . . . . . . 11
β’
((((βπ₯ π₯ β π΄ β§ π:Οβontoβπ΄) β§ π β Ο) β§ Β¬ π = β
) β π:Οβontoβπ΄) |
6 | | fof 5438 |
. . . . . . . . . . 11
β’ (π:Οβontoβπ΄ β π:ΟβΆπ΄) |
7 | 5, 6 | syl 14 |
. . . . . . . . . 10
β’
((((βπ₯ π₯ β π΄ β§ π:Οβontoβπ΄) β§ π β Ο) β§ Β¬ π = β
) β π:ΟβΆπ΄) |
8 | | nnpredcl 4622 |
. . . . . . . . . . 11
β’ (π β Ο β βͺ π
β Ο) |
9 | 8 | ad2antlr 489 |
. . . . . . . . . 10
β’
((((βπ₯ π₯ β π΄ β§ π:Οβontoβπ΄) β§ π β Ο) β§ Β¬ π = β
) β βͺ π
β Ο) |
10 | 7, 9 | ffvelcdmd 5652 |
. . . . . . . . 9
β’
((((βπ₯ π₯ β π΄ β§ π:Οβontoβπ΄) β§ π β Ο) β§ Β¬ π = β
) β (πββͺ π)
β π΄) |
11 | | djulcl 7049 |
. . . . . . . . 9
β’ ((πββͺ π)
β π΄ β
(inlβ(πββͺ π))
β (π΄ β
1o)) |
12 | 10, 11 | syl 14 |
. . . . . . . 8
β’
((((βπ₯ π₯ β π΄ β§ π:Οβontoβπ΄) β§ π β Ο) β§ Β¬ π = β
) β
(inlβ(πββͺ π))
β (π΄ β
1o)) |
13 | | nndceq0 4617 |
. . . . . . . . 9
β’ (π β Ο β
DECID π =
β
) |
14 | 13 | adantl 277 |
. . . . . . . 8
β’
(((βπ₯ π₯ β π΄ β§ π:Οβontoβπ΄) β§ π β Ο) β DECID
π =
β
) |
15 | 4, 12, 14 | ifcldadc 3563 |
. . . . . . 7
β’
(((βπ₯ π₯ β π΄ β§ π:Οβontoβπ΄) β§ π β Ο) β if(π = β
, (inrββ
),
(inlβ(πββͺ π)))
β (π΄ β
1o)) |
16 | 15 | fmpttd 5671 |
. . . . . 6
β’
((βπ₯ π₯ β π΄ β§ π:Οβontoβπ΄) β (π β Ο β¦ if(π = β
, (inrββ
),
(inlβ(πββͺ π)))):ΟβΆ(π΄ β 1o)) |
17 | | simpllr 534 |
. . . . . . . . . . 11
β’
((((βπ₯ π₯ β π΄ β§ π:Οβontoβπ΄) β§ π¦ β (π΄ β 1o)) β§ (π€ β π΄ β§ π¦ = (inlβπ€))) β π:Οβontoβπ΄) |
18 | | simprl 529 |
. . . . . . . . . . 11
β’
((((βπ₯ π₯ β π΄ β§ π:Οβontoβπ΄) β§ π¦ β (π΄ β 1o)) β§ (π€ β π΄ β§ π¦ = (inlβπ€))) β π€ β π΄) |
19 | | foelrn 5753 |
. . . . . . . . . . 11
β’ ((π:Οβontoβπ΄ β§ π€ β π΄) β βπ’ β Ο π€ = (πβπ’)) |
20 | 17, 18, 19 | syl2anc 411 |
. . . . . . . . . 10
β’
((((βπ₯ π₯ β π΄ β§ π:Οβontoβπ΄) β§ π¦ β (π΄ β 1o)) β§ (π€ β π΄ β§ π¦ = (inlβπ€))) β βπ’ β Ο π€ = (πβπ’)) |
21 | | peano2 4594 |
. . . . . . . . . . . 12
β’ (π’ β Ο β suc π’ β
Ο) |
22 | 21 | ad2antrl 490 |
. . . . . . . . . . 11
β’
(((((βπ₯ π₯ β π΄ β§ π:Οβontoβπ΄) β§ π¦ β (π΄ β 1o)) β§ (π€ β π΄ β§ π¦ = (inlβπ€))) β§ (π’ β Ο β§ π€ = (πβπ’))) β suc π’ β Ο) |
23 | | simplrr 536 |
. . . . . . . . . . . . . 14
β’
(((((βπ₯ π₯ β π΄ β§ π:Οβontoβπ΄) β§ π¦ β (π΄ β 1o)) β§ (π€ β π΄ β§ π¦ = (inlβπ€))) β§ (π’ β Ο β§ π€ = (πβπ’))) β π¦ = (inlβπ€)) |
24 | | simprl 529 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((βπ₯ π₯ β π΄ β§ π:Οβontoβπ΄) β§ π¦ β (π΄ β 1o)) β§ (π€ β π΄ β§ π¦ = (inlβπ€))) β§ (π’ β Ο β§ π€ = (πβπ’))) β π’ β Ο) |
25 | | nnord 4611 |
. . . . . . . . . . . . . . . . . . 19
β’ (π’ β Ο β Ord π’) |
26 | | ordtr 4378 |
. . . . . . . . . . . . . . . . . . 19
β’ (Ord
π’ β Tr π’) |
27 | 24, 25, 26 | 3syl 17 |
. . . . . . . . . . . . . . . . . 18
β’
(((((βπ₯ π₯ β π΄ β§ π:Οβontoβπ΄) β§ π¦ β (π΄ β 1o)) β§ (π€ β π΄ β§ π¦ = (inlβπ€))) β§ (π’ β Ο β§ π€ = (πβπ’))) β Tr π’) |
28 | | unisucg 4414 |
. . . . . . . . . . . . . . . . . . 19
β’ (π’ β Ο β (Tr π’ β βͺ suc π’ = π’)) |
29 | 28 | ad2antrl 490 |
. . . . . . . . . . . . . . . . . 18
β’
(((((βπ₯ π₯ β π΄ β§ π:Οβontoβπ΄) β§ π¦ β (π΄ β 1o)) β§ (π€ β π΄ β§ π¦ = (inlβπ€))) β§ (π’ β Ο β§ π€ = (πβπ’))) β (Tr π’ β βͺ suc
π’ = π’)) |
30 | 27, 29 | mpbid 147 |
. . . . . . . . . . . . . . . . 17
β’
(((((βπ₯ π₯ β π΄ β§ π:Οβontoβπ΄) β§ π¦ β (π΄ β 1o)) β§ (π€ β π΄ β§ π¦ = (inlβπ€))) β§ (π’ β Ο β§ π€ = (πβπ’))) β βͺ suc
π’ = π’) |
31 | 30 | fveq2d 5519 |
. . . . . . . . . . . . . . . 16
β’
(((((βπ₯ π₯ β π΄ β§ π:Οβontoβπ΄) β§ π¦ β (π΄ β 1o)) β§ (π€ β π΄ β§ π¦ = (inlβπ€))) β§ (π’ β Ο β§ π€ = (πβπ’))) β (πββͺ suc π’) = (πβπ’)) |
32 | | simprr 531 |
. . . . . . . . . . . . . . . 16
β’
(((((βπ₯ π₯ β π΄ β§ π:Οβontoβπ΄) β§ π¦ β (π΄ β 1o)) β§ (π€ β π΄ β§ π¦ = (inlβπ€))) β§ (π’ β Ο β§ π€ = (πβπ’))) β π€ = (πβπ’)) |
33 | 31, 32 | eqtr4d 2213 |
. . . . . . . . . . . . . . 15
β’
(((((βπ₯ π₯ β π΄ β§ π:Οβontoβπ΄) β§ π¦ β (π΄ β 1o)) β§ (π€ β π΄ β§ π¦ = (inlβπ€))) β§ (π’ β Ο β§ π€ = (πβπ’))) β (πββͺ suc π’) = π€) |
34 | 33 | fveq2d 5519 |
. . . . . . . . . . . . . 14
β’
(((((βπ₯ π₯ β π΄ β§ π:Οβontoβπ΄) β§ π¦ β (π΄ β 1o)) β§ (π€ β π΄ β§ π¦ = (inlβπ€))) β§ (π’ β Ο β§ π€ = (πβπ’))) β (inlβ(πββͺ suc π’)) = (inlβπ€)) |
35 | 23, 34 | eqtr4d 2213 |
. . . . . . . . . . . . 13
β’
(((((βπ₯ π₯ β π΄ β§ π:Οβontoβπ΄) β§ π¦ β (π΄ β 1o)) β§ (π€ β π΄ β§ π¦ = (inlβπ€))) β§ (π’ β Ο β§ π€ = (πβπ’))) β π¦ = (inlβ(πββͺ suc π’))) |
36 | | peano3 4595 |
. . . . . . . . . . . . . . . 16
β’ (π’ β Ο β suc π’ β β
) |
37 | 36 | neneqd 2368 |
. . . . . . . . . . . . . . 15
β’ (π’ β Ο β Β¬ suc
π’ =
β
) |
38 | 37 | ad2antrl 490 |
. . . . . . . . . . . . . 14
β’
(((((βπ₯ π₯ β π΄ β§ π:Οβontoβπ΄) β§ π¦ β (π΄ β 1o)) β§ (π€ β π΄ β§ π¦ = (inlβπ€))) β§ (π’ β Ο β§ π€ = (πβπ’))) β Β¬ suc π’ = β
) |
39 | 38 | iffalsed 3544 |
. . . . . . . . . . . . 13
β’
(((((βπ₯ π₯ β π΄ β§ π:Οβontoβπ΄) β§ π¦ β (π΄ β 1o)) β§ (π€ β π΄ β§ π¦ = (inlβπ€))) β§ (π’ β Ο β§ π€ = (πβπ’))) β if(suc π’ = β
, (inrββ
),
(inlβ(πββͺ suc π’))) = (inlβ(πββͺ suc π’))) |
40 | 35, 39 | eqtr4d 2213 |
. . . . . . . . . . . 12
β’
(((((βπ₯ π₯ β π΄ β§ π:Οβontoβπ΄) β§ π¦ β (π΄ β 1o)) β§ (π€ β π΄ β§ π¦ = (inlβπ€))) β§ (π’ β Ο β§ π€ = (πβπ’))) β π¦ = if(suc π’ = β
, (inrββ
),
(inlβ(πββͺ suc π’)))) |
41 | | eqid 2177 |
. . . . . . . . . . . . 13
β’ (π β Ο β¦ if(π = β
, (inrββ
),
(inlβ(πββͺ π)))) = (π β Ο β¦ if(π = β
, (inrββ
),
(inlβ(πββͺ π)))) |
42 | | eqeq1 2184 |
. . . . . . . . . . . . . 14
β’ (π = suc π’ β (π = β
β suc π’ = β
)) |
43 | | unieq 3818 |
. . . . . . . . . . . . . . . 16
β’ (π = suc π’ β βͺ π = βͺ
suc π’) |
44 | 43 | fveq2d 5519 |
. . . . . . . . . . . . . . 15
β’ (π = suc π’ β (πββͺ π) = (πββͺ suc π’)) |
45 | 44 | fveq2d 5519 |
. . . . . . . . . . . . . 14
β’ (π = suc π’ β (inlβ(πββͺ π)) = (inlβ(πββͺ suc π’))) |
46 | 42, 45 | ifbieq2d 3558 |
. . . . . . . . . . . . 13
β’ (π = suc π’ β if(π = β
, (inrββ
),
(inlβ(πββͺ π)))
= if(suc π’ = β
,
(inrββ
), (inlβ(πββͺ suc π’)))) |
47 | | simpllr 534 |
. . . . . . . . . . . . . 14
β’
(((((βπ₯ π₯ β π΄ β§ π:Οβontoβπ΄) β§ π¦ β (π΄ β 1o)) β§ (π€ β π΄ β§ π¦ = (inlβπ€))) β§ (π’ β Ο β§ π€ = (πβπ’))) β π¦ β (π΄ β 1o)) |
48 | 40, 47 | eqeltrrd 2255 |
. . . . . . . . . . . . 13
β’
(((((βπ₯ π₯ β π΄ β§ π:Οβontoβπ΄) β§ π¦ β (π΄ β 1o)) β§ (π€ β π΄ β§ π¦ = (inlβπ€))) β§ (π’ β Ο β§ π€ = (πβπ’))) β if(suc π’ = β
, (inrββ
),
(inlβ(πββͺ suc π’))) β (π΄ β 1o)) |
49 | 41, 46, 22, 48 | fvmptd3 5609 |
. . . . . . . . . . . 12
β’
(((((βπ₯ π₯ β π΄ β§ π:Οβontoβπ΄) β§ π¦ β (π΄ β 1o)) β§ (π€ β π΄ β§ π¦ = (inlβπ€))) β§ (π’ β Ο β§ π€ = (πβπ’))) β ((π β Ο β¦ if(π = β
, (inrββ
),
(inlβ(πββͺ π))))βsuc π’) = if(suc π’ = β
, (inrββ
),
(inlβ(πββͺ suc π’)))) |
50 | 40, 49 | eqtr4d 2213 |
. . . . . . . . . . 11
β’
(((((βπ₯ π₯ β π΄ β§ π:Οβontoβπ΄) β§ π¦ β (π΄ β 1o)) β§ (π€ β π΄ β§ π¦ = (inlβπ€))) β§ (π’ β Ο β§ π€ = (πβπ’))) β π¦ = ((π β Ο β¦ if(π = β
, (inrββ
),
(inlβ(πββͺ π))))βsuc π’)) |
51 | | fveq2 5515 |
. . . . . . . . . . . 12
β’ (π§ = suc π’ β ((π β Ο β¦ if(π = β
, (inrββ
),
(inlβ(πββͺ π))))βπ§) = ((π β Ο β¦ if(π = β
, (inrββ
),
(inlβ(πββͺ π))))βsuc π’)) |
52 | 51 | rspceeqv 2859 |
. . . . . . . . . . 11
β’ ((suc
π’ β Ο β§
π¦ = ((π β Ο β¦ if(π = β
, (inrββ
),
(inlβ(πββͺ π))))βsuc π’)) β βπ§ β Ο π¦ = ((π β Ο β¦ if(π = β
, (inrββ
),
(inlβ(πββͺ π))))βπ§)) |
53 | 22, 50, 52 | syl2anc 411 |
. . . . . . . . . 10
β’
(((((βπ₯ π₯ β π΄ β§ π:Οβontoβπ΄) β§ π¦ β (π΄ β 1o)) β§ (π€ β π΄ β§ π¦ = (inlβπ€))) β§ (π’ β Ο β§ π€ = (πβπ’))) β βπ§ β Ο π¦ = ((π β Ο β¦ if(π = β
, (inrββ
),
(inlβ(πββͺ π))))βπ§)) |
54 | 20, 53 | rexlimddv 2599 |
. . . . . . . . 9
β’
((((βπ₯ π₯ β π΄ β§ π:Οβontoβπ΄) β§ π¦ β (π΄ β 1o)) β§ (π€ β π΄ β§ π¦ = (inlβπ€))) β βπ§ β Ο π¦ = ((π β Ο β¦ if(π = β
, (inrββ
),
(inlβ(πββͺ π))))βπ§)) |
55 | 54 | rexlimdvaa 2595 |
. . . . . . . 8
β’
(((βπ₯ π₯ β π΄ β§ π:Οβontoβπ΄) β§ π¦ β (π΄ β 1o)) β
(βπ€ β π΄ π¦ = (inlβπ€) β βπ§ β Ο π¦ = ((π β Ο β¦ if(π = β
, (inrββ
),
(inlβ(πββͺ π))))βπ§))) |
56 | | peano1 4593 |
. . . . . . . . . 10
β’ β
β Ο |
57 | | simprr 531 |
. . . . . . . . . . . . 13
β’
((((βπ₯ π₯ β π΄ β§ π:Οβontoβπ΄) β§ π¦ β (π΄ β 1o)) β§ (π€ β 1o β§
π¦ = (inrβπ€))) β π¦ = (inrβπ€)) |
58 | | simprl 529 |
. . . . . . . . . . . . . . 15
β’
((((βπ₯ π₯ β π΄ β§ π:Οβontoβπ΄) β§ π¦ β (π΄ β 1o)) β§ (π€ β 1o β§
π¦ = (inrβπ€))) β π€ β 1o) |
59 | | el1o 6437 |
. . . . . . . . . . . . . . 15
β’ (π€ β 1o β
π€ =
β
) |
60 | 58, 59 | sylib 122 |
. . . . . . . . . . . . . 14
β’
((((βπ₯ π₯ β π΄ β§ π:Οβontoβπ΄) β§ π¦ β (π΄ β 1o)) β§ (π€ β 1o β§
π¦ = (inrβπ€))) β π€ = β
) |
61 | 60 | fveq2d 5519 |
. . . . . . . . . . . . 13
β’
((((βπ₯ π₯ β π΄ β§ π:Οβontoβπ΄) β§ π¦ β (π΄ β 1o)) β§ (π€ β 1o β§
π¦ = (inrβπ€))) β (inrβπ€) =
(inrββ
)) |
62 | 57, 61 | eqtrd 2210 |
. . . . . . . . . . . 12
β’
((((βπ₯ π₯ β π΄ β§ π:Οβontoβπ΄) β§ π¦ β (π΄ β 1o)) β§ (π€ β 1o β§
π¦ = (inrβπ€))) β π¦ = (inrββ
)) |
63 | | eqid 2177 |
. . . . . . . . . . . . 13
β’ β
=
β
|
64 | 63 | iftruei 3540 |
. . . . . . . . . . . 12
β’
if(β
= β
, (inrββ
), (inlβ(πββͺ β
))) = (inrββ
) |
65 | 62, 64 | eqtr4di 2228 |
. . . . . . . . . . 11
β’
((((βπ₯ π₯ β π΄ β§ π:Οβontoβπ΄) β§ π¦ β (π΄ β 1o)) β§ (π€ β 1o β§
π¦ = (inrβπ€))) β π¦ = if(β
= β
, (inrββ
),
(inlβ(πββͺ β
)))) |
66 | 64, 3 | eqeltri 2250 |
. . . . . . . . . . . . 13
β’
if(β
= β
, (inrββ
), (inlβ(πββͺ β
))) β (π΄ β 1o) |
67 | 66 | a1i 9 |
. . . . . . . . . . . 12
β’
((((βπ₯ π₯ β π΄ β§ π:Οβontoβπ΄) β§ π¦ β (π΄ β 1o)) β§ (π€ β 1o β§
π¦ = (inrβπ€))) β if(β
= β
,
(inrββ
), (inlβ(πββͺ
β
))) β (π΄
β 1o)) |
68 | | eqeq1 2184 |
. . . . . . . . . . . . . 14
β’ (π = β
β (π = β
β β
=
β
)) |
69 | | unieq 3818 |
. . . . . . . . . . . . . . . 16
β’ (π = β
β βͺ π =
βͺ β
) |
70 | 69 | fveq2d 5519 |
. . . . . . . . . . . . . . 15
β’ (π = β
β (πββͺ π) =
(πββͺ β
)) |
71 | 70 | fveq2d 5519 |
. . . . . . . . . . . . . 14
β’ (π = β
β
(inlβ(πββͺ π))
= (inlβ(πββͺ β
))) |
72 | 68, 71 | ifbieq2d 3558 |
. . . . . . . . . . . . 13
β’ (π = β
β if(π = β
, (inrββ
),
(inlβ(πββͺ π)))
= if(β
= β
, (inrββ
), (inlβ(πββͺ
β
)))) |
73 | 72, 41 | fvmptg 5592 |
. . . . . . . . . . . 12
β’ ((β
β Ο β§ if(β
= β
, (inrββ
),
(inlβ(πββͺ β
))) β (π΄ β 1o)) β ((π β Ο β¦ if(π = β
, (inrββ
),
(inlβ(πββͺ π))))ββ
) = if(β
= β
,
(inrββ
), (inlβ(πββͺ
β
)))) |
74 | 56, 67, 73 | sylancr 414 |
. . . . . . . . . . 11
β’
((((βπ₯ π₯ β π΄ β§ π:Οβontoβπ΄) β§ π¦ β (π΄ β 1o)) β§ (π€ β 1o β§
π¦ = (inrβπ€))) β ((π β Ο β¦ if(π = β
, (inrββ
),
(inlβ(πββͺ π))))ββ
) = if(β
= β
,
(inrββ
), (inlβ(πββͺ
β
)))) |
75 | 65, 74 | eqtr4d 2213 |
. . . . . . . . . 10
β’
((((βπ₯ π₯ β π΄ β§ π:Οβontoβπ΄) β§ π¦ β (π΄ β 1o)) β§ (π€ β 1o β§
π¦ = (inrβπ€))) β π¦ = ((π β Ο β¦ if(π = β
, (inrββ
),
(inlβ(πββͺ π))))ββ
)) |
76 | | fveq2 5515 |
. . . . . . . . . . 11
β’ (π§ = β
β ((π β Ο β¦ if(π = β
, (inrββ
),
(inlβ(πββͺ π))))βπ§) = ((π β Ο β¦ if(π = β
, (inrββ
),
(inlβ(πββͺ π))))ββ
)) |
77 | 76 | rspceeqv 2859 |
. . . . . . . . . 10
β’ ((β
β Ο β§ π¦ =
((π β Ο β¦
if(π = β
,
(inrββ
), (inlβ(πββͺ π))))ββ
)) β
βπ§ β Ο
π¦ = ((π β Ο β¦ if(π = β
, (inrββ
),
(inlβ(πββͺ π))))βπ§)) |
78 | 56, 75, 77 | sylancr 414 |
. . . . . . . . 9
β’
((((βπ₯ π₯ β π΄ β§ π:Οβontoβπ΄) β§ π¦ β (π΄ β 1o)) β§ (π€ β 1o β§
π¦ = (inrβπ€))) β βπ§ β Ο π¦ = ((π β Ο β¦ if(π = β
, (inrββ
),
(inlβ(πββͺ π))))βπ§)) |
79 | 78 | rexlimdvaa 2595 |
. . . . . . . 8
β’
(((βπ₯ π₯ β π΄ β§ π:Οβontoβπ΄) β§ π¦ β (π΄ β 1o)) β
(βπ€ β
1o π¦ =
(inrβπ€) β
βπ§ β Ο
π¦ = ((π β Ο β¦ if(π = β
, (inrββ
),
(inlβ(πββͺ π))))βπ§))) |
80 | | djur 7067 |
. . . . . . . . . 10
β’ (π¦ β (π΄ β 1o) β
(βπ€ β π΄ π¦ = (inlβπ€) β¨ βπ€ β 1o π¦ = (inrβπ€))) |
81 | 80 | biimpi 120 |
. . . . . . . . 9
β’ (π¦ β (π΄ β 1o) β
(βπ€ β π΄ π¦ = (inlβπ€) β¨ βπ€ β 1o π¦ = (inrβπ€))) |
82 | 81 | adantl 277 |
. . . . . . . 8
β’
(((βπ₯ π₯ β π΄ β§ π:Οβontoβπ΄) β§ π¦ β (π΄ β 1o)) β
(βπ€ β π΄ π¦ = (inlβπ€) β¨ βπ€ β 1o π¦ = (inrβπ€))) |
83 | 55, 79, 82 | mpjaod 718 |
. . . . . . 7
β’
(((βπ₯ π₯ β π΄ β§ π:Οβontoβπ΄) β§ π¦ β (π΄ β 1o)) β
βπ§ β Ο
π¦ = ((π β Ο β¦ if(π = β
, (inrββ
),
(inlβ(πββͺ π))))βπ§)) |
84 | 83 | ralrimiva 2550 |
. . . . . 6
β’
((βπ₯ π₯ β π΄ β§ π:Οβontoβπ΄) β βπ¦ β (π΄ β 1o)βπ§ β Ο π¦ = ((π β Ο β¦ if(π = β
, (inrββ
),
(inlβ(πββͺ π))))βπ§)) |
85 | | dffo3 5663 |
. . . . . 6
β’ ((π β Ο β¦ if(π = β
, (inrββ
),
(inlβ(πββͺ π)))):Οβontoβ(π΄ β 1o) β ((π β Ο β¦ if(π = β
, (inrββ
),
(inlβ(πββͺ π)))):ΟβΆ(π΄ β 1o) β§ βπ¦ β (π΄ β 1o)βπ§ β Ο π¦ = ((π β Ο β¦ if(π = β
, (inrββ
),
(inlβ(πββͺ π))))βπ§))) |
86 | 16, 84, 85 | sylanbrc 417 |
. . . . 5
β’
((βπ₯ π₯ β π΄ β§ π:Οβontoβπ΄) β (π β Ο β¦ if(π = β
, (inrββ
),
(inlβ(πββͺ π)))):Οβontoβ(π΄ β 1o)) |
87 | | omex 4592 |
. . . . . . 7
β’ Ο
β V |
88 | 87 | mptex 5742 |
. . . . . 6
β’ (π β Ο β¦ if(π = β
, (inrββ
),
(inlβ(πββͺ π)))) β V |
89 | | foeq1 5434 |
. . . . . 6
β’ (π = (π β Ο β¦ if(π = β
, (inrββ
),
(inlβ(πββͺ π)))) β (π:Οβontoβ(π΄ β 1o) β (π β Ο β¦ if(π = β
, (inrββ
),
(inlβ(πββͺ π)))):Οβontoβ(π΄ β 1o))) |
90 | 88, 89 | spcev 2832 |
. . . . 5
β’ ((π β Ο β¦ if(π = β
, (inrββ
),
(inlβ(πββͺ π)))):Οβontoβ(π΄ β 1o) β βπ π:Οβontoβ(π΄ β 1o)) |
91 | 86, 90 | syl 14 |
. . . 4
β’
((βπ₯ π₯ β π΄ β§ π:Οβontoβπ΄) β βπ π:Οβontoβ(π΄ β 1o)) |
92 | 91 | ex 115 |
. . 3
β’
(βπ₯ π₯ β π΄ β (π:Οβontoβπ΄ β βπ π:Οβontoβ(π΄ β 1o))) |
93 | 92 | exlimdv 1819 |
. 2
β’
(βπ₯ π₯ β π΄ β (βπ π:Οβontoβπ΄ β βπ π:Οβontoβ(π΄ β 1o))) |
94 | | foeq1 5434 |
. . 3
β’ (π = π β (π:Οβontoβ(π΄ β 1o) β π:Οβontoβ(π΄ β 1o))) |
95 | 94 | cbvexv 1918 |
. 2
β’
(βπ π:Οβontoβ(π΄ β 1o) β βπ π:Οβontoβ(π΄ β 1o)) |
96 | 93, 95 | imbitrrdi 162 |
1
β’
(βπ₯ π₯ β π΄ β (βπ π:Οβontoβπ΄ β βπ π:Οβontoβ(π΄ β 1o))) |