Theorem isref

Description: The property of being a refinement of a cover. Dr. Nyikos once commented in class that the term "refinement" is actually misleading and that people are inclined to confuse it with the notion defined in isfne . On the other hand, the two concepts do seem to have a dual relationship. (Contributed by Jeff Hankins, 18-Jan-2010) (Revised by Thierry Arnoux, 3-Feb-2020)

	Ref	Expression
Hypotheses	isref.1	|- X = U. A
	isref.2	|- Y = U. B
Assertion	isref	|- ( A e. C -> ( A Ref B <-> ( Y = X /\ A. x e. A E. y e. B x C_ y ) ) )

Proof

Step	Hyp	Ref	Expression
1		isref.1	|- X = U. A
2		isref.2	|- Y = U. B
3		refrel	|- Rel Ref
4	3	brrelex2i	|- ( A Ref B -> B e. _V )
5	4	anim2i	|- ( ( A e. C /\ A Ref B ) -> ( A e. C /\ B e. _V ) )
6		simpl	|- ( ( A e. C /\ ( Y = X /\ A. x e. A E. y e. B x C_ y ) ) -> A e. C )
7		simpr	|- ( ( A e. C /\ Y = X ) -> Y = X )
8	7 2 1	3eqtr3g	|- ( ( A e. C /\ Y = X ) -> U. B = U. A )
9		uniexg	|- ( A e. C -> U. A e. _V )
10	9	adantr	|- ( ( A e. C /\ Y = X ) -> U. A e. _V )
11	8 10	eqeltrd	|- ( ( A e. C /\ Y = X ) -> U. B e. _V )
12		uniexb	|- ( B e. _V <-> U. B e. _V )
13	11 12	sylibr	|- ( ( A e. C /\ Y = X ) -> B e. _V )
14	13	adantrr	|- ( ( A e. C /\ ( Y = X /\ A. x e. A E. y e. B x C_ y ) ) -> B e. _V )
15	6 14	jca	|- ( ( A e. C /\ ( Y = X /\ A. x e. A E. y e. B x C_ y ) ) -> ( A e. C /\ B e. _V ) )
16		unieq	|- ( a = A -> U. a = U. A )
17	16 1	eqtr4di	|- ( a = A -> U. a = X )
18	17	eqeq2d	|- ( a = A -> ( U. b = U. a <-> U. b = X ) )
19		raleq	|- ( a = A -> ( A. x e. a E. y e. b x C_ y <-> A. x e. A E. y e. b x C_ y ) )
20	18 19	anbi12d	|- ( a = A -> ( ( U. b = U. a /\ A. x e. a E. y e. b x C_ y ) <-> ( U. b = X /\ A. x e. A E. y e. b x C_ y ) ) )
21		unieq	|- ( b = B -> U. b = U. B )
22	21 2	eqtr4di	|- ( b = B -> U. b = Y )
23	22	eqeq1d	|- ( b = B -> ( U. b = X <-> Y = X ) )
24		rexeq	|- ( b = B -> ( E. y e. b x C_ y <-> E. y e. B x C_ y ) )
25	24	ralbidv	|- ( b = B -> ( A. x e. A E. y e. b x C_ y <-> A. x e. A E. y e. B x C_ y ) )
26	23 25	anbi12d	|- ( b = B -> ( ( U. b = X /\ A. x e. A E. y e. b x C_ y ) <-> ( Y = X /\ A. x e. A E. y e. B x C_ y ) ) )
27		df-ref	|- Ref = { <. a , b >. | ( U. b = U. a /\ A. x e. a E. y e. b x C_ y ) }
28	20 26 27	brabg	|- ( ( A e. C /\ B e. _V ) -> ( A Ref B <-> ( Y = X /\ A. x e. A E. y e. B x C_ y ) ) )
29	5 15 28	pm5.21nd	|- ( A e. C -> ( A Ref B <-> ( Y = X /\ A. x e. A E. y e. B x C_ y ) ) )