This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = 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 ) ) )