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 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