trintss

Description: Any nonempty transitive class includes its intersection. Exercise 3 in TakeutiZaring p. 44 (which mistakenly does not include the nonemptiness hypothesis). (Contributed by Scott Fenton, 3-Mar-2011) (Proof shortened by Andrew Salmon, 14-Nov-2011)

		Ref	Expression
	Assertion	trintss	$⊢ (Tr A \land A \neq \emptyset) \to ⋂ A \subseteq A$

Proof

Step	Hyp	Ref	Expression
1		n0	$⊢ A \neq \emptyset \leftrightarrow \exists x x \in A$
2		intss1	$⊢ x \in A \to ⋂ A \subseteq x$
3		trss	$⊢ Tr A \to (x \in A \to x \subseteq A)$
4	3	com12	$⊢ x \in A \to (Tr A \to x \subseteq A)$
5		sstr2	$⊢ ⋂ A \subseteq x \to (x \subseteq A \to ⋂ A \subseteq A)$
6	2 4 5	sylsyld	$⊢ x \in A \to (Tr A \to ⋂ A \subseteq A)$
7	6	exlimiv	$⊢ \exists x x \in A \to (Tr A \to ⋂ A \subseteq A)$
8	1 7	sylbi	$⊢ A \neq \emptyset \to (Tr A \to ⋂ A \subseteq A)$
9	8	impcom	$⊢ (Tr A \land A \neq \emptyset) \to ⋂ A \subseteq A$

Metamath Proof Explorer

Theorem trintss

Proof