Axiom ax-tco 36660

Description: The Axiom of Transitive Containment of ZF set theory. It was derived as axtco 36659 above and is therefore redundant if we assume ax-ext 2709, ax-rep 5212 and ax-inf2 9551, but we state it as a separate axiom here so that its uses can be identified more easily. It states that a transitive set 𝑦 exists that contains a given set 𝑥. In particular, the transitive closure of 𝑥 is a set, since it is a subset of 𝑦, see df-tc 9645.

Traditionally, this statement is not counted as an axiom at all, but as a theorem from Replacement and Infinity. In fact, from the transitive closure of 𝑥 we can construct the set of iterated unions of 𝑥 (and vice versa), and Skolem took the existence of the latter set as a motivation for introducing the Axiom of Replacement. But Transitive Containment is strictly weaker than either of those axioms, so many authors identify it as its own axiom when investigating subsystems of ZF, such as Zermelo set theory or finitist set theory. We follow this separation in order to avoid nonessential usage of the stronger axioms.

There are two main versions of this axiom that appear in the literature: the strong form ⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ Tr 𝑦), see axtco1 36661 and axtco1g 36664, and the weak form ⊢ ∃𝑦(𝑥 ⊆ 𝑦 ∧ Tr 𝑦), see axtco2 36662 and axtco2g 36665. The weak form follows directly from the strong form, see axtco2 36662. But the strong form only follows from the weak form if we allow el 5383 or one of its variants, see axtco1from2 36663. We take the strong form here as the axiom, since it is slightly shorter when expanded to primitive symbols. Yet the weak form turns out to be more suitable for axtcond 36666 for reasons of syntax. (Contributed by Matthew House, 6-Apr-2026.)

Assertion

Ref	Expression
ax-tco	⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)))

Distinct variable group:   𝑥,𝑤,𝑦,𝑧

Detailed syntax breakdown of Axiom ax-tco

Step	Hyp	Ref	Expression
1		vx	. . . 4 setvar 𝑥
2		vy	. . . 4 setvar 𝑦
3	1, 2	wel 2115	. . 3 wff 𝑥 ∈ 𝑦
4		vz	. . . . . 6 setvar 𝑧
5	4, 2	wel 2115	. . . . 5 wff 𝑧 ∈ 𝑦
6		vw	. . . . . . . 8 setvar 𝑤
7	6, 4	wel 2115	. . . . . . 7 wff 𝑤 ∈ 𝑧
8	6, 2	wel 2115	. . . . . . 7 wff 𝑤 ∈ 𝑦
9	7, 8	wi 4	. . . . . 6 wff (𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)
10	9, 6	wal 1540	. . . . 5 wff ∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)
11	5, 10	wi 4	. . . 4 wff (𝑧 ∈ 𝑦 → ∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦))
12	11, 4	wal 1540	. . 3 wff ∀𝑧(𝑧 ∈ 𝑦 → ∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦))
13	3, 12	wa 395	. 2 wff (𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)))
14	13, 2	wex 1781	1 wff ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)))

This axiom is referenced by:  axtco1  36661  axuntco  36667  axnultcoreg  36668  elALTtco  36669