# 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}\in \mathrm{V}$
Assertion tcel ${⊢}{B}\in {A}\to \mathrm{TC}\left({B}\right)\subseteq \mathrm{TC}\left({A}\right)$

### Proof

Step Hyp Ref Expression
1 tc2.1 ${⊢}{A}\in \mathrm{V}$
2 tcvalg ${⊢}{B}\in {A}\to \mathrm{TC}\left({B}\right)=\bigcap \left\{{x}|\left({B}\subseteq {x}\wedge \mathrm{Tr}{x}\right)\right\}$
3 ssel ${⊢}{A}\subseteq {x}\to \left({B}\in {A}\to {B}\in {x}\right)$
4 trss ${⊢}\mathrm{Tr}{x}\to \left({B}\in {x}\to {B}\subseteq {x}\right)$
5 4 com12 ${⊢}{B}\in {x}\to \left(\mathrm{Tr}{x}\to {B}\subseteq {x}\right)$
6 3 5 syl6com ${⊢}{B}\in {A}\to \left({A}\subseteq {x}\to \left(\mathrm{Tr}{x}\to {B}\subseteq {x}\right)\right)$
7 6 impd ${⊢}{B}\in {A}\to \left(\left({A}\subseteq {x}\wedge \mathrm{Tr}{x}\right)\to {B}\subseteq {x}\right)$
8 simpr ${⊢}\left({A}\subseteq {x}\wedge \mathrm{Tr}{x}\right)\to \mathrm{Tr}{x}$
9 7 8 jca2 ${⊢}{B}\in {A}\to \left(\left({A}\subseteq {x}\wedge \mathrm{Tr}{x}\right)\to \left({B}\subseteq {x}\wedge \mathrm{Tr}{x}\right)\right)$
10 9 ss2abdv ${⊢}{B}\in {A}\to \left\{{x}|\left({A}\subseteq {x}\wedge \mathrm{Tr}{x}\right)\right\}\subseteq \left\{{x}|\left({B}\subseteq {x}\wedge \mathrm{Tr}{x}\right)\right\}$
11 intss ${⊢}\left\{{x}|\left({A}\subseteq {x}\wedge \mathrm{Tr}{x}\right)\right\}\subseteq \left\{{x}|\left({B}\subseteq {x}\wedge \mathrm{Tr}{x}\right)\right\}\to \bigcap \left\{{x}|\left({B}\subseteq {x}\wedge \mathrm{Tr}{x}\right)\right\}\subseteq \bigcap \left\{{x}|\left({A}\subseteq {x}\wedge \mathrm{Tr}{x}\right)\right\}$
12 10 11 syl ${⊢}{B}\in {A}\to \bigcap \left\{{x}|\left({B}\subseteq {x}\wedge \mathrm{Tr}{x}\right)\right\}\subseteq \bigcap \left\{{x}|\left({A}\subseteq {x}\wedge \mathrm{Tr}{x}\right)\right\}$
13 tcvalg ${⊢}{A}\in \mathrm{V}\to \mathrm{TC}\left({A}\right)=\bigcap \left\{{x}|\left({A}\subseteq {x}\wedge \mathrm{Tr}{x}\right)\right\}$
14 1 13 ax-mp ${⊢}\mathrm{TC}\left({A}\right)=\bigcap \left\{{x}|\left({A}\subseteq {x}\wedge \mathrm{Tr}{x}\right)\right\}$
15 12 14 sseqtrrdi ${⊢}{B}\in {A}\to \bigcap \left\{{x}|\left({B}\subseteq {x}\wedge \mathrm{Tr}{x}\right)\right\}\subseteq \mathrm{TC}\left({A}\right)$
16 2 15 eqsstrd ${⊢}{B}\in {A}\to \mathrm{TC}\left({B}\right)\subseteq \mathrm{TC}\left({A}\right)$