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 ⊢ 𝐴 ∈ V
Assertion tcel ( 𝐵 ∈ 𝐴 → ( TC ‘ 𝐵 ) ⊆ ( TC ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 tc2.1 ⊢ 𝐴 ∈ V
2 tcvalg ⊢ ( 𝐵 ∈ 𝐴 → ( TC ‘ 𝐵 ) = ∩ { 𝑥 ∣ ( 𝐵 ⊆ 𝑥 ∧ Tr 𝑥 ) } )
3 ssel ⊢ ( 𝐴 ⊆ 𝑥 → ( 𝐵 ∈ 𝐴 → 𝐵 ∈ 𝑥 ) )
4 trss ⊢ ( Tr 𝑥 → ( 𝐵 ∈ 𝑥 → 𝐵 ⊆ 𝑥 ) )
5 4 com12 ⊢ ( 𝐵 ∈ 𝑥 → ( Tr 𝑥 → 𝐵 ⊆ 𝑥 ) )
6 3 5 syl6com ⊢ ( 𝐵 ∈ 𝐴 → ( 𝐴 ⊆ 𝑥 → ( Tr 𝑥 → 𝐵 ⊆ 𝑥 ) ) )
7 6 impd ⊢ ( 𝐵 ∈ 𝐴 → ( ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ) → 𝐵 ⊆ 𝑥 ) )
8 simpr ⊢ ( ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ) → Tr 𝑥 )
9 7 8 jca2 ⊢ ( 𝐵 ∈ 𝐴 → ( ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ) → ( 𝐵 ⊆ 𝑥 ∧ Tr 𝑥 ) ) )
10 9 ss2abdv ⊢ ( 𝐵 ∈ 𝐴 → { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ) } ⊆ { 𝑥 ∣ ( 𝐵 ⊆ 𝑥 ∧ Tr 𝑥 ) } )
11 intss ⊢ ( { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ) } ⊆ { 𝑥 ∣ ( 𝐵 ⊆ 𝑥 ∧ Tr 𝑥 ) } → ∩ { 𝑥 ∣ ( 𝐵 ⊆ 𝑥 ∧ Tr 𝑥 ) } ⊆ ∩ { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ) } )
12 10 11 syl ⊢ ( 𝐵 ∈ 𝐴 → ∩ { 𝑥 ∣ ( 𝐵 ⊆ 𝑥 ∧ Tr 𝑥 ) } ⊆ ∩ { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ) } )
13 tcvalg ⊢ ( 𝐴 ∈ V → ( TC ‘ 𝐴 ) = ∩ { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ) } )
14 1 13 ax-mp ⊢ ( TC ‘ 𝐴 ) = ∩ { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ) }
15 12 14 sseqtrrdi ⊢ ( 𝐵 ∈ 𝐴 → ∩ { 𝑥 ∣ ( 𝐵 ⊆ 𝑥 ∧ Tr 𝑥 ) } ⊆ ( TC ‘ 𝐴 ) )
16 2 15 eqsstrd ⊢ ( 𝐵 ∈ 𝐴 → ( TC ‘ 𝐵 ) ⊆ ( TC ‘ 𝐴 ) )