This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem tz9.1c

Description: Alternate expression for the existence of transitive closures tz9.1 : the intersection of all transitive sets containing A is a set. (Contributed by Mario Carneiro, 22-Mar-2013)

Ref Expression
Hypothesis tz9.1.1 ⊢ A ∈ V
Assertion tz9.1c ⊢ ⋂ x | A ⊆ x ∧ Tr ⁡ x ∈ V

Proof

Step Hyp Ref Expression
1 tz9.1.1 ⊢ A ∈ V
2 eqid ⊢ rec ⁡ z ∈ V ⟼ z ∪ ⋃ z A ↾ ω = rec ⁡ z ∈ V ⟼ z ∪ ⋃ z A ↾ ω
3 eqid ⊢ ⋃ w ∈ ω rec ⁡ z ∈ V ⟼ z ∪ ⋃ z A ↾ ω ⁡ w = ⋃ w ∈ ω rec ⁡ z ∈ V ⟼ z ∪ ⋃ z A ↾ ω ⁡ w
4 1 2 3 trcl ⊢ A ⊆ ⋃ w ∈ ω rec ⁡ z ∈ V ⟼ z ∪ ⋃ z A ↾ ω ⁡ w ∧ Tr ⁡ ⋃ w ∈ ω rec ⁡ z ∈ V ⟼ z ∪ ⋃ z A ↾ ω ⁡ w ∧ ∀ x A ⊆ x ∧ Tr ⁡ x → ⋃ w ∈ ω rec ⁡ z ∈ V ⟼ z ∪ ⋃ z A ↾ ω ⁡ w ⊆ x
5 3simpa ⊢ A ⊆ ⋃ w ∈ ω rec ⁡ z ∈ V ⟼ z ∪ ⋃ z A ↾ ω ⁡ w ∧ Tr ⁡ ⋃ w ∈ ω rec ⁡ z ∈ V ⟼ z ∪ ⋃ z A ↾ ω ⁡ w ∧ ∀ x A ⊆ x ∧ Tr ⁡ x → ⋃ w ∈ ω rec ⁡ z ∈ V ⟼ z ∪ ⋃ z A ↾ ω ⁡ w ⊆ x → A ⊆ ⋃ w ∈ ω rec ⁡ z ∈ V ⟼ z ∪ ⋃ z A ↾ ω ⁡ w ∧ Tr ⁡ ⋃ w ∈ ω rec ⁡ z ∈ V ⟼ z ∪ ⋃ z A ↾ ω ⁡ w
6 omex ⊢ ω ∈ V
7 fvex ⊢ rec ⁡ z ∈ V ⟼ z ∪ ⋃ z A ↾ ω ⁡ w ∈ V
8 6 7 iunex ⊢ ⋃ w ∈ ω rec ⁡ z ∈ V ⟼ z ∪ ⋃ z A ↾ ω ⁡ w ∈ V
9 sseq2 ⊢ x = ⋃ w ∈ ω rec ⁡ z ∈ V ⟼ z ∪ ⋃ z A ↾ ω ⁡ w → A ⊆ x ↔ A ⊆ ⋃ w ∈ ω rec ⁡ z ∈ V ⟼ z ∪ ⋃ z A ↾ ω ⁡ w
10 treq ⊢ x = ⋃ w ∈ ω rec ⁡ z ∈ V ⟼ z ∪ ⋃ z A ↾ ω ⁡ w → Tr ⁡ x ↔ Tr ⁡ ⋃ w ∈ ω rec ⁡ z ∈ V ⟼ z ∪ ⋃ z A ↾ ω ⁡ w
11 9 10 anbi12d ⊢ x = ⋃ w ∈ ω rec ⁡ z ∈ V ⟼ z ∪ ⋃ z A ↾ ω ⁡ w → A ⊆ x ∧ Tr ⁡ x ↔ A ⊆ ⋃ w ∈ ω rec ⁡ z ∈ V ⟼ z ∪ ⋃ z A ↾ ω ⁡ w ∧ Tr ⁡ ⋃ w ∈ ω rec ⁡ z ∈ V ⟼ z ∪ ⋃ z A ↾ ω ⁡ w
12 8 11 spcev ⊢ A ⊆ ⋃ w ∈ ω rec ⁡ z ∈ V ⟼ z ∪ ⋃ z A ↾ ω ⁡ w ∧ Tr ⁡ ⋃ w ∈ ω rec ⁡ z ∈ V ⟼ z ∪ ⋃ z A ↾ ω ⁡ w → ∃ x A ⊆ x ∧ Tr ⁡ x
13 4 5 12 mp2b ⊢ ∃ x A ⊆ x ∧ Tr ⁡ x
14 abn0 ⊢ x | A ⊆ x ∧ Tr ⁡ x ≠ ∅ ↔ ∃ x A ⊆ x ∧ Tr ⁡ x
15 13 14 mpbir ⊢ x | A ⊆ x ∧ Tr ⁡ x ≠ ∅
16 intex ⊢ x | A ⊆ x ∧ Tr ⁡ x ≠ ∅ ↔ ⋂ x | A ⊆ x ∧ Tr ⁡ x ∈ V
17 15 16 mpbi ⊢ ⋂ x | A ⊆ x ∧ Tr ⁡ x ∈ V