Metamath Proof Explorer


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 = A
isref.2 Y = B
Assertion isref A C A Ref B Y = X x A y B x y

Proof

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