This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem tcel

Description: The transitive closure function converts the element relation to the subset relation. (Contributed by Mario Carneiro, 23-Jun-2013)

Ref Expression
Hypothesis tc2.1 
|- A e. _V
Assertion tcel 
|- ( B e. A -> ( TC ` B ) C_ ( TC ` A ) )

Proof

Step Hyp Ref Expression
1 tc2.1 
 |-  A e. _V
2 tcvalg 
 |-  ( B e. A -> ( TC ` B ) = |^| { x | ( B C_ x /\ Tr x ) } )
3 ssel 
 |-  ( A C_ x -> ( B e. A -> B e. x ) )
4 trss 
 |-  ( Tr x -> ( B e. x -> B C_ x ) )
5 4 com12 
 |-  ( B e. x -> ( Tr x -> B C_ x ) )
6 3 5 syl6com 
 |-  ( B e. A -> ( A C_ x -> ( Tr x -> B C_ x ) ) )
7 6 impd 
 |-  ( B e. A -> ( ( A C_ x /\ Tr x ) -> B C_ x ) )
8 simpr 
 |-  ( ( A C_ x /\ Tr x ) -> Tr x )
9 7 8 jca2 
 |-  ( B e. A -> ( ( A C_ x /\ Tr x ) -> ( B C_ x /\ Tr x ) ) )
10 9 ss2abdv 
 |-  ( B e. A -> { x | ( A C_ x /\ Tr x ) } C_ { x | ( B C_ x /\ Tr x ) } )
11 intss 
 |-  ( { x | ( A C_ x /\ Tr x ) } C_ { x | ( B C_ x /\ Tr x ) } -> |^| { x | ( B C_ x /\ Tr x ) } C_ |^| { x | ( A C_ x /\ Tr x ) } )
12 10 11 syl 
 |-  ( B e. A -> |^| { x | ( B C_ x /\ Tr x ) } C_ |^| { x | ( A C_ x /\ Tr x ) } )
13 tcvalg 
 |-  ( A e. _V -> ( TC ` A ) = |^| { x | ( A C_ x /\ Tr x ) } )
14 1 13 ax-mp 
 |-  ( TC ` A ) = |^| { x | ( A C_ x /\ Tr x ) }
15 12 14 sseqtrrdi 
 |-  ( B e. A -> |^| { x | ( B C_ x /\ Tr x ) } C_ ( TC ` A ) )
16 2 15 eqsstrd 
 |-  ( B e. A -> ( TC ` B ) C_ ( TC ` A ) )