Metamath Proof Explorer

Theorem reff

Description: For any cover refinement, there exists a function associating with each set in the refinement a set in the original cover containing it. This is sometimes used as a definition of refinement. Note that this definition uses the axiom of choice through ac6sg . (Contributed by Thierry Arnoux, 12-Jan-2020) Remove dependency on ax-reg and ax-inf2 . (Revised by Timothy J. O'Malley, 15-Oct-2026)

Ref Expression
Assertion reff 
|- ( A e. V -> ( A Ref B <-> ( U. B C_ U. A /\ E. f ( f : A --> B /\ A. v e. A v C_ ( f ` v ) ) ) ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  U. A = U. A
2 eqid 
 |-  U. B = U. B
3 1 2 isref 
 |-  ( A e. V -> ( A Ref B <-> ( U. B = U. A /\ A. v e. A E. u e. B v C_ u ) ) )
4 3 simprbda 
 |-  ( ( A e. V /\ A Ref B ) -> U. B = U. A )
5 4 eqimssd 
 |-  ( ( A e. V /\ A Ref B ) -> U. B C_ U. A )
6 simpl 
 |-  ( ( A e. V /\ A Ref B ) -> A e. V )
7 uniexg 
 |-  ( A e. V -> U. A e. _V )
8 pwexg 
 |-  ( U. A e. _V -> ~P U. A e. _V )
9 6 7 8 3syl 
 |-  ( ( A e. V /\ A Ref B ) -> ~P U. A e. _V )
10 sspwuni 
 |-  ( B C_ ~P U. A <-> U. B C_ U. A )
11 5 10 sylibr 
 |-  ( ( A e. V /\ A Ref B ) -> B C_ ~P U. A )
12 9 11 ssexd 
 |-  ( ( A e. V /\ A Ref B ) -> B e. _V )
13 3 simplbda 
 |-  ( ( A e. V /\ A Ref B ) -> A. v e. A E. u e. B v C_ u )
14 sseq2 
 |-  ( u = ( f ` v ) -> ( v C_ u <-> v C_ ( f ` v ) ) )
15 14 ac6 
 |-  ( ( A e. V /\ B e. _V /\ A. v e. A E. u e. B v C_ u ) -> E. f ( f : A --> B /\ A. v e. A v C_ ( f ` v ) ) )
16 6 12 13 15 syl3anc 
 |-  ( ( A e. V /\ A Ref B ) -> E. f ( f : A --> B /\ A. v e. A v C_ ( f ` v ) ) )
17 5 16 jca 
 |-  ( ( A e. V /\ A Ref B ) -> ( U. B C_ U. A /\ E. f ( f : A --> B /\ A. v e. A v C_ ( f ` v ) ) ) )
18 simplr 
 |-  ( ( ( A e. V /\ U. B C_ U. A ) /\ ( f : A --> B /\ A. v e. A v C_ ( f ` v ) ) ) -> U. B C_ U. A )
19 nfv 
 |-  F/ v ( A e. V /\ U. B C_ U. A )
20 nfv 
 |-  F/ v f : A --> B
21 nfra1 
 |-  F/ v A. v e. A v C_ ( f ` v )
22 20 21 nfan 
 |-  F/ v ( f : A --> B /\ A. v e. A v C_ ( f ` v ) )
23 19 22 nfan 
 |-  F/ v ( ( A e. V /\ U. B C_ U. A ) /\ ( f : A --> B /\ A. v e. A v C_ ( f ` v ) ) )
24 nfv 
 |-  F/ v x e. U. A
25 23 24 nfan 
 |-  F/ v ( ( ( A e. V /\ U. B C_ U. A ) /\ ( f : A --> B /\ A. v e. A v C_ ( f ` v ) ) ) /\ x e. U. A )
26 eleq2 
 |-  ( u = ( f ` v ) -> ( x e. u <-> x e. ( f ` v ) ) )
27 simplrl 
 |-  ( ( ( ( A e. V /\ U. B C_ U. A ) /\ ( f : A --> B /\ A. v e. A v C_ ( f ` v ) ) ) /\ v e. A ) -> f : A --> B )
28 simpr 
 |-  ( ( ( ( A e. V /\ U. B C_ U. A ) /\ ( f : A --> B /\ A. v e. A v C_ ( f ` v ) ) ) /\ v e. A ) -> v e. A )
29 27 28 ffvelcdmd 
 |-  ( ( ( ( A e. V /\ U. B C_ U. A ) /\ ( f : A --> B /\ A. v e. A v C_ ( f ` v ) ) ) /\ v e. A ) -> ( f ` v ) e. B )
30 29 ad4ant13 
 |-  ( ( ( ( ( ( A e. V /\ U. B C_ U. A ) /\ ( f : A --> B /\ A. v e. A v C_ ( f ` v ) ) ) /\ x e. U. A ) /\ v e. A ) /\ x e. v ) -> ( f ` v ) e. B )
31 simplrr 
 |-  ( ( ( ( A e. V /\ U. B C_ U. A ) /\ ( f : A --> B /\ A. v e. A v C_ ( f ` v ) ) ) /\ v e. A ) -> A. v e. A v C_ ( f ` v ) )
32 31 adantlr 
 |-  ( ( ( ( ( A e. V /\ U. B C_ U. A ) /\ ( f : A --> B /\ A. v e. A v C_ ( f ` v ) ) ) /\ x e. U. A ) /\ v e. A ) -> A. v e. A v C_ ( f ` v ) )
33 rspa 
 |-  ( ( A. v e. A v C_ ( f ` v ) /\ v e. A ) -> v C_ ( f ` v ) )
34 32 33 sylancom 
 |-  ( ( ( ( ( A e. V /\ U. B C_ U. A ) /\ ( f : A --> B /\ A. v e. A v C_ ( f ` v ) ) ) /\ x e. U. A ) /\ v e. A ) -> v C_ ( f ` v ) )
35 34 sselda 
 |-  ( ( ( ( ( ( A e. V /\ U. B C_ U. A ) /\ ( f : A --> B /\ A. v e. A v C_ ( f ` v ) ) ) /\ x e. U. A ) /\ v e. A ) /\ x e. v ) -> x e. ( f ` v ) )
36 26 30 35 rspcedvdw 
 |-  ( ( ( ( ( ( A e. V /\ U. B C_ U. A ) /\ ( f : A --> B /\ A. v e. A v C_ ( f ` v ) ) ) /\ x e. U. A ) /\ v e. A ) /\ x e. v ) -> E. u e. B x e. u )
