Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  reff Structured version   Unicode version

Theorem reff 27820
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 defintion of refinement. Note that this definition uses the axiom of choice through ac6sg 8871. (Contributed by Thierry Arnoux, 12-Jan-2020.)
Assertion
Ref Expression
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
) ) ) ) )
Distinct variable groups:    A, f,
v    B, f, v    f, V, v

Proof of Theorem reff
Dummy variables  x  u are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ssid 3508 . . . 4  |-  U. B  C_ 
U. B
2 eqid 2443 . . . . . 6  |-  U. A  =  U. A
3 eqid 2443 . . . . . 6  |-  U. B  =  U. B
42, 3isref 19988 . . . . 5  |-  ( A  e.  V  ->  ( A Ref B  <->  ( U. B  =  U. A  /\  A. v  e.  A  E. u  e.  B  v  C_  u ) ) )
54simprbda 623 . . . 4  |-  ( ( A  e.  V  /\  A Ref B )  ->  U. B  =  U. A )
61, 5syl5sseq 3537 . . 3  |-  ( ( A  e.  V  /\  A Ref B )  ->  U. B  C_  U. A
)
74simplbda 624 . . . 4  |-  ( ( A  e.  V  /\  A Ref B )  ->  A. v  e.  A  E. u  e.  B  v  C_  u )
8 sseq2 3511 . . . . . 6  |-  ( u  =  ( f `  v )  ->  (
v  C_  u  <->  v  C_  ( f `  v
) ) )
98ac6sg 8871 . . . . 5  |-  ( 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 )
) ) )
109adantr 465 . . . 4  |-  ( ( 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 ) ) ) )
117, 10mpd 15 . . 3  |-  ( ( A  e.  V  /\  A Ref B )  ->  E. f ( f : A --> B  /\  A. v  e.  A  v  C_  ( f `  v
) ) )
126, 11jca 532 . 2  |-  ( ( 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 755 . . . . . . 7  |-  ( ( ( 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 1694 . . . . . . . . . . . . 13  |-  F/ v ( A  e.  V  /\  U. B  C_  U. A
)
15 nfv 1694 . . . . . . . . . . . . . 14  |-  F/ v  f : A --> B
16 nfra1 2824 . . . . . . . . . . . . . 14  |-  F/ v A. v  e.  A  v  C_  ( f `  v )
1715, 16nfan 1914 . . . . . . . . . . . . 13  |-  F/ v ( f : A --> B  /\  A. v  e.  A  v  C_  (
f `  v )
)
1814, 17nfan 1914 . . . . . . . . . . . 12  |-  F/ v ( ( A  e.  V  /\  U. B  C_ 
U. A )  /\  ( f : A --> B  /\  A. v  e.  A  v  C_  (
f `  v )
) )
19 nfv 1694 . . . . . . . . . . . 12  |-  F/ v  x  e.  U. A
2018, 19nfan 1914 . . . . . . . . . . 11  |-  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 761 . . . . . . . . . . . . . . 15  |-  ( ( ( ( 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 461 . . . . . . . . . . . . . . 15  |-  ( ( ( ( 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 )
2321, 22ffvelrnd 6017 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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 )
2423adantlr 714 . . . . . . . . . . . . 13  |-  ( ( ( ( ( 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
)
2524adantr 465 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( 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 762 . . . . . . . . . . . . . . 15  |-  ( ( ( ( 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
) )
2726adantlr 714 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( 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 461 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( 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 2810 . . . . . . . . . . . . . 14  |-  ( ( A. v  e.  A  v  C_  ( f `  v )  /\  v  e.  A )  ->  v  C_  ( f `  v
) )
3027, 28, 29syl2anc 661 . . . . . . . . . . . . 13  |-  ( ( ( ( ( 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
) )
3130sselda 3489 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( 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 2516 . . . . . . . . . . . . 13  |-  ( u  =  ( f `  v )  ->  (
x  e.  u  <->  x  e.  ( f `  v
) ) )
3332rspcev 3196 . . . . . . . . . . . 12  |-  ( ( ( f `  v
)  e.  B  /\  x  e.  ( f `  v ) )  ->  E. u  e.  B  x  e.  u )
3425, 31, 33syl2anc 661 . . . . . . . . . . 11  |-  ( ( ( ( ( ( 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 461 . . . . . . . . . . . 12  |-  ( ( ( ( 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 4238 . . . . . . . . . . . 12  |-  ( x  e.  U. A  <->  E. v  e.  A  x  e.  v )
3735, 36sylib 196 . . . . . . . . . . 11  |-  ( ( ( ( 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 )
3820, 34, 37r19.29af 2983 . . . . . . . . . 10  |-  ( ( ( ( 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 4238 . . . . . . . . . 10  |-  ( x  e.  U. B  <->  E. u  e.  B  x  e.  u )
4038, 39sylibr 212 . . . . . . . . 9  |-  ( ( ( ( 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 )
4140ex 434 . . . . . . . 8  |-  ( ( ( 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 ) )
4241ssrdv 3495 . . . . . . 7  |-  ( ( ( A  e.  V  /\  U. B  C_  U. A
)  /\  ( f : A --> B  /\  A. v  e.  A  v  C_  ( f `  v
) ) )  ->  U. A  C_  U. B
)
4313, 42eqssd 3506 . . . . . 6  |-  ( ( ( A  e.  V  /\  U. B  C_  U. A
)  /\  ( f : A --> B  /\  A. v  e.  A  v  C_  ( f `  v
) ) )  ->  U. B  =  U. A )
4426, 22, 29syl2anc 661 . . . . . . . . 9  |-  ( ( ( ( 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
) )
458rspcev 3196 . . . . . . . . 9  |-  ( ( ( f `  v
)  e.  B  /\  v  C_  ( f `  v ) )  ->  E. u  e.  B  v  C_  u )
4623, 44, 45syl2anc 661 . . . . . . . 8  |-  ( ( ( ( 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 )
4746ex 434 . . . . . . 7  |-  ( ( ( 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 ) )
4818, 47ralrimi 2843 . . . . . 6  |-  ( ( ( 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 )
494ad2antrr 725 . . . . . 6  |-  ( ( ( 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
) ) )
5043, 48, 49mpbir2and 922 . . . . 5  |-  ( ( ( A  e.  V  /\  U. B  C_  U. A
)  /\  ( f : A --> B  /\  A. v  e.  A  v  C_  ( f `  v
) ) )  ->  A Ref B )
5150ex 434 . . . 4  |-  ( ( A  e.  V  /\  U. B  C_  U. A )  ->  ( ( f : A --> B  /\  A. v  e.  A  v 
C_  ( f `  v ) )  ->  A Ref B ) )
5251exlimdv 1711 . . 3  |-  ( ( A  e.  V  /\  U. B  C_  U. A )  ->  ( E. f
( f : A --> B  /\  A. v  e.  A  v  C_  (
f `  v )
)  ->  A Ref B ) )
5352impr 619 . 2  |-  ( ( A  e.  V  /\  ( U. B  C_  U. A  /\  E. f ( f : A --> B  /\  A. v  e.  A  v 
C_  ( f `  v ) ) ) )  ->  A Ref B )
5412, 53impbida 832 1  |-  ( A  e.  V  ->  ( A Ref B  <->  ( U. B  C_  U. A  /\  E. f ( f : A --> B  /\  A. v  e.  A  v  C_  ( f `  v
) ) ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1383   E.wex 1599    e. wcel 1804   A.wral 2793   E.wrex 2794    C_ wss 3461   U.cuni 4234   class class class wbr 4437   -->wf 5574   ` cfv 5578   Refcref 19981
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-rep 4548  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-un 6577  ax-reg 8021  ax-inf2 8061  ax-ac2 8846
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 975  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rex 2799  df-reu 2800  df-rmo 2801  df-rab 2802  df-v 3097  df-sbc 3314  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-tp 4019  df-op 4021  df-uni 4235  df-int 4272  df-iun 4317  df-iin 4318  df-br 4438  df-opab 4496  df-mpt 4497  df-tr 4531  df-eprel 4781  df-id 4785  df-po 4790  df-so 4791  df-fr 4828  df-se 4829  df-we 4830  df-ord 4871  df-on 4872  df-lim 4873  df-suc 4874  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-res 5001  df-ima 5002  df-iota 5541  df-fun 5580  df-fn 5581  df-f 5582  df-f1 5583  df-fo 5584  df-f1o 5585  df-fv 5586  df-isom 5587  df-riota 6242  df-om 6686  df-recs 7044  df-rdg 7078  df-en 7519  df-r1 8185  df-rank 8186  df-card 8323  df-ac 8500  df-ref 19984
This theorem is referenced by:  locfinreflem  27821
  Copyright terms: Public domain W3C validator