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 = U. A
	isfne.2	|- Y = U. B
Assertion	isfne	|- ( B e. C -> ( A Fne B <-> ( X = Y /\ A. x e. A x C_ U. ( B i^i ~P x ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		isfne.1	|- X = U. A
2		isfne.2	|- Y = U. B
3		fnerel	|- Rel Fne
4	3	brrelex1i	|- ( A Fne B -> A e. _V )
5	4	anim1i	|- ( ( A Fne B /\ B e. C ) -> ( A e. _V /\ B e. C ) )
6	5	ancoms	|- ( ( B e. C /\ A Fne B ) -> ( A e. _V /\ B e. C ) )
7		simpr	|- ( ( B e. C /\ X = Y ) -> X = Y )
8	7 1 2	3eqtr3g	|- ( ( B e. C /\ X = Y ) -> U. A = U. B )
9		simpr	|- ( ( B e. C /\ U. A = U. B ) -> U. A = U. B )
10		uniexg	|- ( B e. C -> U. B e. _V )
11	10	adantr	|- ( ( B e. C /\ U. A = U. B ) -> U. B e. _V )
12	9 11	eqeltrd	|- ( ( B e. C /\ U. A = U. B ) -> U. A e. _V )
13		uniexb	|- ( A e. _V <-> U. A e. _V )
14	12 13	sylibr	|- ( ( B e. C /\ U. A = U. B ) -> A e. _V )
15		simpl	|- ( ( B e. C /\ U. A = U. B ) -> B e. C )
16	14 15	jca	|- ( ( B e. C /\ U. A = U. B ) -> ( A e. _V /\ B e. C ) )
17	8 16	syldan	|- ( ( B e. C /\ X = Y ) -> ( A e. _V /\ B e. C ) )
18	17	adantrr	|- ( ( B e. C /\ ( X = Y /\ A. x e. A x C_ U. ( B i^i ~P x ) ) ) -> ( A e. _V /\ B e. C ) )
19		unieq	|- ( r = A -> U. r = U. A )
20	19 1	eqtr4di	|- ( r = A -> U. r = X )
21	20	eqeq1d	|- ( r = A -> ( U. r = U. s <-> X = U. s ) )
22		raleq	|- ( r = A -> ( A. x e. r x C_ U. ( s i^i ~P x ) <-> A. x e. A x C_ U. ( s i^i ~P x ) ) )
23	21 22	anbi12d	|- ( r = A -> ( ( U. r = U. s /\ A. x e. r x C_ U. ( s i^i ~P x ) ) <-> ( X = U. s /\ A. x e. A x C_ U. ( s i^i ~P x ) ) ) )
24		unieq	|- ( s = B -> U. s = U. B )
25	24 2	eqtr4di	|- ( s = B -> U. s = Y )
26	25	eqeq2d	|- ( s = B -> ( X = U. s <-> X = Y ) )
27		ineq1	|- ( s = B -> ( s i^i ~P x ) = ( B i^i ~P x ) )
28	27	unieqd	|- ( s = B -> U. ( s i^i ~P x ) = U. ( B i^i ~P x ) )
29	28	sseq2d	|- ( s = B -> ( x C_ U. ( s i^i ~P x ) <-> x C_ U. ( B i^i ~P x ) ) )
30	29	ralbidv	|- ( s = B -> ( A. x e. A x C_ U. ( s i^i ~P x ) <-> A. x e. A x C_ U. ( B i^i ~P x ) ) )
31	26 30	anbi12d	|- ( s = B -> ( ( X = U. s /\ A. x e. A x C_ U. ( s i^i ~P x ) ) <-> ( X = Y /\ A. x e. A x C_ U. ( B i^i ~P x ) ) ) )
32		df-fne	|- Fne = { <. r , s >. | ( U. r = U. s /\ A. x e. r x C_ U. ( s i^i ~P x ) ) }
33	23 31 32	brabg	|- ( ( A e. _V /\ B e. C ) -> ( A Fne B <-> ( X = Y /\ A. x e. A x C_ U. ( B i^i ~P x ) ) ) )
34	6 18 33	pm5.21nd	|- ( B e. C -> ( A Fne B <-> ( X = Y /\ A. x e. A x C_ U. ( B i^i ~P x ) ) ) )