Theorem 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\mathrm{Tr}B\to \mathrm{Tr}\bigcup _{x\in A}B$$

Proof

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