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

Metamath Proof Explorer

Theorem tskint

Description: The intersection of an element of a transitive Tarski class is an element of the class. (Contributed by FL, 17-Apr-2011) (Revised by Mario Carneiro, 20-Sep-2014)

		Ref	Expression
	Assertion	tskint	⊢ ( ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ) ∧ 𝐴 ∈ 𝑇 ∧ 𝐴 ≠ ∅ ) → ∩ 𝐴 ∈ 𝑇 )

Proof

Step	Hyp	Ref	Expression
1		simp1l	⊢ ( ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ) ∧ 𝐴 ∈ 𝑇 ∧ 𝐴 ≠ ∅ ) → 𝑇 ∈ Tarski )
2		tskuni	⊢ ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇 ) → ∪ 𝐴 ∈ 𝑇 )
3	2	3expa	⊢ ( ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ) ∧ 𝐴 ∈ 𝑇 ) → ∪ 𝐴 ∈ 𝑇 )
4	3	3adant3	⊢ ( ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ) ∧ 𝐴 ∈ 𝑇 ∧ 𝐴 ≠ ∅ ) → ∪ 𝐴 ∈ 𝑇 )
5		intssuni	⊢ ( 𝐴 ≠ ∅ → ∩ 𝐴 ⊆ ∪ 𝐴 )
6	5	3ad2ant3	⊢ ( ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ) ∧ 𝐴 ∈ 𝑇 ∧ 𝐴 ≠ ∅ ) → ∩ 𝐴 ⊆ ∪ 𝐴 )
7		tskss	⊢ ( ( 𝑇 ∈ Tarski ∧ ∪ 𝐴 ∈ 𝑇 ∧ ∩ 𝐴 ⊆ ∪ 𝐴 ) → ∩ 𝐴 ∈ 𝑇 )
8	1 4 6 7	syl3anc	⊢ ( ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ) ∧ 𝐴 ∈ 𝑇 ∧ 𝐴 ≠ ∅ ) → ∩ 𝐴 ∈ 𝑇 )