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 e. _V
Assertion	tz9.1c	|- |^| { x | ( A C_ x /\ Tr x ) } e. _V

Proof

Step	Hyp	Ref	Expression
1		tz9.1.1	|- A e. _V
2		eqid	|- ( rec ( ( z e. _V |-> ( z u. U. z ) ) , A ) |` _om ) = ( rec ( ( z e. _V |-> ( z u. U. z ) ) , A ) |` _om )
3		eqid	|- U_ w e. _om ( ( rec ( ( z e. _V |-> ( z u. U. z ) ) , A ) |` _om ) ` w ) = U_ w e. _om ( ( rec ( ( z e. _V |-> ( z u. U. z ) ) , A ) |` _om ) ` w )
4	1 2 3	trcl	|- ( A C_ U_ w e. _om ( ( rec ( ( z e. _V |-> ( z u. U. z ) ) , A ) |` _om ) ` w ) /\ Tr U_ w e. _om ( ( rec ( ( z e. _V |-> ( z u. U. z ) ) , A ) |` _om ) ` w ) /\ A. x ( ( A C_ x /\ Tr x ) -> U_ w e. _om ( ( rec ( ( z e. _V |-> ( z u. U. z ) ) , A ) |` _om ) ` w ) C_ x ) )
5		3simpa	|- ( ( A C_ U_ w e. _om ( ( rec ( ( z e. _V |-> ( z u. U. z ) ) , A ) |` _om ) ` w ) /\ Tr U_ w e. _om ( ( rec ( ( z e. _V |-> ( z u. U. z ) ) , A ) |` _om ) ` w ) /\ A. x ( ( A C_ x /\ Tr x ) -> U_ w e. _om ( ( rec ( ( z e. _V |-> ( z u. U. z ) ) , A ) |` _om ) ` w ) C_ x ) ) -> ( A C_ U_ w e. _om ( ( rec ( ( z e. _V |-> ( z u. U. z ) ) , A ) |` _om ) ` w ) /\ Tr U_ w e. _om ( ( rec ( ( z e. _V |-> ( z u. U. z ) ) , A ) |` _om ) ` w ) ) )
6		omex	|- _om e. _V
7		fvex	|- ( ( rec ( ( z e. _V |-> ( z u. U. z ) ) , A ) |` _om ) ` w ) e. _V
8	6 7	iunex	|- U_ w e. _om ( ( rec ( ( z e. _V |-> ( z u. U. z ) ) , A ) |` _om ) ` w ) e. _V
9		sseq2	|- ( x = U_ w e. _om ( ( rec ( ( z e. _V |-> ( z u. U. z ) ) , A ) |` _om ) ` w ) -> ( A C_ x <-> A C_ U_ w e. _om ( ( rec ( ( z e. _V |-> ( z u. U. z ) ) , A ) |` _om ) ` w ) ) )
10		treq	|- ( x = U_ w e. _om ( ( rec ( ( z e. _V |-> ( z u. U. z ) ) , A ) |` _om ) ` w ) -> ( Tr x <-> Tr U_ w e. _om ( ( rec ( ( z e. _V |-> ( z u. U. z ) ) , A ) |` _om ) ` w ) ) )
11	9 10	anbi12d	|- ( x = U_ w e. _om ( ( rec ( ( z e. _V |-> ( z u. U. z ) ) , A ) |` _om ) ` w ) -> ( ( A C_ x /\ Tr x ) <-> ( A C_ U_ w e. _om ( ( rec ( ( z e. _V |-> ( z u. U. z ) ) , A ) |` _om ) ` w ) /\ Tr U_ w e. _om ( ( rec ( ( z e. _V |-> ( z u. U. z ) ) , A ) |` _om ) ` w ) ) ) )
12	8 11	spcev	|- ( ( A C_ U_ w e. _om ( ( rec ( ( z e. _V |-> ( z u. U. z ) ) , A ) |` _om ) ` w ) /\ Tr U_ w e. _om ( ( rec ( ( z e. _V |-> ( z u. U. z ) ) , A ) |` _om ) ` w ) ) -> E. x ( A C_ x /\ Tr x ) )
13	4 5 12	mp2b	|- E. x ( A C_ x /\ Tr x )
14		abn0	|- ( { x | ( A C_ x /\ Tr x ) } =/= (/) <-> E. x ( A C_ x /\ Tr x ) )
15	13 14	mpbir	|- { x | ( A C_ x /\ Tr x ) } =/= (/)
16		intex	|- ( { x | ( A C_ x /\ Tr x ) } =/= (/) <-> |^| { x | ( A C_ x /\ Tr x ) } e. _V )
17	15 16	mpbi	|- |^| { x | ( A C_ x /\ Tr x ) } e. _V