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 ∈ V
Assertion tcel ⊢ B ∈ A → TC ⁡ B ⊆ TC ⁡ A

Proof

Step Hyp Ref Expression
1 tc2.1 ⊢ A ∈ V
2 tcvalg ⊢ B ∈ A → TC ⁡ B = ⋂ x | B ⊆ x ∧ Tr ⁡ x
3 ssel ⊢ A ⊆ x → B ∈ A → B ∈ x
4 trss ⊢ Tr ⁡ x → B ∈ x → B ⊆ x
5 4 com12 ⊢ B ∈ x → Tr ⁡ x → B ⊆ x
6 3 5 syl6com ⊢ B ∈ A → A ⊆ x → Tr ⁡ x → B ⊆ x
7 6 impd ⊢ B ∈ A → A ⊆ x ∧ Tr ⁡ x → B ⊆ x
8 simpr ⊢ A ⊆ x ∧ Tr ⁡ x → Tr ⁡ x
9 7 8 jca2 ⊢ B ∈ A → A ⊆ x ∧ Tr ⁡ x → B ⊆ x ∧ Tr ⁡ x
10 9 ss2abdv ⊢ B ∈ A → x | A ⊆ x ∧ Tr ⁡ x ⊆ x | B ⊆ x ∧ Tr ⁡ x
11 intss ⊢ x | A ⊆ x ∧ Tr ⁡ x ⊆ x | B ⊆ x ∧ Tr ⁡ x → ⋂ x | B ⊆ x ∧ Tr ⁡ x ⊆ ⋂ x | A ⊆ x ∧ Tr ⁡ x
12 10 11 syl ⊢ B ∈ A → ⋂ x | B ⊆ x ∧ Tr ⁡ x ⊆ ⋂ x | A ⊆ x ∧ Tr ⁡ x
13 tcvalg ⊢ A ∈ V → TC ⁡ A = ⋂ x | A ⊆ x ∧ Tr ⁡ x
14 1 13 ax-mp ⊢ TC ⁡ A = ⋂ x | A ⊆ x ∧ Tr ⁡ x
15 12 14 sseqtrrdi ⊢ B ∈ A → ⋂ x | B ⊆ x ∧ Tr ⁡ x ⊆ TC ⁡ A
16 2 15 eqsstrd ⊢ B ∈ A → TC ⁡ B ⊆ TC ⁡ A