Theorem dfon2lem1

Description: Lemma for dfon2 . (Contributed by Scott Fenton, 28-Feb-2011)

	Ref	Expression
Assertion	dfon2lem1	$$⊢\mathrm{Tr}\bigcup \left\{x|\left(\phi \wedge \mathrm{Tr}x\wedge \psi \right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		truni	$$⊢\forall y\in \left\{x|\left(\phi \wedge \mathrm{Tr}x\wedge \psi \right)\right\}\mathrm{Tr}y\to \mathrm{Tr}\bigcup \left\{x|\left(\phi \wedge \mathrm{Tr}x\wedge \psi \right)\right\}$$
2		nfsbc1v	$$⊢Ⅎx\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi$$
3		nfv	$$⊢Ⅎx\mathrm{Tr}y$$
4		nfsbc1v	$$⊢Ⅎx\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\psi$$
5	2 3 4	nf3an	$$⊢Ⅎx\left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \wedge \mathrm{Tr}y\wedge \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\psi \right)$$
6		vex	$$⊢y\in \mathrm{V}$$
7		sbceq1a	$$⊢x=y\to \left(\phi \leftrightarrow \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)$$
8		treq	$$⊢x=y\to \left(\mathrm{Tr}x\leftrightarrow \mathrm{Tr}y\right)$$
9		sbceq1a	$$⊢x=y\to \left(\psi \leftrightarrow \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\psi \right)$$
10	7 8 9	3anbi123d	$$⊢x=y\to \left(\left(\phi \wedge \mathrm{Tr}x\wedge \psi \right)\leftrightarrow \left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \wedge \mathrm{Tr}y\wedge \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\psi \right)\right)$$
11	5 6 10	elabf	$$⊢y\in \left\{x|\left(\phi \wedge \mathrm{Tr}x\wedge \psi \right)\right\}\leftrightarrow \left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \wedge \mathrm{Tr}y\wedge \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\psi \right)$$
12	11	simp2bi	$$⊢y\in \left\{x|\left(\phi \wedge \mathrm{Tr}x\wedge \psi \right)\right\}\to \mathrm{Tr}y$$
13	1 12	mprg	$$⊢\mathrm{Tr}\bigcup \left\{x|\left(\phi \wedge \mathrm{Tr}x\wedge \psi \right)\right\}$$