「Lの元はZFCから存在証明可能」は偽だけどね。
直接的理由として、Lにおける「定義可能」とは「集合論の言語で書ける論理式によって定義可能」ではないから。
間接的理由として、Lは非可算だが証明全体の集まりはたかだか可算だから。