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