Step | Hyp | Ref
| Expression |
1 | | f1oi 5499 |
. . . . . . . . . . 11
β’ ( I
βΎ π΄):π΄β1-1-ontoβπ΄ |
2 | | f1of 5461 |
. . . . . . . . . . 11
β’ (( I
βΎ π΄):π΄β1-1-ontoβπ΄ β ( I βΎ π΄):π΄βΆπ΄) |
3 | 1, 2 | mp1i 10 |
. . . . . . . . . 10
β’ ((π₯ β π΄ β§ π:Οβontoβ(π΄ β 1o)) β ( I βΎ
π΄):π΄βΆπ΄) |
4 | | fconst6g 5414 |
. . . . . . . . . . 11
β’ (π₯ β π΄ β (1o Γ {π₯}):1oβΆπ΄) |
5 | 4 | adantr 276 |
. . . . . . . . . 10
β’ ((π₯ β π΄ β§ π:Οβontoβ(π΄ β 1o)) β
(1o Γ {π₯}):1oβΆπ΄) |
6 | 3, 5 | casef 7086 |
. . . . . . . . 9
β’ ((π₯ β π΄ β§ π:Οβontoβ(π΄ β 1o)) β case(( I
βΎ π΄), (1o
Γ {π₯})):(π΄ β
1o)βΆπ΄) |
7 | | ffun 5368 |
. . . . . . . . 9
β’ (case(( I
βΎ π΄), (1o
Γ {π₯})):(π΄ β
1o)βΆπ΄
β Fun case(( I βΎ π΄), (1o Γ {π₯}))) |
8 | 6, 7 | syl 14 |
. . . . . . . 8
β’ ((π₯ β π΄ β§ π:Οβontoβ(π΄ β 1o)) β Fun case((
I βΎ π΄),
(1o Γ {π₯}))) |
9 | | vex 2740 |
. . . . . . . . 9
β’ π β V |
10 | 9 | a1i 9 |
. . . . . . . 8
β’ ((π₯ β π΄ β§ π:Οβontoβ(π΄ β 1o)) β π β V) |
11 | | cofunexg 6109 |
. . . . . . . 8
β’ ((Fun
case(( I βΎ π΄),
(1o Γ {π₯})) β§ π β V) β (case(( I βΎ π΄), (1o Γ {π₯})) β π) β V) |
12 | 8, 10, 11 | syl2anc 411 |
. . . . . . 7
β’ ((π₯ β π΄ β§ π:Οβontoβ(π΄ β 1o)) β (case(( I
βΎ π΄), (1o
Γ {π₯})) β π) β V) |
13 | | fof 5438 |
. . . . . . . . . 10
β’ (π:Οβontoβ(π΄ β 1o) β π:ΟβΆ(π΄ β
1o)) |
14 | 13 | adantl 277 |
. . . . . . . . 9
β’ ((π₯ β π΄ β§ π:Οβontoβ(π΄ β 1o)) β π:ΟβΆ(π΄ β
1o)) |
15 | | fco 5381 |
. . . . . . . . 9
β’ ((case((
I βΎ π΄),
(1o Γ {π₯})):(π΄ β 1o)βΆπ΄ β§ π:ΟβΆ(π΄ β 1o)) β (case(( I
βΎ π΄), (1o
Γ {π₯})) β π):ΟβΆπ΄) |
16 | 6, 14, 15 | syl2anc 411 |
. . . . . . . 8
β’ ((π₯ β π΄ β§ π:Οβontoβ(π΄ β 1o)) β (case(( I
βΎ π΄), (1o
Γ {π₯})) β π):ΟβΆπ΄) |
17 | | simplr 528 |
. . . . . . . . . . 11
β’ (((π₯ β π΄ β§ π:Οβontoβ(π΄ β 1o)) β§ π¦ β π΄) β π:Οβontoβ(π΄ β 1o)) |
18 | | djulcl 7049 |
. . . . . . . . . . . 12
β’ (π¦ β π΄ β (inlβπ¦) β (π΄ β 1o)) |
19 | 18 | adantl 277 |
. . . . . . . . . . 11
β’ (((π₯ β π΄ β§ π:Οβontoβ(π΄ β 1o)) β§ π¦ β π΄) β (inlβπ¦) β (π΄ β 1o)) |
20 | | foelrn 5753 |
. . . . . . . . . . 11
β’ ((π:Οβontoβ(π΄ β 1o) β§
(inlβπ¦) β (π΄ β 1o)) β
βπ§ β Ο
(inlβπ¦) = (πβπ§)) |
21 | 17, 19, 20 | syl2anc 411 |
. . . . . . . . . 10
β’ (((π₯ β π΄ β§ π:Οβontoβ(π΄ β 1o)) β§ π¦ β π΄) β βπ§ β Ο (inlβπ¦) = (πβπ§)) |
22 | | fofn 5440 |
. . . . . . . . . . . . . . . 16
β’ (π:Οβontoβ(π΄ β 1o) β π Fn Ο) |
23 | 22 | ad4antlr 495 |
. . . . . . . . . . . . . . 15
β’
(((((π₯ β π΄ β§ π:Οβontoβ(π΄ β 1o)) β§ π¦ β π΄) β§ π§ β Ο) β§ (inlβπ¦) = (πβπ§)) β π Fn Ο) |
24 | | simplr 528 |
. . . . . . . . . . . . . . 15
β’
(((((π₯ β π΄ β§ π:Οβontoβ(π΄ β 1o)) β§ π¦ β π΄) β§ π§ β Ο) β§ (inlβπ¦) = (πβπ§)) β π§ β Ο) |
25 | | fvco2 5585 |
. . . . . . . . . . . . . . 15
β’ ((π Fn Ο β§ π§ β Ο) β ((case((
I βΎ π΄),
(1o Γ {π₯})) β π)βπ§) = (case(( I βΎ π΄), (1o Γ {π₯}))β(πβπ§))) |
26 | 23, 24, 25 | syl2anc 411 |
. . . . . . . . . . . . . 14
β’
(((((π₯ β π΄ β§ π:Οβontoβ(π΄ β 1o)) β§ π¦ β π΄) β§ π§ β Ο) β§ (inlβπ¦) = (πβπ§)) β ((case(( I βΎ π΄), (1o Γ {π₯})) β π)βπ§) = (case(( I βΎ π΄), (1o Γ {π₯}))β(πβπ§))) |
27 | | simpr 110 |
. . . . . . . . . . . . . . 15
β’
(((((π₯ β π΄ β§ π:Οβontoβ(π΄ β 1o)) β§ π¦ β π΄) β§ π§ β Ο) β§ (inlβπ¦) = (πβπ§)) β (inlβπ¦) = (πβπ§)) |
28 | 27 | fveq2d 5519 |
. . . . . . . . . . . . . 14
β’
(((((π₯ β π΄ β§ π:Οβontoβ(π΄ β 1o)) β§ π¦ β π΄) β§ π§ β Ο) β§ (inlβπ¦) = (πβπ§)) β (case(( I βΎ π΄), (1o Γ {π₯}))β(inlβπ¦)) = (case(( I βΎ π΄), (1o Γ {π₯}))β(πβπ§))) |
29 | | fnresi 5333 |
. . . . . . . . . . . . . . . 16
β’ ( I
βΎ π΄) Fn π΄ |
30 | 29 | a1i 9 |
. . . . . . . . . . . . . . 15
β’
(((((π₯ β π΄ β§ π:Οβontoβ(π΄ β 1o)) β§ π¦ β π΄) β§ π§ β Ο) β§ (inlβπ¦) = (πβπ§)) β ( I βΎ π΄) Fn π΄) |
31 | | vex 2740 |
. . . . . . . . . . . . . . . . 17
β’ π₯ β V |
32 | 31 | fconst6 5415 |
. . . . . . . . . . . . . . . 16
β’
(1o Γ {π₯}):1oβΆV |
33 | | ffun 5368 |
. . . . . . . . . . . . . . . 16
β’
((1o Γ {π₯}):1oβΆV β Fun
(1o Γ {π₯})) |
34 | 32, 33 | mp1i 10 |
. . . . . . . . . . . . . . 15
β’
(((((π₯ β π΄ β§ π:Οβontoβ(π΄ β 1o)) β§ π¦ β π΄) β§ π§ β Ο) β§ (inlβπ¦) = (πβπ§)) β Fun (1o Γ {π₯})) |
35 | | simpllr 534 |
. . . . . . . . . . . . . . 15
β’
(((((π₯ β π΄ β§ π:Οβontoβ(π΄ β 1o)) β§ π¦ β π΄) β§ π§ β Ο) β§ (inlβπ¦) = (πβπ§)) β π¦ β π΄) |
36 | 30, 34, 35 | caseinl 7089 |
. . . . . . . . . . . . . 14
β’
(((((π₯ β π΄ β§ π:Οβontoβ(π΄ β 1o)) β§ π¦ β π΄) β§ π§ β Ο) β§ (inlβπ¦) = (πβπ§)) β (case(( I βΎ π΄), (1o Γ {π₯}))β(inlβπ¦)) = (( I βΎ π΄)βπ¦)) |
37 | 26, 28, 36 | 3eqtr2d 2216 |
. . . . . . . . . . . . 13
β’
(((((π₯ β π΄ β§ π:Οβontoβ(π΄ β 1o)) β§ π¦ β π΄) β§ π§ β Ο) β§ (inlβπ¦) = (πβπ§)) β ((case(( I βΎ π΄), (1o Γ {π₯})) β π)βπ§) = (( I βΎ π΄)βπ¦)) |
38 | | fvresi 5709 |
. . . . . . . . . . . . . 14
β’ (π¦ β π΄ β (( I βΎ π΄)βπ¦) = π¦) |
39 | 35, 38 | syl 14 |
. . . . . . . . . . . . 13
β’
(((((π₯ β π΄ β§ π:Οβontoβ(π΄ β 1o)) β§ π¦ β π΄) β§ π§ β Ο) β§ (inlβπ¦) = (πβπ§)) β (( I βΎ π΄)βπ¦) = π¦) |
40 | 37, 39 | eqtr2d 2211 |
. . . . . . . . . . . 12
β’
(((((π₯ β π΄ β§ π:Οβontoβ(π΄ β 1o)) β§ π¦ β π΄) β§ π§ β Ο) β§ (inlβπ¦) = (πβπ§)) β π¦ = ((case(( I βΎ π΄), (1o Γ {π₯})) β π)βπ§)) |
41 | 40 | ex 115 |
. . . . . . . . . . 11
β’ ((((π₯ β π΄ β§ π:Οβontoβ(π΄ β 1o)) β§ π¦ β π΄) β§ π§ β Ο) β ((inlβπ¦) = (πβπ§) β π¦ = ((case(( I βΎ π΄), (1o Γ {π₯})) β π)βπ§))) |
42 | 41 | reximdva 2579 |
. . . . . . . . . 10
β’ (((π₯ β π΄ β§ π:Οβontoβ(π΄ β 1o)) β§ π¦ β π΄) β (βπ§ β Ο (inlβπ¦) = (πβπ§) β βπ§ β Ο π¦ = ((case(( I βΎ π΄), (1o Γ {π₯})) β π)βπ§))) |
43 | 21, 42 | mpd 13 |
. . . . . . . . 9
β’ (((π₯ β π΄ β§ π:Οβontoβ(π΄ β 1o)) β§ π¦ β π΄) β βπ§ β Ο π¦ = ((case(( I βΎ π΄), (1o Γ {π₯})) β π)βπ§)) |
44 | 43 | ralrimiva 2550 |
. . . . . . . 8
β’ ((π₯ β π΄ β§ π:Οβontoβ(π΄ β 1o)) β
βπ¦ β π΄ βπ§ β Ο π¦ = ((case(( I βΎ π΄), (1o Γ {π₯})) β π)βπ§)) |
45 | | dffo3 5663 |
. . . . . . . 8
β’ ((case((
I βΎ π΄),
(1o Γ {π₯})) β π):Οβontoβπ΄ β ((case(( I βΎ π΄), (1o Γ {π₯})) β π):ΟβΆπ΄ β§ βπ¦ β π΄ βπ§ β Ο π¦ = ((case(( I βΎ π΄), (1o Γ {π₯})) β π)βπ§))) |
46 | 16, 44, 45 | sylanbrc 417 |
. . . . . . 7
β’ ((π₯ β π΄ β§ π:Οβontoβ(π΄ β 1o)) β (case(( I
βΎ π΄), (1o
Γ {π₯})) β π):Οβontoβπ΄) |
47 | | foeq1 5434 |
. . . . . . . 8
β’ (π = (case(( I βΎ π΄), (1o Γ {π₯})) β π) β (π:Οβontoβπ΄ β (case(( I βΎ π΄), (1o Γ {π₯})) β π):Οβontoβπ΄)) |
48 | 47 | spcegv 2825 |
. . . . . . 7
β’ ((case((
I βΎ π΄),
(1o Γ {π₯})) β π) β V β ((case(( I βΎ π΄), (1o Γ {π₯})) β π):Οβontoβπ΄ β βπ π:Οβontoβπ΄)) |
49 | 12, 46, 48 | sylc 62 |
. . . . . 6
β’ ((π₯ β π΄ β§ π:Οβontoβ(π΄ β 1o)) β
βπ π:Οβontoβπ΄) |
50 | 49 | ex 115 |
. . . . 5
β’ (π₯ β π΄ β (π:Οβontoβ(π΄ β 1o) β βπ π:Οβontoβπ΄)) |
51 | 50 | exlimiv 1598 |
. . . 4
β’
(βπ₯ π₯ β π΄ β (π:Οβontoβ(π΄ β 1o) β βπ π:Οβontoβπ΄)) |
52 | 51 | exlimdv 1819 |
. . 3
β’
(βπ₯ π₯ β π΄ β (βπ π:Οβontoβ(π΄ β 1o) β βπ π:Οβontoβπ΄)) |
53 | | foeq1 5434 |
. . . 4
β’ (π = π β (π:Οβontoβπ΄ β π:Οβontoβπ΄)) |
54 | 53 | cbvexv 1918 |
. . 3
β’
(βπ π:Οβontoβπ΄ β βπ π:Οβontoβπ΄) |
55 | 52, 54 | syl6ibr 162 |
. 2
β’
(βπ₯ π₯ β π΄ β (βπ π:Οβontoβ(π΄ β 1o) β βπ π:Οβontoβπ΄)) |
56 | | ctmlemr 7106 |
. 2
β’
(βπ₯ π₯ β π΄ β (βπ π:Οβontoβπ΄ β βπ π:Οβontoβ(π΄ β 1o))) |
57 | 55, 56 | impbid 129 |
1
β’
(βπ₯ π₯ β π΄ β (βπ π:Οβontoβ(π΄ β 1o) β βπ π:Οβontoβπ΄)) |