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

Metamath Proof Explorer

Theorem tcss

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

Ref Expression
Hypothesis tc2.1 ⊢ 𝐴 ∈ V
Assertion tcss ( 𝐵 ⊆ 𝐴 → ( TC ‘ 𝐵 ) ⊆ ( TC ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 tc2.1 ⊢ 𝐴 ∈ V
2 1 ssex ⊢ ( 𝐵 ⊆ 𝐴 → 𝐵 ∈ V )
3 tcvalg ⊢ ( 𝐵 ∈ V → ( TC ‘ 𝐵 ) = ∩ { 𝑥 ∣ ( 𝐵 ⊆ 𝑥 ∧ Tr 𝑥 ) } )
4 2 3 syl ⊢ ( 𝐵 ⊆ 𝐴 → ( TC ‘ 𝐵 ) = ∩ { 𝑥 ∣ ( 𝐵 ⊆ 𝑥 ∧ Tr 𝑥 ) } )
5 sstr2 ⊢ ( 𝐵 ⊆ 𝐴 → ( 𝐴 ⊆ 𝑥 → 𝐵 ⊆ 𝑥 ) )
6 5 anim1d ⊢ ( 𝐵 ⊆ 𝐴 → ( ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ) → ( 𝐵 ⊆ 𝑥 ∧ Tr 𝑥 ) ) )
7 6 ss2abdv ⊢ ( 𝐵 ⊆ 𝐴 → { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ) } ⊆ { 𝑥 ∣ ( 𝐵 ⊆ 𝑥 ∧ Tr 𝑥 ) } )
8 intss ⊢ ( { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ) } ⊆ { 𝑥 ∣ ( 𝐵 ⊆ 𝑥 ∧ Tr 𝑥 ) } → ∩ { 𝑥 ∣ ( 𝐵 ⊆ 𝑥 ∧ Tr 𝑥 ) } ⊆ ∩ { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ) } )
9 7 8 syl ⊢ ( 𝐵 ⊆ 𝐴 → ∩ { 𝑥 ∣ ( 𝐵 ⊆ 𝑥 ∧ Tr 𝑥 ) } ⊆ ∩ { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ) } )
10 tcvalg ⊢ ( 𝐴 ∈ V → ( TC ‘ 𝐴 ) = ∩ { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ) } )
11 1 10 ax-mp ⊢ ( TC ‘ 𝐴 ) = ∩ { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ) }
12 9 11 sseqtrrdi ⊢ ( 𝐵 ⊆ 𝐴 → ∩ { 𝑥 ∣ ( 𝐵 ⊆ 𝑥 ∧ Tr 𝑥 ) } ⊆ ( TC ‘ 𝐴 ) )
13 4 12 eqsstrd ⊢ ( 𝐵 ⊆ 𝐴 → ( TC ‘ 𝐵 ) ⊆ ( TC ‘ 𝐴 ) )