triun

Description: An indexed union of a class of transitive sets is transitive. (Contributed by Mario Carneiro, 16-Nov-2014)

		Ref	Expression
	Assertion	triun	$⊢ \forall x \in A Tr B \to Tr ⋃_{x \in A} B$

Step	Hyp	Ref	Expression
1		eliun	$⊢ y \in ⋃_{x \in A} B \leftrightarrow \exists x \in A y \in B$
2		r19.29	$⊢ (\forall x \in A Tr B \land \exists x \in A y \in B) \to \exists x \in A (Tr B \land y \in B)$
3		nfcv	$⊢ \underline{Ⅎ} x y$
4		nfiu1	$⊢ \underline{Ⅎ} x ⋃_{x \in A} B$
5	3 4	nfss	$⊢ Ⅎ x y \subseteq ⋃_{x \in A} B$
6		trss	$⊢ Tr B \to (y \in B \to y \subseteq B)$
7	6	imp	$⊢ (Tr B \land y \in B) \to y \subseteq B$
8		ssiun2	$⊢ x \in A \to B \subseteq ⋃_{x \in A} B$
9		sstr2	$⊢ y \subseteq B \to (B \subseteq ⋃_{x \in A} B \to y \subseteq ⋃_{x \in A} B)$
10	7 8 9	syl2imc	$⊢ x \in A \to ((Tr B \land y \in B) \to y \subseteq ⋃_{x \in A} B)$
11	5 10	rexlimi	$⊢ \exists x \in A (Tr B \land y \in B) \to y \subseteq ⋃_{x \in A} B$
12	2 11	syl	$⊢ (\forall x \in A Tr B \land \exists x \in A y \in B) \to y \subseteq ⋃_{x \in A} B$
13	1 12	sylan2b	$⊢ (\forall x \in A Tr B \land y \in ⋃_{x \in A} B) \to y \subseteq ⋃_{x \in A} B$
14	13	ralrimiva	$⊢ \forall x \in A Tr B \to \forall y \in ⋃_{x \in A} B y \subseteq ⋃_{x \in A} B$
15		dftr3	$⊢ Tr ⋃_{x \in A} B \leftrightarrow \forall y \in ⋃_{x \in A} B y \subseteq ⋃_{x \in A} B$
16	14 15	sylibr	$⊢ \forall x \in A Tr B \to Tr ⋃_{x \in A} B$

Metamath Proof Explorer