关于“存在单射函数f:A→B（B为可数集）时A至多可数”的严谨证明问询

我一开始是这么推导的：

假设集合A不是至多可数的，也就是A是不可数集。那按我的理解，这意味着$|A| > |B|$。而单射函数的核心要求是一一对应——A中的每个元素都要映射到B中唯一的元素，如果A的“基数”比B大，那根本不可能存在这样的单射函数，因为必然会有多个A中的元素对应到同一个B中的元素，这就和题目给出的“存在单射函数$f:A \to B$”这个前提矛盾了。所以结论应该是A必须是至多可数的。

不过我总觉得这个证明从第一步断言$|A| > |B|$的时候就不够严谨。虽然直觉上觉得不同“大小”的无穷之间有大小关系，但直接这么说是不是太草率了？有没有大佬能给我指个方向，怎么把这个证明做得更严谨、更符合集合论的规范？谢谢啦！

注：本文中“可数”等价于“可数无穷”。

备注：内容来源于stack exchange，提问作者robert lewison