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	$⊢ ((T \in Tarski \land Tr T) \land A \in T \land A \neq \emptyset) \to ⋂ A \in T$

Proof

Step	Hyp	Ref	Expression
1		simp1l	$⊢ ((T \in Tarski \land Tr T) \land A \in T \land A \neq \emptyset) \to T \in Tarski$
2		tskuni	$⊢ (T \in Tarski \land Tr T \land A \in T) \to ⋃ A \in T$
3	2	3expa	$⊢ ((T \in Tarski \land Tr T) \land A \in T) \to ⋃ A \in T$
4	3	3adant3	$⊢ ((T \in Tarski \land Tr T) \land A \in T \land A \neq \emptyset) \to ⋃ A \in T$
5		intssuni	$⊢ A \neq \emptyset \to ⋂ A \subseteq ⋃ A$
6	5	3ad2ant3	$⊢ ((T \in Tarski \land Tr T) \land A \in T \land A \neq \emptyset) \to ⋂ A \subseteq ⋃ A$
7		tskss	$⊢ (T \in Tarski \land ⋃ A \in T \land ⋂ A \subseteq ⋃ A) \to ⋂ A \in T$
8	1 4 6 7	syl3anc	$⊢ ((T \in Tarski \land Tr T) \land A \in T \land A \neq \emptyset) \to ⋂ A \in T$