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 ‘ 𝐴 ) )