37 eluni2 
 |-  ( x e. U. A <-> E. v e. A x e. v )
38 37 bilani 
 |-  ( ( ( ( A e. V /\ U. B C_ U. A ) /\ ( f : A --> B /\ A. v e. A v C_ ( f ` v ) ) ) /\ x e. U. A ) -> E. v e. A x e. v )
39 25 36 38 r19.29af 
 |-  ( ( ( ( A e. V /\ U. B C_ U. A ) /\ ( f : A --> B /\ A. v e. A v C_ ( f ` v ) ) ) /\ x e. U. A ) -> E. u e. B x e. u )
40 eluni2 
 |-  ( x e. U. B <-> E. u e. B x e. u )
41 39 40 sylibr 
 |-  ( ( ( ( A e. V /\ U. B C_ U. A ) /\ ( f : A --> B /\ A. v e. A v C_ ( f ` v ) ) ) /\ x e. U. A ) -> x e. U. B )
42 18 41 eqelssd 
 |-  ( ( ( A e. V /\ U. B C_ U. A ) /\ ( f : A --> B /\ A. v e. A v C_ ( f ` v ) ) ) -> U. B = U. A )
43 31 33 sylancom 
 |-  ( ( ( ( A e. V /\ U. B C_ U. A ) /\ ( f : A --> B /\ A. v e. A v C_ ( f ` v ) ) ) /\ v e. A ) -> v C_ ( f ` v ) )
44 14 29 43 rspcedvdw 
 |-  ( ( ( ( A e. V /\ U. B C_ U. A ) /\ ( f : A --> B /\ A. v e. A v C_ ( f ` v ) ) ) /\ v e. A ) -> E. u e. B v C_ u )
45 23 44 ralrimia 
 |-  ( ( ( A e. V /\ U. B C_ U. A ) /\ ( f : A --> B /\ A. v e. A v C_ ( f ` v ) ) ) -> A. v e. A E. u e. B v C_ u )
46 3 ad2antrr 
 |-  ( ( ( A e. V /\ U. B C_ U. A ) /\ ( f : A --> B /\ A. v e. A v C_ ( f ` v ) ) ) -> ( A Ref B <-> ( U. B = U. A /\ A. v e. A E. u e. B v C_ u ) ) )
47 42 45 46 mpbir2and 
 |-  ( ( ( A e. V /\ U. B C_ U. A ) /\ ( f : A --> B /\ A. v e. A v C_ ( f ` v ) ) ) -> A Ref B )
48 47 ex 
 |-  ( ( A e. V /\ U. B C_ U. A ) -> ( ( f : A --> B /\ A. v e. A v C_ ( f ` v ) ) -> A Ref B ) )
49 48 exlimdv 
 |-  ( ( A e. V /\ U. B C_ U. A ) -> ( E. f ( f : A --> B /\ A. v e. A v C_ ( f ` v ) ) -> A Ref B ) )
50 49 impr 
 |-  ( ( A e. V /\ ( U. B C_ U. A /\ E. f ( f : A --> B /\ A. v e. A v C_ ( f ` v ) ) ) ) -> A Ref B )
51 17 50 impbida 
 |-  ( A e. V -> ( A Ref B <-> ( U. B C_ U. A /\ E. f ( f : A --> B /\ A. v e. A v C_ ( f ` v ) ) ) ) )