Step | Hyp | Ref
| Expression |
1 | | simpl 109 |
. . . . . . 7
β’
((βπ₯βπ¦((π₯ βΌ π¦ β§ π¦ βΌ π₯) β π₯ β π¦) β§ π§ β {β
}) β βπ₯βπ¦((π₯ βΌ π¦ β§ π¦ βΌ π₯) β π₯ β π¦)) |
2 | | nninfex 7119 |
. . . . . . . . . 10
β’
ββ β V |
3 | | fconstmpt 4673 |
. . . . . . . . . . . . . . 15
β’ (Ο
Γ {β
}) = (π
β Ο β¦ β
) |
4 | | 0nninf 14723 |
. . . . . . . . . . . . . . 15
β’ (Ο
Γ {β
}) β ββ |
5 | 3, 4 | eqeltrri 2251 |
. . . . . . . . . . . . . 14
β’ (π β Ο β¦ β
)
β ββ |
6 | 5 | fconst6 5415 |
. . . . . . . . . . . . 13
β’ (π§ Γ {(π β Ο β¦ β
)}):π§βΆββ |
7 | 6 | a1i 9 |
. . . . . . . . . . . 12
β’ (π§ β {β
} β (π§ Γ {(π β Ο β¦ β
)}):π§βΆββ) |
8 | | ssel 3149 |
. . . . . . . . . . . . . . . . . 18
β’ (π§ β {β
} β (π’ β π§ β π’ β {β
})) |
9 | | elsni 3610 |
. . . . . . . . . . . . . . . . . 18
β’ (π’ β {β
} β π’ = β
) |
10 | 8, 9 | syl6 33 |
. . . . . . . . . . . . . . . . 17
β’ (π§ β {β
} β (π’ β π§ β π’ = β
)) |
11 | | ssel 3149 |
. . . . . . . . . . . . . . . . . 18
β’ (π§ β {β
} β (π£ β π§ β π£ β {β
})) |
12 | | elsni 3610 |
. . . . . . . . . . . . . . . . . 18
β’ (π£ β {β
} β π£ = β
) |
13 | 11, 12 | syl6 33 |
. . . . . . . . . . . . . . . . 17
β’ (π§ β {β
} β (π£ β π§ β π£ = β
)) |
14 | 10, 13 | anim12d 335 |
. . . . . . . . . . . . . . . 16
β’ (π§ β {β
} β
((π’ β π§ β§ π£ β π§) β (π’ = β
β§ π£ = β
))) |
15 | | eqtr3 2197 |
. . . . . . . . . . . . . . . 16
β’ ((π’ = β
β§ π£ = β
) β π’ = π£) |
16 | 14, 15 | syl6 33 |
. . . . . . . . . . . . . . 15
β’ (π§ β {β
} β
((π’ β π§ β§ π£ β π§) β π’ = π£)) |
17 | 16 | imp 124 |
. . . . . . . . . . . . . 14
β’ ((π§ β {β
} β§ (π’ β π§ β§ π£ β π§)) β π’ = π£) |
18 | 17 | a1d 22 |
. . . . . . . . . . . . 13
β’ ((π§ β {β
} β§ (π’ β π§ β§ π£ β π§)) β (((π§ Γ {(π β Ο β¦
β
)})βπ’) =
((π§ Γ {(π β Ο β¦
β
)})βπ£) β
π’ = π£)) |
19 | 18 | ralrimivva 2559 |
. . . . . . . . . . . 12
β’ (π§ β {β
} β
βπ’ β π§ βπ£ β π§ (((π§ Γ {(π β Ο β¦
β
)})βπ’) =
((π§ Γ {(π β Ο β¦
β
)})βπ£) β
π’ = π£)) |
20 | | dff13 5768 |
. . . . . . . . . . . 12
β’ ((π§ Γ {(π β Ο β¦ β
)}):π§β1-1βββ β ((π§ Γ {(π β Ο β¦ β
)}):π§βΆββ β§
βπ’ β π§ βπ£ β π§ (((π§ Γ {(π β Ο β¦
β
)})βπ’) =
((π§ Γ {(π β Ο β¦
β
)})βπ£) β
π’ = π£))) |
21 | 7, 19, 20 | sylanbrc 417 |
. . . . . . . . . . 11
β’ (π§ β {β
} β (π§ Γ {(π β Ο β¦ β
)}):π§β1-1βββ) |
22 | | exmidsbthrlem.s |
. . . . . . . . . . . . 13
β’ π = (π β ββ β¦
(π β Ο β¦
if(π = β
,
1o, (πββͺ π)))) |
23 | 22 | peano4nninf 14725 |
. . . . . . . . . . . 12
β’ π:βββ1-1βββ |
24 | 23 | a1i 9 |
. . . . . . . . . . 11
β’ (π§ β {β
} β π:βββ1-1βββ) |
25 | | disj 3471 |
. . . . . . . . . . . . 13
β’ ((ran
(π§ Γ {(π β Ο β¦
β
)}) β© ran π) =
β
β βπ
β ran (π§ Γ
{(π β Ο β¦
β
)}) Β¬ π β
ran π) |
26 | 22 | peano3nninf 14726 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β
ββ β (πβπ) β (π β Ο β¦
β
)) |
27 | | eqidd 2178 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π β β
= β
) |
28 | 27 | cbvmptv 4099 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β Ο β¦ β
)
= (π β Ο β¦
β
) |
29 | 28 | neeq2i 2363 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πβπ) β (π β Ο β¦ β
) β
(πβπ) β (π β Ο β¦
β
)) |
30 | 26, 29 | sylib 122 |
. . . . . . . . . . . . . . . . . 18
β’ (π β
ββ β (πβπ) β (π β Ο β¦
β
)) |
31 | 30 | neneqd 2368 |
. . . . . . . . . . . . . . . . 17
β’ (π β
ββ β Β¬ (πβπ) = (π β Ο β¦
β
)) |
32 | 31 | nrex 2569 |
. . . . . . . . . . . . . . . 16
β’ Β¬
βπ β
ββ (πβπ) = (π β Ο β¦
β
) |
33 | | f1dm 5426 |
. . . . . . . . . . . . . . . . . 18
β’ (π:βββ1-1βββ β dom
π =
ββ) |
34 | 23, 33 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
β’ dom π =
ββ |
35 | | eqcom 2179 |
. . . . . . . . . . . . . . . . 17
β’ ((π β Ο β¦ β
)
= (πβπ) β (πβπ) = (π β Ο β¦
β
)) |
36 | 34, 35 | rexeqbii 2490 |
. . . . . . . . . . . . . . . 16
β’
(βπ β dom
π(π β Ο β¦ β
) = (πβπ) β βπ β ββ (πβπ) = (π β Ο β¦
β
)) |
37 | 32, 36 | mtbir 671 |
. . . . . . . . . . . . . . 15
β’ Β¬
βπ β dom π(π β Ο β¦ β
) = (πβπ) |
38 | 22 | funmpt2 5255 |
. . . . . . . . . . . . . . . 16
β’ Fun π |
39 | | elrnrexdm 5655 |
. . . . . . . . . . . . . . . 16
β’ (Fun
π β ((π β Ο β¦ β
)
β ran π β
βπ β dom π(π β Ο β¦ β
) = (πβπ))) |
40 | 38, 39 | ax-mp 5 |
. . . . . . . . . . . . . . 15
β’ ((π β Ο β¦ β
)
β ran π β
βπ β dom π(π β Ο β¦ β
) = (πβπ)) |
41 | 37, 40 | mto 662 |
. . . . . . . . . . . . . 14
β’ Β¬
(π β Ο β¦
β
) β ran π |
42 | | rnxpss 5060 |
. . . . . . . . . . . . . . . . 17
β’ ran
(π§ Γ {(π β Ο β¦
β
)}) β {(π
β Ο β¦ β
)} |
43 | 42 | sseli 3151 |
. . . . . . . . . . . . . . . 16
β’ (π β ran (π§ Γ {(π β Ο β¦ β
)}) β
π β {(π β Ο β¦
β
)}) |
44 | | elsni 3610 |
. . . . . . . . . . . . . . . 16
β’ (π β {(π β Ο β¦ β
)} β
π = (π β Ο β¦
β
)) |
45 | 43, 44 | syl 14 |
. . . . . . . . . . . . . . 15
β’ (π β ran (π§ Γ {(π β Ο β¦ β
)}) β
π = (π β Ο β¦
β
)) |
46 | 45 | eleq1d 2246 |
. . . . . . . . . . . . . 14
β’ (π β ran (π§ Γ {(π β Ο β¦ β
)}) β
(π β ran π β (π β Ο β¦ β
) β ran
π)) |
47 | 41, 46 | mtbiri 675 |
. . . . . . . . . . . . 13
β’ (π β ran (π§ Γ {(π β Ο β¦ β
)}) β
Β¬ π β ran π) |
48 | 25, 47 | mprgbir 2535 |
. . . . . . . . . . . 12
β’ (ran
(π§ Γ {(π β Ο β¦
β
)}) β© ran π) =
β
|
49 | 48 | a1i 9 |
. . . . . . . . . . 11
β’ (π§ β {β
} β (ran
(π§ Γ {(π β Ο β¦
β
)}) β© ran π) =
β
) |
50 | 21, 24, 49 | casef1 7088 |
. . . . . . . . . 10
β’ (π§ β {β
} β
case((π§ Γ {(π β Ο β¦
β
)}), π):(π§ β
ββ)β1-1βββ) |
51 | | f1domg 6757 |
. . . . . . . . . 10
β’
(ββ β V β (case((π§ Γ {(π β Ο β¦ β
)}), π):(π§ β
ββ)β1-1βββ β (π§ β
ββ) βΌ
ββ)) |
52 | 2, 50, 51 | mpsyl 65 |
. . . . . . . . 9
β’ (π§ β {β
} β (π§ β
ββ) βΌ
ββ) |
53 | 52 | adantl 277 |
. . . . . . . 8
β’
((βπ₯βπ¦((π₯ βΌ π¦ β§ π¦ βΌ π₯) β π₯ β π¦) β§ π§ β {β
}) β (π§ β
ββ) βΌ
ββ) |
54 | | inrresf1 7060 |
. . . . . . . . 9
β’ (inr
βΎ ββ):βββ1-1β(π§ β
ββ) |
55 | | vex 2740 |
. . . . . . . . . . 11
β’ π§ β V |
56 | | djuex 7041 |
. . . . . . . . . . 11
β’ ((π§ β V β§
ββ β V) β (π§ β ββ) β
V) |
57 | 55, 2, 56 | mp2an 426 |
. . . . . . . . . 10
β’ (π§ β
ββ) β V |
58 | 57 | f1dom 6759 |
. . . . . . . . 9
β’ ((inr
βΎ ββ):βββ1-1β(π§ β ββ) β
ββ βΌ (π§ β
ββ)) |
59 | 54, 58 | ax-mp 5 |
. . . . . . . 8
β’
ββ βΌ (π§ β
ββ) |
60 | 53, 59 | jctir 313 |
. . . . . . 7
β’
((βπ₯βπ¦((π₯ βΌ π¦ β§ π¦ βΌ π₯) β π₯ β π¦) β§ π§ β {β
}) β ((π§ β
ββ) βΌ ββ β§
ββ βΌ (π§ β
ββ))) |
61 | | breq12 4008 |
. . . . . . . . . . 11
β’ ((π₯ = (π§ β ββ) β§
π¦ =
ββ) β (π₯ βΌ π¦ β (π§ β ββ) βΌ
ββ)) |
62 | | breq12 4008 |
. . . . . . . . . . . 12
β’ ((π¦ = ββ
β§ π₯ = (π§ β
ββ)) β (π¦ βΌ π₯ β ββ βΌ
(π§ β
ββ))) |
63 | 62 | ancoms 268 |
. . . . . . . . . . 11
β’ ((π₯ = (π§ β ββ) β§
π¦ =
ββ) β (π¦ βΌ π₯ β ββ βΌ
(π§ β
ββ))) |
64 | 61, 63 | anbi12d 473 |
. . . . . . . . . 10
β’ ((π₯ = (π§ β ββ) β§
π¦ =
ββ) β ((π₯ βΌ π¦ β§ π¦ βΌ π₯) β ((π§ β ββ) βΌ
ββ β§ ββ βΌ (π§ β
ββ)))) |
65 | | breq12 4008 |
. . . . . . . . . 10
β’ ((π₯ = (π§ β ββ) β§
π¦ =
ββ) β (π₯ β π¦ β (π§ β ββ) β
ββ)) |
66 | 64, 65 | imbi12d 234 |
. . . . . . . . 9
β’ ((π₯ = (π§ β ββ) β§
π¦ =
ββ) β (((π₯ βΌ π¦ β§ π¦ βΌ π₯) β π₯ β π¦) β (((π§ β ββ) βΌ
ββ β§ ββ βΌ (π§ β
ββ)) β (π§ β ββ) β
ββ))) |
67 | 66 | spc2gv 2828 |
. . . . . . . 8
β’ (((π§ β
ββ) β V β§ ββ β V)
β (βπ₯βπ¦((π₯ βΌ π¦ β§ π¦ βΌ π₯) β π₯ β π¦) β (((π§ β ββ) βΌ
ββ β§ ββ βΌ (π§ β
ββ)) β (π§ β ββ) β
ββ))) |
68 | 57, 2, 67 | mp2an 426 |
. . . . . . 7
β’
(βπ₯βπ¦((π₯ βΌ π¦ β§ π¦ βΌ π₯) β π₯ β π¦) β (((π§ β ββ) βΌ
ββ β§ ββ βΌ (π§ β
ββ)) β (π§ β ββ) β
ββ)) |
69 | 1, 60, 68 | sylc 62 |
. . . . . 6
β’
((βπ₯βπ¦((π₯ βΌ π¦ β§ π¦ βΌ π₯) β π₯ β π¦) β§ π§ β {β
}) β (π§ β
ββ) β
ββ) |
70 | | bren 6746 |
. . . . . 6
β’ ((π§ β
ββ) β ββ β
βπ π:(π§ β
ββ)β1-1-ontoβββ) |
71 | 69, 70 | sylib 122 |
. . . . 5
β’
((βπ₯βπ¦((π₯ βΌ π¦ β§ π¦ βΌ π₯) β π₯ β π¦) β§ π§ β {β
}) β βπ π:(π§ β
ββ)β1-1-ontoβββ) |
72 | | nninfomni 14738 |
. . . . . . . . 9
β’
ββ β Omni |
73 | 72 | a1i 9 |
. . . . . . . 8
β’
(((βπ₯βπ¦((π₯ βΌ π¦ β§ π¦ βΌ π₯) β π₯ β π¦) β§ π§ β {β
}) β§ π:(π§ β
ββ)β1-1-ontoβββ) β
ββ β Omni) |
74 | | f1ocnv 5474 |
. . . . . . . . . 10
β’ (π:(π§ β
ββ)β1-1-ontoβββ β β‘π:βββ1-1-ontoβ(π§ β
ββ)) |
75 | | f1ofo 5468 |
. . . . . . . . . 10
β’ (β‘π:βββ1-1-ontoβ(π§ β ββ) β
β‘π:βββontoβ(π§ β
ββ)) |
76 | 74, 75 | syl 14 |
. . . . . . . . 9
β’ (π:(π§ β
ββ)β1-1-ontoβββ β β‘π:βββontoβ(π§ β
ββ)) |
77 | 76 | adantl 277 |
. . . . . . . 8
β’
(((βπ₯βπ¦((π₯ βΌ π¦ β§ π¦ βΌ π₯) β π₯ β π¦) β§ π§ β {β
}) β§ π:(π§ β
ββ)β1-1-ontoβββ) β β‘π:βββontoβ(π§ β
ββ)) |
78 | 73, 77 | fodjuomni 7146 |
. . . . . . 7
β’
(((βπ₯βπ¦((π₯ βΌ π¦ β§ π¦ βΌ π₯) β π₯ β π¦) β§ π§ β {β
}) β§ π:(π§ β
ββ)β1-1-ontoβββ) β
(βπ€ π€ β π§ β¨ π§ = β
)) |
79 | | sssnm 3754 |
. . . . . . . . . 10
β’
(βπ€ π€ β π§ β (π§ β {β
} β π§ = {β
})) |
80 | 79 | biimpcd 159 |
. . . . . . . . 9
β’ (π§ β {β
} β
(βπ€ π€ β π§ β π§ = {β
})) |
81 | 80 | ad2antlr 489 |
. . . . . . . 8
β’
(((βπ₯βπ¦((π₯ βΌ π¦ β§ π¦ βΌ π₯) β π₯ β π¦) β§ π§ β {β
}) β§ π:(π§ β
ββ)β1-1-ontoβββ) β
(βπ€ π€ β π§ β π§ = {β
})) |
82 | 81 | orim1d 787 |
. . . . . . 7
β’
(((βπ₯βπ¦((π₯ βΌ π¦ β§ π¦ βΌ π₯) β π₯ β π¦) β§ π§ β {β
}) β§ π:(π§ β
ββ)β1-1-ontoβββ) β
((βπ€ π€ β π§ β¨ π§ = β
) β (π§ = {β
} β¨ π§ = β
))) |
83 | 78, 82 | mpd 13 |
. . . . . 6
β’
(((βπ₯βπ¦((π₯ βΌ π¦ β§ π¦ βΌ π₯) β π₯ β π¦) β§ π§ β {β
}) β§ π:(π§ β
ββ)β1-1-ontoβββ) β (π§ = {β
} β¨ π§ = β
)) |
84 | 83 | orcomd 729 |
. . . . 5
β’
(((βπ₯βπ¦((π₯ βΌ π¦ β§ π¦ βΌ π₯) β π₯ β π¦) β§ π§ β {β
}) β§ π:(π§ β
ββ)β1-1-ontoβββ) β (π§ = β
β¨ π§ = {β
})) |
85 | 71, 84 | exlimddv 1898 |
. . . 4
β’
((βπ₯βπ¦((π₯ βΌ π¦ β§ π¦ βΌ π₯) β π₯ β π¦) β§ π§ β {β
}) β (π§ = β
β¨ π§ = {β
})) |
86 | 85 | ex 115 |
. . 3
β’
(βπ₯βπ¦((π₯ βΌ π¦ β§ π¦ βΌ π₯) β π₯ β π¦) β (π§ β {β
} β (π§ = β
β¨ π§ = {β
}))) |
87 | 86 | alrimiv 1874 |
. 2
β’
(βπ₯βπ¦((π₯ βΌ π¦ β§ π¦ βΌ π₯) β π₯ β π¦) β βπ§(π§ β {β
} β (π§ = β
β¨ π§ = {β
}))) |
88 | | exmid01 4198 |
. 2
β’
(EXMID β βπ§(π§ β {β
} β (π§ = β
β¨ π§ = {β
}))) |
89 | 87, 88 | sylibr 134 |
1
β’
(βπ₯βπ¦((π₯ βΌ π¦ β§ π¦ βΌ π₯) β π₯ β π¦) β
EXMID) |