Step | Hyp | Ref
| Expression |
1 | | omp1eom 7093 |
. . . . 5
β’ (Ο
β 1o) β Ο |
2 | | simp2 998 |
. . . . 5
β’
((βπ₯ β
π΄ βπ¦ β π΄ DECID π₯ = π¦ β§ Ο βΌ π΄ β§ π΅ β π΄) β Ο βΌ π΄) |
3 | | endomtr 6789 |
. . . . 5
β’
(((Ο β 1o) β Ο β§ Ο βΌ
π΄) β (Ο β
1o) βΌ π΄) |
4 | 1, 2, 3 | sylancr 414 |
. . . 4
β’
((βπ₯ β
π΄ βπ¦ β π΄ DECID π₯ = π¦ β§ Ο βΌ π΄ β§ π΅ β π΄) β (Ο β 1o)
βΌ π΄) |
5 | | brdomi 6748 |
. . . 4
β’ ((Ο
β 1o) βΌ π΄ β βπ π:(Ο β 1o)β1-1βπ΄) |
6 | 4, 5 | syl 14 |
. . 3
β’
((βπ₯ β
π΄ βπ¦ β π΄ DECID π₯ = π¦ β§ Ο βΌ π΄ β§ π΅ β π΄) β βπ π:(Ο β 1o)β1-1βπ΄) |
7 | | inlresf1 7059 |
. . . . . . . 8
β’ (inl
βΎ Ο):Οβ1-1β(Ο β
1o) |
8 | | f1co 5433 |
. . . . . . . 8
β’ ((π:(Ο β
1o)β1-1βπ΄ β§ (inl βΎ
Ο):Οβ1-1β(Ο
β 1o)) β (π β (inl βΎ
Ο)):Οβ1-1βπ΄) |
9 | 7, 8 | mpan2 425 |
. . . . . . 7
β’ (π:(Ο β
1o)β1-1βπ΄ β (π β (inl βΎ
Ο)):Οβ1-1βπ΄) |
10 | 9 | ad2antlr 489 |
. . . . . 6
β’
((((βπ₯ β
π΄ βπ¦ β π΄ DECID π₯ = π¦ β§ Ο βΌ π΄ β§ π΅ β π΄) β§ π:(Ο β 1o)β1-1βπ΄) β§ (πβ(inrββ
)) = π΅) β (π β (inl βΎ
Ο)):Οβ1-1βπ΄) |
11 | | f1f 5421 |
. . . . . . . . . . . 12
β’ ((π β (inl βΎ
Ο)):Οβ1-1βπ΄ β (π β (inl βΎ
Ο)):ΟβΆπ΄) |
12 | 10, 11 | syl 14 |
. . . . . . . . . . 11
β’
((((βπ₯ β
π΄ βπ¦ β π΄ DECID π₯ = π¦ β§ Ο βΌ π΄ β§ π΅ β π΄) β§ π:(Ο β 1o)β1-1βπ΄) β§ (πβ(inrββ
)) = π΅) β (π β (inl βΎ
Ο)):ΟβΆπ΄) |
13 | 12 | frnd 5375 |
. . . . . . . . . 10
β’
((((βπ₯ β
π΄ βπ¦ β π΄ DECID π₯ = π¦ β§ Ο βΌ π΄ β§ π΅ β π΄) β§ π:(Ο β 1o)β1-1βπ΄) β§ (πβ(inrββ
)) = π΅) β ran (π β (inl βΎ Ο)) β π΄) |
14 | 13 | sselda 3155 |
. . . . . . . . 9
β’
(((((βπ₯
β π΄ βπ¦ β π΄ DECID π₯ = π¦ β§ Ο βΌ π΄ β§ π΅ β π΄) β§ π:(Ο β 1o)β1-1βπ΄) β§ (πβ(inrββ
)) = π΅) β§ π β ran (π β (inl βΎ Ο))) β π β π΄) |
15 | | simpllr 534 |
. . . . . . . . . . . . . . . 16
β’
((((((βπ₯
β π΄ βπ¦ β π΄ DECID π₯ = π¦ β§ Ο βΌ π΄ β§ π΅ β π΄) β§ π:(Ο β 1o)β1-1βπ΄) β§ (πβ(inrββ
)) = π΅) β§ π β Ο) β§ ((π β (inl βΎ Ο))βπ) = π΅) β (πβ(inrββ
)) = π΅) |
16 | | simpr 110 |
. . . . . . . . . . . . . . . 16
β’
((((((βπ₯
β π΄ βπ¦ β π΄ DECID π₯ = π¦ β§ Ο βΌ π΄ β§ π΅ β π΄) β§ π:(Ο β 1o)β1-1βπ΄) β§ (πβ(inrββ
)) = π΅) β§ π β Ο) β§ ((π β (inl βΎ Ο))βπ) = π΅) β ((π β (inl βΎ Ο))βπ) = π΅) |
17 | | f1f 5421 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((inl
βΎ Ο):Οβ1-1β(Ο β 1o) β (inl
βΎ Ο):ΟβΆ(Ο β
1o)) |
18 | 7, 17 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
β’ (inl
βΎ Ο):ΟβΆ(Ο β
1o) |
19 | | simpr 110 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((βπ₯
β π΄ βπ¦ β π΄ DECID π₯ = π¦ β§ Ο βΌ π΄ β§ π΅ β π΄) β§ π:(Ο β 1o)β1-1βπ΄) β§ (πβ(inrββ
)) = π΅) β§ π β Ο) β π β Ο) |
20 | | fvco3 5587 |
. . . . . . . . . . . . . . . . . . 19
β’ (((inl
βΎ Ο):ΟβΆ(Ο β 1o) β§ π β Ο) β ((π β (inl βΎ
Ο))βπ) = (πβ((inl βΎ
Ο)βπ))) |
21 | 18, 19, 20 | sylancr 414 |
. . . . . . . . . . . . . . . . . 18
β’
(((((βπ₯
β π΄ βπ¦ β π΄ DECID π₯ = π¦ β§ Ο βΌ π΄ β§ π΅ β π΄) β§ π:(Ο β 1o)β1-1βπ΄) β§ (πβ(inrββ
)) = π΅) β§ π β Ο) β ((π β (inl βΎ Ο))βπ) = (πβ((inl βΎ Ο)βπ))) |
22 | 19 | fvresd 5540 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((βπ₯
β π΄ βπ¦ β π΄ DECID π₯ = π¦ β§ Ο βΌ π΄ β§ π΅ β π΄) β§ π:(Ο β 1o)β1-1βπ΄) β§ (πβ(inrββ
)) = π΅) β§ π β Ο) β ((inl βΎ
Ο)βπ) =
(inlβπ)) |
23 | 22 | fveq2d 5519 |
. . . . . . . . . . . . . . . . . 18
β’
(((((βπ₯
β π΄ βπ¦ β π΄ DECID π₯ = π¦ β§ Ο βΌ π΄ β§ π΅ β π΄) β§ π:(Ο β 1o)β1-1βπ΄) β§ (πβ(inrββ
)) = π΅) β§ π β Ο) β (πβ((inl βΎ Ο)βπ)) = (πβ(inlβπ))) |
24 | 21, 23 | eqtrd 2210 |
. . . . . . . . . . . . . . . . 17
β’
(((((βπ₯
β π΄ βπ¦ β π΄ DECID π₯ = π¦ β§ Ο βΌ π΄ β§ π΅ β π΄) β§ π:(Ο β 1o)β1-1βπ΄) β§ (πβ(inrββ
)) = π΅) β§ π β Ο) β ((π β (inl βΎ Ο))βπ) = (πβ(inlβπ))) |
25 | 24 | adantr 276 |
. . . . . . . . . . . . . . . 16
β’
((((((βπ₯
β π΄ βπ¦ β π΄ DECID π₯ = π¦ β§ Ο βΌ π΄ β§ π΅ β π΄) β§ π:(Ο β 1o)β1-1βπ΄) β§ (πβ(inrββ
)) = π΅) β§ π β Ο) β§ ((π β (inl βΎ Ο))βπ) = π΅) β ((π β (inl βΎ Ο))βπ) = (πβ(inlβπ))) |
26 | 15, 16, 25 | 3eqtr2rd 2217 |
. . . . . . . . . . . . . . 15
β’
((((((βπ₯
β π΄ βπ¦ β π΄ DECID π₯ = π¦ β§ Ο βΌ π΄ β§ π΅ β π΄) β§ π:(Ο β 1o)β1-1βπ΄) β§ (πβ(inrββ
)) = π΅) β§ π β Ο) β§ ((π β (inl βΎ Ο))βπ) = π΅) β (πβ(inlβπ)) = (πβ(inrββ
))) |
27 | | simp-4r 542 |
. . . . . . . . . . . . . . . 16
β’
((((((βπ₯
β π΄ βπ¦ β π΄ DECID π₯ = π¦ β§ Ο βΌ π΄ β§ π΅ β π΄) β§ π:(Ο β 1o)β1-1βπ΄) β§ (πβ(inrββ
)) = π΅) β§ π β Ο) β§ ((π β (inl βΎ Ο))βπ) = π΅) β π:(Ο β 1o)β1-1βπ΄) |
28 | | djulcl 7049 |
. . . . . . . . . . . . . . . . 17
β’ (π β Ο β
(inlβπ) β
(Ο β 1o)) |
29 | 28 | ad2antlr 489 |
. . . . . . . . . . . . . . . 16
β’
((((((βπ₯
β π΄ βπ¦ β π΄ DECID π₯ = π¦ β§ Ο βΌ π΄ β§ π΅ β π΄) β§ π:(Ο β 1o)β1-1βπ΄) β§ (πβ(inrββ
)) = π΅) β§ π β Ο) β§ ((π β (inl βΎ Ο))βπ) = π΅) β (inlβπ) β (Ο β
1o)) |
30 | | 0lt1o 6440 |
. . . . . . . . . . . . . . . . . 18
β’ β
β 1o |
31 | | djurcl 7050 |
. . . . . . . . . . . . . . . . . 18
β’ (β
β 1o β (inrββ
) β (Ο β
1o)) |
32 | 30, 31 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
β’
(inrββ
) β (Ο β
1o) |
33 | 32 | a1i 9 |
. . . . . . . . . . . . . . . 16
β’
((((((βπ₯
β π΄ βπ¦ β π΄ DECID π₯ = π¦ β§ Ο βΌ π΄ β§ π΅ β π΄) β§ π:(Ο β 1o)β1-1βπ΄) β§ (πβ(inrββ
)) = π΅) β§ π β Ο) β§ ((π β (inl βΎ Ο))βπ) = π΅) β (inrββ
) β (Ο
β 1o)) |
34 | | f1veqaeq 5769 |
. . . . . . . . . . . . . . . 16
β’ ((π:(Ο β
1o)β1-1βπ΄ β§ ((inlβπ) β (Ο β
1o) β§ (inrββ
) β (Ο β
1o))) β ((πβ(inlβπ)) = (πβ(inrββ
)) β
(inlβπ) =
(inrββ
))) |
35 | 27, 29, 33, 34 | syl12anc 1236 |
. . . . . . . . . . . . . . 15
β’
((((((βπ₯
β π΄ βπ¦ β π΄ DECID π₯ = π¦ β§ Ο βΌ π΄ β§ π΅ β π΄) β§ π:(Ο β 1o)β1-1βπ΄) β§ (πβ(inrββ
)) = π΅) β§ π β Ο) β§ ((π β (inl βΎ Ο))βπ) = π΅) β ((πβ(inlβπ)) = (πβ(inrββ
)) β
(inlβπ) =
(inrββ
))) |
36 | 26, 35 | mpd 13 |
. . . . . . . . . . . . . 14
β’
((((((βπ₯
β π΄ βπ¦ β π΄ DECID π₯ = π¦ β§ Ο βΌ π΄ β§ π΅ β π΄) β§ π:(Ο β 1o)β1-1βπ΄) β§ (πβ(inrββ
)) = π΅) β§ π β Ο) β§ ((π β (inl βΎ Ο))βπ) = π΅) β (inlβπ) = (inrββ
)) |
37 | 19 | adantr 276 |
. . . . . . . . . . . . . . . 16
β’
((((((βπ₯
β π΄ βπ¦ β π΄ DECID π₯ = π¦ β§ Ο βΌ π΄ β§ π΅ β π΄) β§ π:(Ο β 1o)β1-1βπ΄) β§ (πβ(inrββ
)) = π΅) β§ π β Ο) β§ ((π β (inl βΎ Ο))βπ) = π΅) β π β Ο) |
38 | | djune 7076 |
. . . . . . . . . . . . . . . 16
β’ ((π β Ο β§ β
β 1o) β (inlβπ) β (inrββ
)) |
39 | 37, 30, 38 | sylancl 413 |
. . . . . . . . . . . . . . 15
β’
((((((βπ₯
β π΄ βπ¦ β π΄ DECID π₯ = π¦ β§ Ο βΌ π΄ β§ π΅ β π΄) β§ π:(Ο β 1o)β1-1βπ΄) β§ (πβ(inrββ
)) = π΅) β§ π β Ο) β§ ((π β (inl βΎ Ο))βπ) = π΅) β (inlβπ) β (inrββ
)) |
40 | 39 | neneqd 2368 |
. . . . . . . . . . . . . 14
β’
((((((βπ₯
β π΄ βπ¦ β π΄ DECID π₯ = π¦ β§ Ο βΌ π΄ β§ π΅ β π΄) β§ π:(Ο β 1o)β1-1βπ΄) β§ (πβ(inrββ
)) = π΅) β§ π β Ο) β§ ((π β (inl βΎ Ο))βπ) = π΅) β Β¬ (inlβπ) = (inrββ
)) |
41 | 36, 40 | pm2.65da 661 |
. . . . . . . . . . . . 13
β’
(((((βπ₯
β π΄ βπ¦ β π΄ DECID π₯ = π¦ β§ Ο βΌ π΄ β§ π΅ β π΄) β§ π:(Ο β 1o)β1-1βπ΄) β§ (πβ(inrββ
)) = π΅) β§ π β Ο) β Β¬ ((π β (inl βΎ
Ο))βπ) = π΅) |
42 | 41 | ralrimiva 2550 |
. . . . . . . . . . . 12
β’
((((βπ₯ β
π΄ βπ¦ β π΄ DECID π₯ = π¦ β§ Ο βΌ π΄ β§ π΅ β π΄) β§ π:(Ο β 1o)β1-1βπ΄) β§ (πβ(inrββ
)) = π΅) β βπ β Ο Β¬ ((π β (inl βΎ
Ο))βπ) = π΅) |
43 | 12 | ffnd 5366 |
. . . . . . . . . . . . 13
β’
((((βπ₯ β
π΄ βπ¦ β π΄ DECID π₯ = π¦ β§ Ο βΌ π΄ β§ π΅ β π΄) β§ π:(Ο β 1o)β1-1βπ΄) β§ (πβ(inrββ
)) = π΅) β (π β (inl βΎ Ο)) Fn
Ο) |
44 | | eqeq1 2184 |
. . . . . . . . . . . . . . 15
β’ (π = ((π β (inl βΎ Ο))βπ) β (π = π΅ β ((π β (inl βΎ Ο))βπ) = π΅)) |
45 | 44 | notbid 667 |
. . . . . . . . . . . . . 14
β’ (π = ((π β (inl βΎ Ο))βπ) β (Β¬ π = π΅ β Β¬ ((π β (inl βΎ Ο))βπ) = π΅)) |
46 | 45 | ralrn 5654 |
. . . . . . . . . . . . 13
β’ ((π β (inl βΎ Ο))
Fn Ο β (βπ β ran (π β (inl βΎ Ο)) Β¬ π = π΅ β βπ β Ο Β¬ ((π β (inl βΎ Ο))βπ) = π΅)) |
47 | 43, 46 | syl 14 |
. . . . . . . . . . . 12
β’
((((βπ₯ β
π΄ βπ¦ β π΄ DECID π₯ = π¦ β§ Ο βΌ π΄ β§ π΅ β π΄) β§ π:(Ο β 1o)β1-1βπ΄) β§ (πβ(inrββ
)) = π΅) β (βπ β ran (π β (inl βΎ Ο)) Β¬ π = π΅ β βπ β Ο Β¬ ((π β (inl βΎ Ο))βπ) = π΅)) |
48 | 42, 47 | mpbird 167 |
. . . . . . . . . . 11
β’
((((βπ₯ β
π΄ βπ¦ β π΄ DECID π₯ = π¦ β§ Ο βΌ π΄ β§ π΅ β π΄) β§ π:(Ο β 1o)β1-1βπ΄) β§ (πβ(inrββ
)) = π΅) β βπ β ran (π β (inl βΎ Ο)) Β¬ π = π΅) |
49 | 48 | r19.21bi 2565 |
. . . . . . . . . 10
β’
(((((βπ₯
β π΄ βπ¦ β π΄ DECID π₯ = π¦ β§ Ο βΌ π΄ β§ π΅ β π΄) β§ π:(Ο β 1o)β1-1βπ΄) β§ (πβ(inrββ
)) = π΅) β§ π β ran (π β (inl βΎ Ο))) β Β¬
π = π΅) |
50 | | velsn 3609 |
. . . . . . . . . 10
β’ (π β {π΅} β π = π΅) |
51 | 49, 50 | sylnibr 677 |
. . . . . . . . 9
β’
(((((βπ₯
β π΄ βπ¦ β π΄ DECID π₯ = π¦ β§ Ο βΌ π΄ β§ π΅ β π΄) β§ π:(Ο β 1o)β1-1βπ΄) β§ (πβ(inrββ
)) = π΅) β§ π β ran (π β (inl βΎ Ο))) β Β¬
π β {π΅}) |
52 | 14, 51 | eldifd 3139 |
. . . . . . . 8
β’
(((((βπ₯
β π΄ βπ¦ β π΄ DECID π₯ = π¦ β§ Ο βΌ π΄ β§ π΅ β π΄) β§ π:(Ο β 1o)β1-1βπ΄) β§ (πβ(inrββ
)) = π΅) β§ π β ran (π β (inl βΎ Ο))) β π β (π΄ β {π΅})) |
53 | 52 | ex 115 |
. . . . . . 7
β’
((((βπ₯ β
π΄ βπ¦ β π΄ DECID π₯ = π¦ β§ Ο βΌ π΄ β§ π΅ β π΄) β§ π:(Ο β 1o)β1-1βπ΄) β§ (πβ(inrββ
)) = π΅) β (π β ran (π β (inl βΎ Ο)) β π β (π΄ β {π΅}))) |
54 | 53 | ssrdv 3161 |
. . . . . 6
β’
((((βπ₯ β
π΄ βπ¦ β π΄ DECID π₯ = π¦ β§ Ο βΌ π΄ β§ π΅ β π΄) β§ π:(Ο β 1o)β1-1βπ΄) β§ (πβ(inrββ
)) = π΅) β ran (π β (inl βΎ Ο)) β
(π΄ β {π΅})) |
55 | | f1ssr 5428 |
. . . . . 6
β’ (((π β (inl βΎ
Ο)):Οβ1-1βπ΄ β§ ran (π β (inl βΎ Ο)) β
(π΄ β {π΅})) β (π β (inl βΎ
Ο)):Οβ1-1β(π΄ β {π΅})) |
56 | 10, 54, 55 | syl2anc 411 |
. . . . 5
β’
((((βπ₯ β
π΄ βπ¦ β π΄ DECID π₯ = π¦ β§ Ο βΌ π΄ β§ π΅ β π΄) β§ π:(Ο β 1o)β1-1βπ΄) β§ (πβ(inrββ
)) = π΅) β (π β (inl βΎ
Ο)):Οβ1-1β(π΄ β {π΅})) |
57 | | f1f 5421 |
. . . . . . 7
β’ ((π β (inl βΎ
Ο)):Οβ1-1β(π΄ β {π΅}) β (π β (inl βΎ
Ο)):ΟβΆ(π΄
β {π΅})) |
58 | | omex 4592 |
. . . . . . 7
β’ Ο
β V |
59 | | fex 5745 |
. . . . . . 7
β’ (((π β (inl βΎ
Ο)):ΟβΆ(π΄
β {π΅}) β§ Ο
β V) β (π β
(inl βΎ Ο)) β V) |
60 | 57, 58, 59 | sylancl 413 |
. . . . . 6
β’ ((π β (inl βΎ
Ο)):Οβ1-1β(π΄ β {π΅}) β (π β (inl βΎ Ο)) β
V) |
61 | | f1eq1 5416 |
. . . . . . 7
β’ (π = (π β (inl βΎ Ο)) β (π:Οβ1-1β(π΄ β {π΅}) β (π β (inl βΎ
Ο)):Οβ1-1β(π΄ β {π΅}))) |
62 | 61 | spcegv 2825 |
. . . . . 6
β’ ((π β (inl βΎ Ο))
β V β ((π β
(inl βΎ Ο)):Οβ1-1β(π΄ β {π΅}) β βπ π:Οβ1-1β(π΄ β {π΅}))) |
63 | 60, 62 | mpcom 36 |
. . . . 5
β’ ((π β (inl βΎ
Ο)):Οβ1-1β(π΄ β {π΅}) β βπ π:Οβ1-1β(π΄ β {π΅})) |
64 | 56, 63 | syl 14 |
. . . 4
β’
((((βπ₯ β
π΄ βπ¦ β π΄ DECID π₯ = π¦ β§ Ο βΌ π΄ β§ π΅ β π΄) β§ π:(Ο β 1o)β1-1βπ΄) β§ (πβ(inrββ
)) = π΅) β βπ π:Οβ1-1β(π΄ β {π΅})) |
65 | | simpl1 1000 |
. . . . . . 7
β’
(((βπ₯ β
π΄ βπ¦ β π΄ DECID π₯ = π¦ β§ Ο βΌ π΄ β§ π΅ β π΄) β§ π:(Ο β 1o)β1-1βπ΄) β βπ₯ β π΄ βπ¦ β π΄ DECID π₯ = π¦) |
66 | 65 | adantr 276 |
. . . . . 6
β’
((((βπ₯ β
π΄ βπ¦ β π΄ DECID π₯ = π¦ β§ Ο βΌ π΄ β§ π΅ β π΄) β§ π:(Ο β 1o)β1-1βπ΄) β§ Β¬ (πβ(inrββ
)) = π΅) β βπ₯ β π΄ βπ¦ β π΄ DECID π₯ = π¦) |
67 | | simpl3 1002 |
. . . . . . 7
β’
(((βπ₯ β
π΄ βπ¦ β π΄ DECID π₯ = π¦ β§ Ο βΌ π΄ β§ π΅ β π΄) β§ π:(Ο β 1o)β1-1βπ΄) β π΅ β π΄) |
68 | 67 | adantr 276 |
. . . . . 6
β’
((((βπ₯ β
π΄ βπ¦ β π΄ DECID π₯ = π¦ β§ Ο βΌ π΄ β§ π΅ β π΄) β§ π:(Ο β 1o)β1-1βπ΄) β§ Β¬ (πβ(inrββ
)) = π΅) β π΅ β π΄) |
69 | | simpr 110 |
. . . . . . 7
β’
(((βπ₯ β
π΄ βπ¦ β π΄ DECID π₯ = π¦ β§ Ο βΌ π΄ β§ π΅ β π΄) β§ π:(Ο β 1o)β1-1βπ΄) β π:(Ο β 1o)β1-1βπ΄) |
70 | 69 | adantr 276 |
. . . . . 6
β’
((((βπ₯ β
π΄ βπ¦ β π΄ DECID π₯ = π¦ β§ Ο βΌ π΄ β§ π΅ β π΄) β§ π:(Ο β 1o)β1-1βπ΄) β§ Β¬ (πβ(inrββ
)) = π΅) β π:(Ο β 1o)β1-1βπ΄) |
71 | | simpr 110 |
. . . . . . 7
β’
((((βπ₯ β
π΄ βπ¦ β π΄ DECID π₯ = π¦ β§ Ο βΌ π΄ β§ π΅ β π΄) β§ π:(Ο β 1o)β1-1βπ΄) β§ Β¬ (πβ(inrββ
)) = π΅) β Β¬ (πβ(inrββ
)) =
π΅) |
72 | 71 | neqned 2354 |
. . . . . 6
β’
((((βπ₯ β
π΄ βπ¦ β π΄ DECID π₯ = π¦ β§ Ο βΌ π΄ β§ π΅ β π΄) β§ π:(Ο β 1o)β1-1βπ΄) β§ Β¬ (πβ(inrββ
)) = π΅) β (πβ(inrββ
)) β π΅) |
73 | | eqid 2177 |
. . . . . 6
β’ (π β Ο β¦
if((πβ(inlβπ)) = π΅, (πβ(inrββ
)), (πβ(inlβπ)))) = (π β Ο β¦ if((πβ(inlβπ)) = π΅, (πβ(inrββ
)), (πβ(inlβπ)))) |
74 | 66, 68, 70, 72, 73 | difinfsnlem 7097 |
. . . . 5
β’
((((βπ₯ β
π΄ βπ¦ β π΄ DECID π₯ = π¦ β§ Ο βΌ π΄ β§ π΅ β π΄) β§ π:(Ο β 1o)β1-1βπ΄) β§ Β¬ (πβ(inrββ
)) = π΅) β (π β Ο β¦ if((πβ(inlβπ)) = π΅, (πβ(inrββ
)), (πβ(inlβπ)))):Οβ1-1β(π΄ β {π΅})) |
75 | 58 | mptex 5742 |
. . . . . 6
β’ (π β Ο β¦
if((πβ(inlβπ)) = π΅, (πβ(inrββ
)), (πβ(inlβπ)))) β V |
76 | | f1eq1 5416 |
. . . . . 6
β’ (π = (π β Ο β¦ if((πβ(inlβπ)) = π΅, (πβ(inrββ
)), (πβ(inlβπ)))) β (π:Οβ1-1β(π΄ β {π΅}) β (π β Ο β¦ if((πβ(inlβπ)) = π΅, (πβ(inrββ
)), (πβ(inlβπ)))):Οβ1-1β(π΄ β {π΅}))) |
77 | 75, 76 | spcev 2832 |
. . . . 5
β’ ((π β Ο β¦
if((πβ(inlβπ)) = π΅, (πβ(inrββ
)), (πβ(inlβπ)))):Οβ1-1β(π΄ β {π΅}) β βπ π:Οβ1-1β(π΄ β {π΅})) |
78 | 74, 77 | syl 14 |
. . . 4
β’
((((βπ₯ β
π΄ βπ¦ β π΄ DECID π₯ = π¦ β§ Ο βΌ π΄ β§ π΅ β π΄) β§ π:(Ο β 1o)β1-1βπ΄) β§ Β¬ (πβ(inrββ
)) = π΅) β βπ π:Οβ1-1β(π΄ β {π΅})) |
79 | | f1f 5421 |
. . . . . . . . 9
β’ (π:(Ο β
1o)β1-1βπ΄ β π:(Ο β
1o)βΆπ΄) |
80 | 69, 79 | syl 14 |
. . . . . . . 8
β’
(((βπ₯ β
π΄ βπ¦ β π΄ DECID π₯ = π¦ β§ Ο βΌ π΄ β§ π΅ β π΄) β§ π:(Ο β 1o)β1-1βπ΄) β π:(Ο β
1o)βΆπ΄) |
81 | 32 | a1i 9 |
. . . . . . . 8
β’
(((βπ₯ β
π΄ βπ¦ β π΄ DECID π₯ = π¦ β§ Ο βΌ π΄ β§ π΅ β π΄) β§ π:(Ο β 1o)β1-1βπ΄) β (inrββ
) β (Ο
β 1o)) |
82 | 80, 81 | ffvelcdmd 5652 |
. . . . . . 7
β’
(((βπ₯ β
π΄ βπ¦ β π΄ DECID π₯ = π¦ β§ Ο βΌ π΄ β§ π΅ β π΄) β§ π:(Ο β 1o)β1-1βπ΄) β (πβ(inrββ
)) β π΄) |
83 | 82, 67 | jca 306 |
. . . . . 6
β’
(((βπ₯ β
π΄ βπ¦ β π΄ DECID π₯ = π¦ β§ Ο βΌ π΄ β§ π΅ β π΄) β§ π:(Ο β 1o)β1-1βπ΄) β ((πβ(inrββ
)) β π΄ β§ π΅ β π΄)) |
84 | | eqeq12 2190 |
. . . . . . . 8
β’ ((π₯ = (πβ(inrββ
)) β§ π¦ = π΅) β (π₯ = π¦ β (πβ(inrββ
)) = π΅)) |
85 | 84 | dcbid 838 |
. . . . . . 7
β’ ((π₯ = (πβ(inrββ
)) β§ π¦ = π΅) β (DECID π₯ = π¦ β DECID (πβ(inrββ
)) =
π΅)) |
86 | 85 | rspc2gv 2853 |
. . . . . 6
β’ (((πβ(inrββ
))
β π΄ β§ π΅ β π΄) β (βπ₯ β π΄ βπ¦ β π΄ DECID π₯ = π¦ β DECID (πβ(inrββ
)) =
π΅)) |
87 | 83, 65, 86 | sylc 62 |
. . . . 5
β’
(((βπ₯ β
π΄ βπ¦ β π΄ DECID π₯ = π¦ β§ Ο βΌ π΄ β§ π΅ β π΄) β§ π:(Ο β 1o)β1-1βπ΄) β DECID (πβ(inrββ
)) =
π΅) |
88 | | exmiddc 836 |
. . . . 5
β’
(DECID (πβ(inrββ
)) = π΅ β ((πβ(inrββ
)) = π΅ β¨ Β¬ (πβ(inrββ
)) = π΅)) |
89 | 87, 88 | syl 14 |
. . . 4
β’
(((βπ₯ β
π΄ βπ¦ β π΄ DECID π₯ = π¦ β§ Ο βΌ π΄ β§ π΅ β π΄) β§ π:(Ο β 1o)β1-1βπ΄) β ((πβ(inrββ
)) = π΅ β¨ Β¬ (πβ(inrββ
)) = π΅)) |
90 | 64, 78, 89 | mpjaodan 798 |
. . 3
β’
(((βπ₯ β
π΄ βπ¦ β π΄ DECID π₯ = π¦ β§ Ο βΌ π΄ β§ π΅ β π΄) β§ π:(Ο β 1o)β1-1βπ΄) β βπ π:Οβ1-1β(π΄ β {π΅})) |
91 | 6, 90 | exlimddv 1898 |
. 2
β’
((βπ₯ β
π΄ βπ¦ β π΄ DECID π₯ = π¦ β§ Ο βΌ π΄ β§ π΅ β π΄) β βπ π:Οβ1-1β(π΄ β {π΅})) |
92 | | reldom 6744 |
. . . . . 6
β’ Rel
βΌ |
93 | 92 | brrelex2i 4670 |
. . . . 5
β’ (Ο
βΌ π΄ β π΄ β V) |
94 | | difexg 4144 |
. . . . 5
β’ (π΄ β V β (π΄ β {π΅}) β V) |
95 | 93, 94 | syl 14 |
. . . 4
β’ (Ο
βΌ π΄ β (π΄ β {π΅}) β V) |
96 | 95 | 3ad2ant2 1019 |
. . 3
β’
((βπ₯ β
π΄ βπ¦ β π΄ DECID π₯ = π¦ β§ Ο βΌ π΄ β§ π΅ β π΄) β (π΄ β {π΅}) β V) |
97 | | brdomg 6747 |
. . 3
β’ ((π΄ β {π΅}) β V β (Ο βΌ (π΄ β {π΅}) β βπ π:Οβ1-1β(π΄ β {π΅}))) |
98 | 96, 97 | syl 14 |
. 2
β’
((βπ₯ β
π΄ βπ¦ β π΄ DECID π₯ = π¦ β§ Ο βΌ π΄ β§ π΅ β π΄) β (Ο βΌ (π΄ β {π΅}) β βπ π:Οβ1-1β(π΄ β {π΅}))) |
99 | 91, 98 | mpbird 167 |
1
β’
((βπ₯ β
π΄ βπ¦ β π΄ DECID π₯ = π¦ β§ Ο βΌ π΄ β§ π΅ β π΄) β Ο βΌ (π΄ β {π΅})) |