Description: Every set has a transitive closure (the smallest transitive extension). Theorem 9.1 of TakeutiZaring p. 73. See trcl for an explicit expression for the transitive closure. Apparently open problems are whether this theorem can be proved without the Axiom of Infinity; if not, then whether it implies Infinity; and if not, what is the "property" that Infinity has that the other axioms don't have that is weaker than Infinity itself?
(Added 22-Mar-2011) The following article seems to answer the first question, that it can't be proved without Infinity, in the affirmative: Mancini, Antonella and Zambella, Domenico (2001). "A note on recursive models of set theories."Notre Dame Journal of Formal Logic, 42(2):109-115. (Thanks to Scott Fenton.) (Contributed by NM, 15-Sep-2003)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | tz9.1.1 | ⊢ 𝐴 ∈ V | |
| Assertion | tz9.1 | ⊢ ∃ 𝑥 ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀ 𝑦 ( ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) → 𝑥 ⊆ 𝑦 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | tz9.1.1 | ⊢ 𝐴 ∈ V | |
| 2 | omex | ⊢ ω ∈ V | |
| 3 | fvex | ⊢ ( ( rec ( ( 𝑤 ∈ V ↦ ( 𝑤 ∪ ∪ 𝑤 ) ) , 𝐴 ) ↾ ω ) ‘ 𝑧 ) ∈ V | |
| 4 | 2 3 | iunex | ⊢ ∪ 𝑧 ∈ ω ( ( rec ( ( 𝑤 ∈ V ↦ ( 𝑤 ∪ ∪ 𝑤 ) ) , 𝐴 ) ↾ ω ) ‘ 𝑧 ) ∈ V |
| 5 | sseq2 | ⊢ ( 𝑥 = ∪ 𝑧 ∈ ω ( ( rec ( ( 𝑤 ∈ V ↦ ( 𝑤 ∪ ∪ 𝑤 ) ) , 𝐴 ) ↾ ω ) ‘ 𝑧 ) → ( 𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ ∪ 𝑧 ∈ ω ( ( rec ( ( 𝑤 ∈ V ↦ ( 𝑤 ∪ ∪ 𝑤 ) ) , 𝐴 ) ↾ ω ) ‘ 𝑧 ) ) ) | |
| 6 | treq | ⊢ ( 𝑥 = ∪ 𝑧 ∈ ω ( ( rec ( ( 𝑤 ∈ V ↦ ( 𝑤 ∪ ∪ 𝑤 ) ) , 𝐴 ) ↾ ω ) ‘ 𝑧 ) → ( Tr 𝑥 ↔ Tr ∪ 𝑧 ∈ ω ( ( rec ( ( 𝑤 ∈ V ↦ ( 𝑤 ∪ ∪ 𝑤 ) ) , 𝐴 ) ↾ ω ) ‘ 𝑧 ) ) ) | |
| 7 | sseq1 | ⊢ ( 𝑥 = ∪ 𝑧 ∈ ω ( ( rec ( ( 𝑤 ∈ V ↦ ( 𝑤 ∪ ∪ 𝑤 ) ) , 𝐴 ) ↾ ω ) ‘ 𝑧 ) → ( 𝑥 ⊆ 𝑦 ↔ ∪ 𝑧 ∈ ω ( ( rec ( ( 𝑤 ∈ V ↦ ( 𝑤 ∪ ∪ 𝑤 ) ) , 𝐴 ) ↾ ω ) ‘ 𝑧 ) ⊆ 𝑦 ) ) | |
| 8 | 7 | imbi2d | ⊢ ( 𝑥 = ∪ 𝑧 ∈ ω ( ( rec ( ( 𝑤 ∈ V ↦ ( 𝑤 ∪ ∪ 𝑤 ) ) , 𝐴 ) ↾ ω ) ‘ 𝑧 ) → ( ( ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) → 𝑥 ⊆ 𝑦 ) ↔ ( ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) → ∪ 𝑧 ∈ ω ( ( rec ( ( 𝑤 ∈ V ↦ ( 𝑤 ∪ ∪ 𝑤 ) ) , 𝐴 ) ↾ ω ) ‘ 𝑧 ) ⊆ 𝑦 ) ) ) |
| 9 | 8 | albidv | ⊢ ( 𝑥 = ∪ 𝑧 ∈ ω ( ( rec ( ( 𝑤 ∈ V ↦ ( 𝑤 ∪ ∪ 𝑤 ) ) , 𝐴 ) ↾ ω ) ‘ 𝑧 ) → ( ∀ 𝑦 ( ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) → 𝑥 ⊆ 𝑦 ) ↔ ∀ 𝑦 ( ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) → ∪ 𝑧 ∈ ω ( ( rec ( ( 𝑤 ∈ V ↦ ( 𝑤 ∪ ∪ 𝑤 ) ) , 𝐴 ) ↾ ω ) ‘ 𝑧 ) ⊆ 𝑦 ) ) ) |
| 10 | 5 6 9 | 3anbi123d | ⊢ ( 𝑥 = ∪ 𝑧 ∈ ω ( ( rec ( ( 𝑤 ∈ V ↦ ( 𝑤 ∪ ∪ 𝑤 ) ) , 𝐴 ) ↾ ω ) ‘ 𝑧 ) → ( ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀ 𝑦 ( ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) → 𝑥 ⊆ 𝑦 ) ) ↔ ( 𝐴 ⊆ ∪ 𝑧 ∈ ω ( ( rec ( ( 𝑤 ∈ V ↦ ( 𝑤 ∪ ∪ 𝑤 ) ) , 𝐴 ) ↾ ω ) ‘ 𝑧 ) ∧ Tr ∪ 𝑧 ∈ ω ( ( rec ( ( 𝑤 ∈ V ↦ ( 𝑤 ∪ ∪ 𝑤 ) ) , 𝐴 ) ↾ ω ) ‘ 𝑧 ) ∧ ∀ 𝑦 ( ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) → ∪ 𝑧 ∈ ω ( ( rec ( ( 𝑤 ∈ V ↦ ( 𝑤 ∪ ∪ 𝑤 ) ) , 𝐴 ) ↾ ω ) ‘ 𝑧 ) ⊆ 𝑦 ) ) ) ) |
| 11 | eqid | ⊢ ( rec ( ( 𝑤 ∈ V ↦ ( 𝑤 ∪ ∪ 𝑤 ) ) , 𝐴 ) ↾ ω ) = ( rec ( ( 𝑤 ∈ V ↦ ( 𝑤 ∪ ∪ 𝑤 ) ) , 𝐴 ) ↾ ω ) | |
| 12 | eqid | ⊢ ∪ 𝑧 ∈ ω ( ( rec ( ( 𝑤 ∈ V ↦ ( 𝑤 ∪ ∪ 𝑤 ) ) , 𝐴 ) ↾ ω ) ‘ 𝑧 ) = ∪ 𝑧 ∈ ω ( ( rec ( ( 𝑤 ∈ V ↦ ( 𝑤 ∪ ∪ 𝑤 ) ) , 𝐴 ) ↾ ω ) ‘ 𝑧 ) | |
| 13 | 1 11 12 | trcl | ⊢ ( 𝐴 ⊆ ∪ 𝑧 ∈ ω ( ( rec ( ( 𝑤 ∈ V ↦ ( 𝑤 ∪ ∪ 𝑤 ) ) , 𝐴 ) ↾ ω ) ‘ 𝑧 ) ∧ Tr ∪ 𝑧 ∈ ω ( ( rec ( ( 𝑤 ∈ V ↦ ( 𝑤 ∪ ∪ 𝑤 ) ) , 𝐴 ) ↾ ω ) ‘ 𝑧 ) ∧ ∀ 𝑦 ( ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) → ∪ 𝑧 ∈ ω ( ( rec ( ( 𝑤 ∈ V ↦ ( 𝑤 ∪ ∪ 𝑤 ) ) , 𝐴 ) ↾ ω ) ‘ 𝑧 ) ⊆ 𝑦 ) ) |
| 14 | 4 10 13 | ceqsexv2d | ⊢ ∃ 𝑥 ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀ 𝑦 ( ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) → 𝑥 ⊆ 𝑦 ) ) |