[proofplan] We prove the contrapositive. Jensen's covering lemma for $L$ states that if $0^\sharp$ does not exist, then every uncountable set of ordinals in $V$ is contained in a constructible set of the same $V$-cardinality. Applying this covering conclusion to the alleged counterexample $X$ produces exactly the set $Y \in L$ whose nonexistence is assumed. Hence a failure of Jensen covering is incompatible with the nonexistence of $0^\sharp$. [/proofplan] [step:Assume $0^\sharp$ does not exist and recall Jensen covering] Argue contrapositively. Assume that $0^\sharp$ does not exist. By Jensen's covering lemma for $L$ (citing a result not yet in the wiki: Jensen covering lemma for $L$), for every uncountable set $A \subset \operatorname{Ord}$ there exists a set $B \in L$ such that $A \subset B$ and $|B| = |A|$, with cardinalities computed in $V$. [/step] [step:Apply covering to the alleged failure set] Let $X \subset \operatorname{Ord}$ be an uncountable set. Applying Jensen's covering lemma with $A := X$, there exists a set $Y \in L$ such that $X \subset Y$ and $|Y| = |X|$. [guided] The contrapositive assumption $0^\sharp$ does not exist is used only through Jensen's covering lemma. The lemma applies to $X$ because $X$ is an uncountable set of ordinals in the ambient universe $V$. Its conclusion gives a constructible set $Y \in L$ with two properties: first, $X \subset Y$, so $Y$ covers $X$; second, $|Y| = |X|$, so the cover does not increase cardinality in $V$. Thus, for this particular uncountable set $X \subset \operatorname{Ord}$, the covering conclusion holds. Since $X$ was arbitrary among uncountable sets of ordinals, the nonexistence of $0^\sharp$ implies Jensen's covering conclusion for every such $X$. [/guided] [/step] [step:Conclude the contrapositive] Therefore, if $0^\sharp$ does not exist, there is no uncountable set $X \subset \operatorname{Ord}$ such that every $Y \in L$ with $X \subset Y$ satisfies $|Y| \ne |X|$. Equivalently, if such an uncountable set $X$ exists, then the assumption that $0^\sharp$ does not exist is false. Hence $0^\sharp$ exists. [/step]