Theorem fneref

Description: Reflexivity of the fineness relation. (Contributed by Jeff Hankins, 12-Oct-2009)

	Ref	Expression
Assertion	fneref	$$⊢A\in V\to A\mathrm{Fne}A$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\bigcup A=\bigcup A$$
2		ssid	$$⊢x\subseteq x$$
3		elequ2	$$⊢z=x\to \left(y\in z\leftrightarrow y\in x\right)$$
4		sseq1	$$⊢z=x\to \left(z\subseteq x\leftrightarrow x\subseteq x\right)$$
5	3 4	anbi12d	$$⊢z=x\to \left(\left(y\in z\wedge z\subseteq x\right)\leftrightarrow \left(y\in x\wedge x\subseteq x\right)\right)$$
6	5	rspcev	$$⊢\left(x\in A\wedge \left(y\in x\wedge x\subseteq x\right)\right)\to \exists z\in A\left(y\in z\wedge z\subseteq x\right)$$
7	2 6	mpanr2	$$⊢\left(x\in A\wedge y\in x\right)\to \exists z\in A\left(y\in z\wedge z\subseteq x\right)$$
8	7	rgen2	$$⊢\forall x\in A\forall y\in x\exists z\in A\left(y\in z\wedge z\subseteq x\right)$$
9	1 8	pm3.2i	$$⊢\left(\bigcup A=\bigcup A\wedge \forall x\in A\forall y\in x\exists z\in A\left(y\in z\wedge z\subseteq x\right)\right)$$
10	1 1	isfne2	$$⊢A\in V\to \left(A\mathrm{Fne}A\leftrightarrow \left(\bigcup A=\bigcup A\wedge \forall x\in A\forall y\in x\exists z\in A\left(y\in z\wedge z\subseteq x\right)\right)\right)$$
11	9 10	mpbiri	$$⊢A\in V\to A\mathrm{Fne}A$$