Metamath Proof Explorer

Theorem tcmin

Description: Defining property of the transitive closure function: it is a subset of any transitive class containing A . (Contributed by Mario Carneiro, 23-Jun-2013)

Ref Expression
Assertion tcmin 
|- ( A e. V -> ( ( A C_ B /\ Tr B ) -> ( TC ` A ) C_ B ) )

Proof

Step Hyp Ref Expression
1 tcvalg 
 |-  ( A e. V -> ( TC ` A ) = |^| { x | ( A C_ x /\ Tr x ) } )
2 fvex 
 |-  ( TC ` A ) e. _V
3 1 2 eqeltrrdi 
 |-  ( A e. V -> |^| { x | ( A C_ x /\ Tr x ) } e. _V )
4 intexab 
 |-  ( E. x ( A C_ x /\ Tr x ) <-> |^| { x | ( A C_ x /\ Tr x ) } e. _V )
5 3 4 sylibr 
 |-  ( A e. V -> E. x ( A C_ x /\ Tr x ) )
6 ssin 
 |-  ( ( A C_ x /\ A C_ B ) <-> A C_ ( x i^i B ) )
7 6 biimpi 
 |-  ( ( A C_ x /\ A C_ B ) -> A C_ ( x i^i B ) )
8 trin 
 |-  ( ( Tr x /\ Tr B ) -> Tr ( x i^i B ) )
9 7 8 anim12i 
 |-  ( ( ( A C_ x /\ A C_ B ) /\ ( Tr x /\ Tr B ) ) -> ( A C_ ( x i^i B ) /\ Tr ( x i^i B ) ) )
10 9 an4s 
 |-  ( ( ( A C_ x /\ Tr x ) /\ ( A C_ B /\ Tr B ) ) -> ( A C_ ( x i^i B ) /\ Tr ( x i^i B ) ) )
11 10 expcom 
 |-  ( ( A C_ B /\ Tr B ) -> ( ( A C_ x /\ Tr x ) -> ( A C_ ( x i^i B ) /\ Tr ( x i^i B ) ) ) )
12 vex 
 |-  x e. _V
13 12 inex1 
 |-  ( x i^i B ) e. _V
14 sseq2 
 |-  ( y = ( x i^i B ) -> ( A C_ y <-> A C_ ( x i^i B ) ) )
15 treq 
 |-  ( y = ( x i^i B ) -> ( Tr y <-> Tr ( x i^i B ) ) )
16 14 15 anbi12d 
 |-  ( y = ( x i^i B ) -> ( ( A C_ y /\ Tr y ) <-> ( A C_ ( x i^i B ) /\ Tr ( x i^i B ) ) ) )
17 13 16 elab 
 |-  ( ( x i^i B ) e. { y | ( A C_ y /\ Tr y ) } <-> ( A C_ ( x i^i B ) /\ Tr ( x i^i B ) ) )
18 intss1 
 |-  ( ( x i^i B ) e. { y | ( A C_ y /\ Tr y ) } -> |^| { y | ( A C_ y /\ Tr y ) } C_ ( x i^i B ) )
19 17 18 sylbir 
 |-  ( ( A C_ ( x i^i B ) /\ Tr ( x i^i B ) ) -> |^| { y | ( A C_ y /\ Tr y ) } C_ ( x i^i B ) )
20 inss2 
 |-  ( x i^i B ) C_ B
21 19 20 sstrdi 
 |-  ( ( A C_ ( x i^i B ) /\ Tr ( x i^i B ) ) -> |^| { y | ( A C_ y /\ Tr y ) } C_ B )
22 11 21 syl6 
 |-  ( ( A C_ B /\ Tr B ) -> ( ( A C_ x /\ Tr x ) -> |^| { y | ( A C_ y /\ Tr y ) } C_ B ) )
23 22 exlimdv 
 |-  ( ( A C_ B /\ Tr B ) -> ( E. x ( A C_ x /\ Tr x ) -> |^| { y | ( A C_ y /\ Tr y ) } C_ B ) )
24 5 23 syl5com 
 |-  ( A e. V -> ( ( A C_ B /\ Tr B ) -> |^| { y | ( A C_ y /\ Tr y ) } C_ B ) )
25 tcvalg 
 |-  ( A e. V -> ( TC ` A ) = |^| { y | ( A C_ y /\ Tr y ) } )
26 25 sseq1d 
 |-  ( A e. V -> ( ( TC ` A ) C_ B <-> |^| { y | ( A C_ y /\ Tr y ) } C_ B ) )
27 24 26 sylibrd 
 |-  ( A e. V -> ( ( A C_ B /\ Tr B ) -> ( TC ` A ) C_ B ) )