As discussed, I have a new version which preserves the proof structure, but weakens the premises about as much as possible. A1. The collection of all entities is a set E, with a causal relation C and a partial order P, such that x P y if and only if x is a part of y. Note: This merges the assumption that P is a partial order into the overall set-up; that feature of P now gets used earlier in the argument. A2. The set E can be well-ordered. This ensures we can apply Zorn's Lemma when considering chains in E, but is not as strong as the full Axiom of Choice. If the set E is finite or countable, for instance, then A2 applies automatically. Definitions: We define a relation C such that x C y iff there are entities v, w such that v P x, y P w and v C w. Note: This gives a broader causal relation which automatically satisfies "if x C y and x P z then z C y" as well as "if x C z and y P z then x C y", loosely "anything which is caused by a part is caused by the whole" and "anything which causes the whole, causes the part". So we don't need to state those as extra premises. We then define a further relation <= such that x <= y iff x = y, or there are finitely many entities x1, ..., xn such that x1 = x, xn = y and xi C* xi+1 for i=1.. n-1. Note: This construction ensures that <= is a pre-order on E. Say that a subset S of E is a "chain" iff for any x, y in S we have x <= y or y <= x. Say that S is an "endless chain" iff for any x in S there is some y in S distinct from x with y <= x. We shall say that y is "uncaused" if and only if there is no z in E distinct from y with z C* y (this of course implies there is no z distinct from y with z C y, but it also implies that y isn't part of anything which is caused by something distinct from y). Say that x is a proper part of y iff x is distinct from y but x P y. A3. Let S be any endless chain in E; then there is some z in E such that every x in S is a proper part of z. Lemma 1: For any chain S in E, there is an entity x

Looking over the "recipe" again, I notice one thing I failed to notice earlier; at no point have you formally defined the uncaused cause as God. That's a weak step, but if you actually want to use that argument to argue for monotheism (instead of merely the presence of an uncaused entity, nature unknown) then I think it's a necessary step. Some of the assumptions necessary to eliminate multiple uncaused causes are a bit weak, but I think that you have a very good argument that somewhere in the history of the universe there must be at least one uncaused cause of some sort.