Theorem isfne

Description: The predicate " B is finer than A ". This property is, in a sense, the opposite of refinement, as refinement requires every element to be a subset of an element of the original and fineness requires that every element of the original have a subset in the finer cover containing every point. I do not know of a literature reference for this. (Contributed by Jeff Hankins, 28-Sep-2009)

	Ref	Expression
Hypotheses	isfne.1	$$⊢X=\bigcup A$$
	isfne.2	$$⊢Y=\bigcup B$$
Assertion	isfne	$$⊢B\in C\to \left(A\mathrm{Fne}B\leftrightarrow \left(X=Y\wedge \forall x\in Ax\subseteq \bigcup \left(B\cap 𝒫x\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		isfne.1	$$⊢X=\bigcup A$$
2		isfne.2	$$⊢Y=\bigcup B$$
3		fnerel	$$⊢\mathrm{Rel}\mathrm{Fne}$$
4	3	brrelex1i	$$⊢A\mathrm{Fne}B\to A\in \mathrm{V}$$
5	4	anim1i	$$⊢\left(A\mathrm{Fne}B\wedge B\in C\right)\to \left(A\in \mathrm{V}\wedge B\in C\right)$$
6	5	ancoms	$$⊢\left(B\in C\wedge A\mathrm{Fne}B\right)\to \left(A\in \mathrm{V}\wedge B\in C\right)$$
7		simpr	$$⊢\left(B\in C\wedge X=Y\right)\to X=Y$$
8	7 1 2	3eqtr3g	$$⊢\left(B\in C\wedge X=Y\right)\to \bigcup A=\bigcup B$$
9		simpr	$$⊢\left(B\in C\wedge \bigcup A=\bigcup B\right)\to \bigcup A=\bigcup B$$
10		uniexg	$$⊢B\in C\to \bigcup B\in \mathrm{V}$$
11	10	adantr	$$⊢\left(B\in C\wedge \bigcup A=\bigcup B\right)\to \bigcup B\in \mathrm{V}$$
12	9 11	eqeltrd	$$⊢\left(B\in C\wedge \bigcup A=\bigcup B\right)\to \bigcup A\in \mathrm{V}$$
13		uniexb	$$⊢A\in \mathrm{V}\leftrightarrow \bigcup A\in \mathrm{V}$$
14	12 13	sylibr	$$⊢\left(B\in C\wedge \bigcup A=\bigcup B\right)\to A\in \mathrm{V}$$
15		simpl	$$⊢\left(B\in C\wedge \bigcup A=\bigcup B\right)\to B\in C$$
16	14 15	jca	$$⊢\left(B\in C\wedge \bigcup A=\bigcup B\right)\to \left(A\in \mathrm{V}\wedge B\in C\right)$$
17	8 16	syldan	$$⊢\left(B\in C\wedge X=Y\right)\to \left(A\in \mathrm{V}\wedge B\in C\right)$$
18	17	adantrr	$$⊢\left(B\in C\wedge \left(X=Y\wedge \forall x\in Ax\subseteq \bigcup \left(B\cap 𝒫x\right)\right)\right)\to \left(A\in \mathrm{V}\wedge B\in C\right)$$
19		unieq	$$⊢r=A\to \bigcup r=\bigcup A$$
20	19 1	eqtr4di	$$⊢r=A\to \bigcup r=X$$
21	20	eqeq1d	$$⊢r=A\to \left(\bigcup r=\bigcup s\leftrightarrow X=\bigcup s\right)$$
22		raleq	$$⊢r=A\to \left(\forall x\in rx\subseteq \bigcup \left(s\cap 𝒫x\right)\leftrightarrow \forall x\in Ax\subseteq \bigcup \left(s\cap 𝒫x\right)\right)$$
23	21 22	anbi12d	$$⊢r=A\to \left(\left(\bigcup r=\bigcup s\wedge \forall x\in rx\subseteq \bigcup \left(s\cap 𝒫x\right)\right)\leftrightarrow \left(X=\bigcup s\wedge \forall x\in Ax\subseteq \bigcup \left(s\cap 𝒫x\right)\right)\right)$$
24		unieq	$$⊢s=B\to \bigcup s=\bigcup B$$
25	24 2	eqtr4di	$$⊢s=B\to \bigcup s=Y$$
26	25	eqeq2d	$$⊢s=B\to \left(X=\bigcup s\leftrightarrow X=Y\right)$$
27		ineq1	$$⊢s=B\to s\cap 𝒫x=B\cap 𝒫x$$
28	27	unieqd	$$⊢s=B\to \bigcup \left(s\cap 𝒫x\right)=\bigcup \left(B\cap 𝒫x\right)$$
29	28	sseq2d	$$⊢s=B\to \left(x\subseteq \bigcup \left(s\cap 𝒫x\right)\leftrightarrow x\subseteq \bigcup \left(B\cap 𝒫x\right)\right)$$
30	29	ralbidv	$$⊢s=B\to \left(\forall x\in Ax\subseteq \bigcup \left(s\cap 𝒫x\right)\leftrightarrow \forall x\in Ax\subseteq \bigcup \left(B\cap 𝒫x\right)\right)$$
31	26 30	anbi12d	$$⊢s=B\to \left(\left(X=\bigcup s\wedge \forall x\in Ax\subseteq \bigcup \left(s\cap 𝒫x\right)\right)\leftrightarrow \left(X=Y\wedge \forall x\in Ax\subseteq \bigcup \left(B\cap 𝒫x\right)\right)\right)$$
32		df-fne	$$⊢\mathrm{Fne}=\left\{⟨r,s⟩|\left(\bigcup r=\bigcup s\wedge \forall x\in rx\subseteq \bigcup \left(s\cap 𝒫x\right)\right)\right\}$$
33	23 31 32	brabg	$$⊢\left(A\in \mathrm{V}\wedge B\in C\right)\to \left(A\mathrm{Fne}B\leftrightarrow \left(X=Y\wedge \forall x\in Ax\subseteq \bigcup \left(B\cap 𝒫x\right)\right)\right)$$
34	6 18 33	pm5.21nd	$$⊢B\in C\to \left(A\mathrm{Fne}B\leftrightarrow \left(X=Y\wedge \forall x\in Ax\subseteq \bigcup \left(B\cap 𝒫x\right)\right)\right)$$