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