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)

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 ssid 
 |-  U. B C_ U. B
2 eqid 
 |-  U. A = U. A
3 eqid 
 |-  U. B = U. B
4 2 3 isref 
 |-  ( A e. V -> ( A Ref B <-> ( U. B = U. A /\ A. v e. A E. u e. B v C_ u ) ) )
5 4 simprbda 
 |-  ( ( A e. V /\ A Ref B ) -> U. B = U. A )
6 1 5 sseqtrid 
 |-  ( ( A e. V /\ A Ref B ) -> U. B C_ U. A )
7 4 simplbda 
 |-  ( ( A e. V /\ A Ref B ) -> A. v e. A E. u e. B v C_ u )
8 sseq2 
 |-  ( u = ( f ` v ) -> ( v C_ u <-> v C_ ( f ` v ) ) )
9 8 ac6sg 
 |-  ( A 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 ) ) ) )
10 9 adantr 
 |-  ( ( A e. V /\ A Ref B ) -> ( A. v e. A E. u e. B v C_ u -> E. f ( f : A --> B /\ A. v e. A v C_ ( f ` v ) ) ) )
11 7 10 mpd 
 |-  ( ( A e. V /\ A Ref B ) -> E. f ( f : A --> B /\ A. v e. A v C_ ( f ` v ) ) )
12 6 11 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 ) ) ) )
13 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 )
14 nfv 
 |-  F/ v ( A e. V /\ U. B C_ U. A )
15 nfv 
 |-  F/ v f : A --> B
16 nfra1 
 |-  F/ v A. v e. A v C_ ( f ` v )
17 15 16 nfan 
 |-  F/ v ( f : A --> B /\ A. v e. A v C_ ( f ` v ) )
18 14 17 nfan 
 |-  F/ v ( ( A e. V /\ U. B C_ U. A ) /\ ( f : A --> B /\ A. v e. A v C_ ( f ` v ) ) )
19 nfv 
 |-  F/ v x e. U. A
20 18 19 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 )
21 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 )
22 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 )
23 21 22 ffvelrnd 
 |-  ( ( ( ( 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 )
24 23 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 ) -> ( f ` v ) e. B )
25 24 adantr 
 |-  ( ( ( ( ( ( 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 )
26 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 ) )
27 26 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 ) )
28 simpr 
 |-  ( ( ( ( ( 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 e. A )
29 rspa 
 |-  ( ( A. v e. A v C_ ( f ` v ) /\ v e. A ) -> v C_ ( f ` v ) )
30 27 28 29 syl2anc 
 |-  ( ( ( ( ( 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 ) )
31 30 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 ) )
32 eleq2 
 |-  ( u = ( f ` v ) -> ( x e. u <-> x e. ( f ` v ) ) )
33 32 rspcev 
 |-  ( ( ( f ` v ) e. B /\ x e. ( f ` v ) ) -> E. u e. B x e. u )
34 25 31 33 syl2anc 
 |-  ( ( ( ( ( ( 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 )
35 simpr 
 |-  ( ( ( ( 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. A )
36 eluni2 
 |-  ( x e. U. A <-> E. v e. A x e. v )
37 35 36 sylib 
 |-  ( ( ( ( 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 )
38 20 34 37 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 )
39 eluni2 
 |-  ( x e. U. B <-> E. u e. B x e. u )
40 38 39 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 )
41 13 40 eqelssd 
 |-  ( ( ( A e. V /\ U. B C_ U. A ) /\ ( f : A --> B /\ A. v e. A v C_ ( f ` v ) ) ) -> U. B = U. A )
42 26 22 29 syl2anc 
 |-  ( ( ( ( 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 ) )
43 8 rspcev 
 |-  ( ( ( f ` v ) e. B /\ v C_ ( f ` v ) ) -> E. u e. B v C_ u )
44 23 42 43 syl2anc 
 |-  ( ( ( ( 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 44 ex 
 |-  ( ( ( 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 ) )
46 18 45 ralrimi 
 |-  ( ( ( 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 )
47 4 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 ) ) )
48 41 46 47 mpbir2and 
 |-  ( ( ( A e. V /\ U. B C_ U. A ) /\ ( f : A --> B /\ A. v e. A v C_ ( f ` v ) ) ) -> A Ref B )
49 48 ex 
 |-  ( ( A e. V /\ U. B C_ U. A ) -> ( ( f : A --> B /\ A. v e. A v C_ ( f ` v ) ) -> A Ref B ) )
50 49 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 ) )
51 50 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 )
52 12 51 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 ) ) ) ) )