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 ⊢ 𝐴 ∈ V
Assertion tz9.1c ∩ { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ) } ∈ V

Proof

Step Hyp Ref Expression
1 tz9.1.1 ⊢ 𝐴 ∈ V
2 eqid ⊢ ( rec ( ( 𝑧 ∈ V ↦ ( 𝑧 ∪ ∪ 𝑧 ) ) , 𝐴 ) ↾ ω ) = ( rec ( ( 𝑧 ∈ V ↦ ( 𝑧 ∪ ∪ 𝑧 ) ) , 𝐴 ) ↾ ω )
3 eqid ⊢ ∪ 𝑤 ∈ ω ( ( rec ( ( 𝑧 ∈ V ↦ ( 𝑧 ∪ ∪ 𝑧 ) ) , 𝐴 ) ↾ ω ) ‘ 𝑤 ) = ∪ 𝑤 ∈ ω ( ( rec ( ( 𝑧 ∈ V ↦ ( 𝑧 ∪ ∪ 𝑧 ) ) , 𝐴 ) ↾ ω ) ‘ 𝑤 )
4 1 2 3 trcl ⊢ ( 𝐴 ⊆ ∪ 𝑤 ∈ ω ( ( rec ( ( 𝑧 ∈ V ↦ ( 𝑧 ∪ ∪ 𝑧 ) ) , 𝐴 ) ↾ ω ) ‘ 𝑤 ) ∧ Tr ∪ 𝑤 ∈ ω ( ( rec ( ( 𝑧 ∈ V ↦ ( 𝑧 ∪ ∪ 𝑧 ) ) , 𝐴 ) ↾ ω ) ‘ 𝑤 ) ∧ ∀ 𝑥 ( ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ) → ∪ 𝑤 ∈ ω ( ( rec ( ( 𝑧 ∈ V ↦ ( 𝑧 ∪ ∪ 𝑧 ) ) , 𝐴 ) ↾ ω ) ‘ 𝑤 ) ⊆ 𝑥 ) )
5 3simpa ⊢ ( ( 𝐴 ⊆ ∪ 𝑤 ∈ ω ( ( rec ( ( 𝑧 ∈ V ↦ ( 𝑧 ∪ ∪ 𝑧 ) ) , 𝐴 ) ↾ ω ) ‘ 𝑤 ) ∧ Tr ∪ 𝑤 ∈ ω ( ( rec ( ( 𝑧 ∈ V ↦ ( 𝑧 ∪ ∪ 𝑧 ) ) , 𝐴 ) ↾ ω ) ‘ 𝑤 ) ∧ ∀ 𝑥 ( ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ) → ∪ 𝑤 ∈ ω ( ( rec ( ( 𝑧 ∈ V ↦ ( 𝑧 ∪ ∪ 𝑧 ) ) , 𝐴 ) ↾ ω ) ‘ 𝑤 ) ⊆ 𝑥 ) ) → ( 𝐴 ⊆ ∪ 𝑤 ∈ ω ( ( rec ( ( 𝑧 ∈ V ↦ ( 𝑧 ∪ ∪ 𝑧 ) ) , 𝐴 ) ↾ ω ) ‘ 𝑤 ) ∧ Tr ∪ 𝑤 ∈ ω ( ( rec ( ( 𝑧 ∈ V ↦ ( 𝑧 ∪ ∪ 𝑧 ) ) , 𝐴 ) ↾ ω ) ‘ 𝑤 ) ) )
6 omex ⊢ ω ∈ V
7 fvex ⊢ ( ( rec ( ( 𝑧 ∈ V ↦ ( 𝑧 ∪ ∪ 𝑧 ) ) , 𝐴 ) ↾ ω ) ‘ 𝑤 ) ∈ V
8 6 7 iunex ⊢ ∪ 𝑤 ∈ ω ( ( rec ( ( 𝑧 ∈ V ↦ ( 𝑧 ∪ ∪ 𝑧 ) ) , 𝐴 ) ↾ ω ) ‘ 𝑤 ) ∈ V
9 sseq2 ⊢ ( 𝑥 = ∪ 𝑤 ∈ ω ( ( rec ( ( 𝑧 ∈ V ↦ ( 𝑧 ∪ ∪ 𝑧 ) ) , 𝐴 ) ↾ ω ) ‘ 𝑤 ) → ( 𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ ∪ 𝑤 ∈ ω ( ( rec ( ( 𝑧 ∈ V ↦ ( 𝑧 ∪ ∪ 𝑧 ) ) , 𝐴 ) ↾ ω ) ‘ 𝑤 ) ) )
10 treq ⊢ ( 𝑥 = ∪ 𝑤 ∈ ω ( ( rec ( ( 𝑧 ∈ V ↦ ( 𝑧 ∪ ∪ 𝑧 ) ) , 𝐴 ) ↾ ω ) ‘ 𝑤 ) → ( Tr 𝑥 ↔ Tr ∪ 𝑤 ∈ ω ( ( rec ( ( 𝑧 ∈ V ↦ ( 𝑧 ∪ ∪ 𝑧 ) ) , 𝐴 ) ↾ ω ) ‘ 𝑤 ) ) )
11 9 10 anbi12d ⊢ ( 𝑥 = ∪ 𝑤 ∈ ω ( ( rec ( ( 𝑧 ∈ V ↦ ( 𝑧 ∪ ∪ 𝑧 ) ) , 𝐴 ) ↾ ω ) ‘ 𝑤 ) → ( ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ) ↔ ( 𝐴 ⊆ ∪ 𝑤 ∈ ω ( ( rec ( ( 𝑧 ∈ V ↦ ( 𝑧 ∪ ∪ 𝑧 ) ) , 𝐴 ) ↾ ω ) ‘ 𝑤 ) ∧ Tr ∪ 𝑤 ∈ ω ( ( rec ( ( 𝑧 ∈ V ↦ ( 𝑧 ∪ ∪ 𝑧 ) ) , 𝐴 ) ↾ ω ) ‘ 𝑤 ) ) ) )
12 8 11 spcev ⊢ ( ( 𝐴 ⊆ ∪ 𝑤 ∈ ω ( ( rec ( ( 𝑧 ∈ V ↦ ( 𝑧 ∪ ∪ 𝑧 ) ) , 𝐴 ) ↾ ω ) ‘ 𝑤 ) ∧ Tr ∪ 𝑤 ∈ ω ( ( rec ( ( 𝑧 ∈ V ↦ ( 𝑧 ∪ ∪ 𝑧 ) ) , 𝐴 ) ↾ ω ) ‘ 𝑤 ) ) → ∃ 𝑥 ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ) )
13 4 5 12 mp2b ⊢ ∃ 𝑥 ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 )
14 abn0 ⊢ ( { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ) } ≠ ∅ ↔ ∃ 𝑥 ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ) )
15 13 14 mpbir ⊢ { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ) } ≠ ∅
16 intex ⊢ ( { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ) } ≠ ∅ ↔ ∩ { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ) } ∈ V )
17 15 16 mpbi ⊢ ∩ { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ) } ∈ V