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

Theorem reff 31322
 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 9961. (Contributed by Thierry Arnoux, 12-Jan-2020.)
Assertion
Ref Expression
reff (𝐴𝑉 → (𝐴Ref𝐵 ↔ ( 𝐵 𝐴 ∧ ∃𝑓(𝑓:𝐴𝐵 ∧ ∀𝑣𝐴 𝑣 ⊆ (𝑓𝑣)))))
Distinct variable groups:   𝐴,𝑓,𝑣   𝐵,𝑓,𝑣   𝑓,𝑉,𝑣

Proof of Theorem reff
Dummy variables 𝑥 𝑢 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ssid 3916 . . . 4 𝐵 𝐵
2 eqid 2758 . . . . . 6 𝐴 = 𝐴
3 eqid 2758 . . . . . 6 𝐵 = 𝐵
42, 3isref 22222 . . . . 5 (𝐴𝑉 → (𝐴Ref𝐵 ↔ ( 𝐵 = 𝐴 ∧ ∀𝑣𝐴𝑢𝐵 𝑣𝑢)))
54simprbda 502 . . . 4 ((𝐴𝑉𝐴Ref𝐵) → 𝐵 = 𝐴)
61, 5sseqtrid 3946 . . 3 ((𝐴𝑉𝐴Ref𝐵) → 𝐵 𝐴)
74simplbda 503 . . . 4 ((𝐴𝑉𝐴Ref𝐵) → ∀𝑣𝐴𝑢𝐵 𝑣𝑢)
8 sseq2 3920 . . . . . 6 (𝑢 = (𝑓𝑣) → (𝑣𝑢𝑣 ⊆ (𝑓𝑣)))
98ac6sg 9961 . . . . 5 (𝐴𝑉 → (∀𝑣𝐴𝑢𝐵 𝑣𝑢 → ∃𝑓(𝑓:𝐴𝐵 ∧ ∀𝑣𝐴 𝑣 ⊆ (𝑓𝑣))))
109adantr 484 . . . 4 ((𝐴𝑉𝐴Ref𝐵) → (∀𝑣𝐴𝑢𝐵 𝑣𝑢 → ∃𝑓(𝑓:𝐴𝐵 ∧ ∀𝑣𝐴 𝑣 ⊆ (𝑓𝑣))))
117, 10mpd 15 . . 3 ((𝐴𝑉𝐴Ref𝐵) → ∃𝑓(𝑓:𝐴𝐵 ∧ ∀𝑣𝐴 𝑣 ⊆ (𝑓𝑣)))
126, 11jca 515 . 2 ((𝐴𝑉𝐴Ref𝐵) → ( 𝐵 𝐴 ∧ ∃𝑓(𝑓:𝐴𝐵 ∧ ∀𝑣𝐴 𝑣 ⊆ (𝑓𝑣))))
13 simplr 768 . . . . . . 7 (((𝐴𝑉 𝐵 𝐴) ∧ (𝑓:𝐴𝐵 ∧ ∀𝑣𝐴 𝑣 ⊆ (𝑓𝑣))) → 𝐵 𝐴)
14 nfv 1915 . . . . . . . . . . 11 𝑣(𝐴𝑉 𝐵 𝐴)
15 nfv 1915 . . . . . . . . . . . 12 𝑣 𝑓:𝐴𝐵
16 nfra1 3147 . . . . . . . . . . . 12 𝑣𝑣𝐴 𝑣 ⊆ (𝑓𝑣)
1715, 16nfan 1900 . . . . . . . . . . 11 𝑣(𝑓:𝐴𝐵 ∧ ∀𝑣𝐴 𝑣 ⊆ (𝑓𝑣))
1814, 17nfan 1900 . . . . . . . . . 10 𝑣((𝐴𝑉 𝐵 𝐴) ∧ (𝑓:𝐴𝐵 ∧ ∀𝑣𝐴 𝑣 ⊆ (𝑓𝑣)))
19 nfv 1915 . . . . . . . . . 10 𝑣 𝑥 𝐴
2018, 19nfan 1900 . . . . . . . . 9 𝑣(((𝐴𝑉 𝐵 𝐴) ∧ (𝑓:𝐴𝐵 ∧ ∀𝑣𝐴 𝑣 ⊆ (𝑓𝑣))) ∧ 𝑥 𝐴)
21 simplrl 776 . . . . . . . . . . . . 13 ((((𝐴𝑉 𝐵 𝐴) ∧ (𝑓:𝐴𝐵 ∧ ∀𝑣𝐴 𝑣 ⊆ (𝑓𝑣))) ∧ 𝑣𝐴) → 𝑓:𝐴𝐵)
22 simpr 488 . . . . . . . . . . . . 13 ((((𝐴𝑉 𝐵 𝐴) ∧ (𝑓:𝐴𝐵 ∧ ∀𝑣𝐴 𝑣 ⊆ (𝑓𝑣))) ∧ 𝑣𝐴) → 𝑣𝐴)
2321, 22ffvelrnd 6849 . . . . . . . . . . . 12 ((((𝐴𝑉 𝐵 𝐴) ∧ (𝑓:𝐴𝐵 ∧ ∀𝑣𝐴 𝑣 ⊆ (𝑓𝑣))) ∧ 𝑣𝐴) → (𝑓𝑣) ∈ 𝐵)
2423adantlr 714 . . . . . . . . . . 11 (((((𝐴𝑉 𝐵 𝐴) ∧ (𝑓:𝐴𝐵 ∧ ∀𝑣𝐴 𝑣 ⊆ (𝑓𝑣))) ∧ 𝑥 𝐴) ∧ 𝑣𝐴) → (𝑓𝑣) ∈ 𝐵)
2524adantr 484 . . . . . . . . . 10 ((((((𝐴𝑉 𝐵 𝐴) ∧ (𝑓:𝐴𝐵 ∧ ∀𝑣𝐴 𝑣 ⊆ (𝑓𝑣))) ∧ 𝑥 𝐴) ∧ 𝑣𝐴) ∧ 𝑥𝑣) → (𝑓𝑣) ∈ 𝐵)
26 simplrr 777 . . . . . . . . . . . . 13 ((((𝐴𝑉 𝐵 𝐴) ∧ (𝑓:𝐴𝐵 ∧ ∀𝑣𝐴 𝑣 ⊆ (𝑓𝑣))) ∧ 𝑣𝐴) → ∀𝑣𝐴 𝑣 ⊆ (𝑓𝑣))
2726adantlr 714 . . . . . . . . . . . 12 (((((𝐴𝑉 𝐵 𝐴) ∧ (𝑓:𝐴𝐵 ∧ ∀𝑣𝐴 𝑣 ⊆ (𝑓𝑣))) ∧ 𝑥 𝐴) ∧ 𝑣𝐴) → ∀𝑣𝐴 𝑣 ⊆ (𝑓𝑣))
28 simpr 488 . . . . . . . . . . . 12 (((((𝐴𝑉 𝐵 𝐴) ∧ (𝑓:𝐴𝐵 ∧ ∀𝑣𝐴 𝑣 ⊆ (𝑓𝑣))) ∧ 𝑥 𝐴) ∧ 𝑣𝐴) → 𝑣𝐴)
29 rspa 3135 . . . . . . . . . . . 12 ((∀𝑣𝐴 𝑣 ⊆ (𝑓𝑣) ∧ 𝑣𝐴) → 𝑣 ⊆ (𝑓𝑣))
3027, 28, 29syl2anc 587 . . . . . . . . . . 11 (((((𝐴𝑉 𝐵 𝐴) ∧ (𝑓:𝐴𝐵 ∧ ∀𝑣𝐴 𝑣 ⊆ (𝑓𝑣))) ∧ 𝑥 𝐴) ∧ 𝑣𝐴) → 𝑣 ⊆ (𝑓𝑣))
3130sselda 3894 . . . . . . . . . 10 ((((((𝐴𝑉 𝐵 𝐴) ∧ (𝑓:𝐴𝐵 ∧ ∀𝑣𝐴 𝑣 ⊆ (𝑓𝑣))) ∧ 𝑥 𝐴) ∧ 𝑣𝐴) ∧ 𝑥𝑣) → 𝑥 ∈ (𝑓𝑣))
32 eleq2 2840 . . . . . . . . . . 11 (𝑢 = (𝑓𝑣) → (𝑥𝑢𝑥 ∈ (𝑓𝑣)))
3332rspcev 3543 . . . . . . . . . 10 (((𝑓𝑣) ∈ 𝐵𝑥 ∈ (𝑓𝑣)) → ∃𝑢𝐵 𝑥𝑢)
3425, 31, 33syl2anc 587 . . . . . . . . 9 ((((((𝐴𝑉 𝐵 𝐴) ∧ (𝑓:𝐴𝐵 ∧ ∀𝑣𝐴 𝑣 ⊆ (𝑓𝑣))) ∧ 𝑥 𝐴) ∧ 𝑣𝐴) ∧ 𝑥𝑣) → ∃𝑢𝐵 𝑥𝑢)
35 simpr 488 . . . . . . . . . 10 ((((𝐴𝑉 𝐵 𝐴) ∧ (𝑓:𝐴𝐵 ∧ ∀𝑣𝐴 𝑣 ⊆ (𝑓𝑣))) ∧ 𝑥 𝐴) → 𝑥 𝐴)
36 eluni2 4805 . . . . . . . . . 10 (𝑥 𝐴 ↔ ∃𝑣𝐴 𝑥𝑣)
3735, 36sylib 221 . . . . . . . . 9 ((((𝐴𝑉 𝐵 𝐴) ∧ (𝑓:𝐴𝐵 ∧ ∀𝑣𝐴 𝑣 ⊆ (𝑓𝑣))) ∧ 𝑥 𝐴) → ∃𝑣𝐴 𝑥𝑣)
3820, 34, 37r19.29af 3254 . . . . . . . 8 ((((𝐴𝑉 𝐵 𝐴) ∧ (𝑓:𝐴𝐵 ∧ ∀𝑣𝐴 𝑣 ⊆ (𝑓𝑣))) ∧ 𝑥 𝐴) → ∃𝑢𝐵 𝑥𝑢)
39 eluni2 4805 . . . . . . . 8 (𝑥 𝐵 ↔ ∃𝑢𝐵 𝑥𝑢)
4038, 39sylibr 237 . . . . . . 7 ((((𝐴𝑉 𝐵 𝐴) ∧ (𝑓:𝐴𝐵 ∧ ∀𝑣𝐴 𝑣 ⊆ (𝑓𝑣))) ∧ 𝑥 𝐴) → 𝑥 𝐵)
4113, 40eqelssd 3915 . . . . . 6 (((𝐴𝑉 𝐵 𝐴) ∧ (𝑓:𝐴𝐵 ∧ ∀𝑣𝐴 𝑣 ⊆ (𝑓𝑣))) → 𝐵 = 𝐴)
4226, 22, 29syl2anc 587 . . . . . . . . 9 ((((𝐴𝑉 𝐵 𝐴) ∧ (𝑓:𝐴𝐵 ∧ ∀𝑣𝐴 𝑣 ⊆ (𝑓𝑣))) ∧ 𝑣𝐴) → 𝑣 ⊆ (𝑓𝑣))
438rspcev 3543 . . . . . . . . 9 (((𝑓𝑣) ∈ 𝐵𝑣 ⊆ (𝑓𝑣)) → ∃𝑢𝐵 𝑣𝑢)
4423, 42, 43syl2anc 587 . . . . . . . 8 ((((𝐴𝑉 𝐵 𝐴) ∧ (𝑓:𝐴𝐵 ∧ ∀𝑣𝐴 𝑣 ⊆ (𝑓𝑣))) ∧ 𝑣𝐴) → ∃𝑢𝐵 𝑣𝑢)
4544ex 416 . . . . . . 7 (((𝐴𝑉 𝐵 𝐴) ∧ (𝑓:𝐴𝐵 ∧ ∀𝑣𝐴 𝑣 ⊆ (𝑓𝑣))) → (𝑣𝐴 → ∃𝑢𝐵 𝑣𝑢))
4618, 45ralrimi 3144 . . . . . 6 (((𝐴𝑉 𝐵 𝐴) ∧ (𝑓:𝐴𝐵 ∧ ∀𝑣𝐴 𝑣 ⊆ (𝑓𝑣))) → ∀𝑣𝐴𝑢𝐵 𝑣𝑢)
474ad2antrr 725 . . . . . 6 (((𝐴𝑉 𝐵 𝐴) ∧ (𝑓:𝐴𝐵 ∧ ∀𝑣𝐴 𝑣 ⊆ (𝑓𝑣))) → (𝐴Ref𝐵 ↔ ( 𝐵 = 𝐴 ∧ ∀𝑣𝐴𝑢𝐵 𝑣𝑢)))
4841, 46, 47mpbir2and 712 . . . . 5 (((𝐴𝑉 𝐵 𝐴) ∧ (𝑓:𝐴𝐵 ∧ ∀𝑣𝐴 𝑣 ⊆ (𝑓𝑣))) → 𝐴Ref𝐵)
4948ex 416 . . . 4 ((𝐴𝑉 𝐵 𝐴) → ((𝑓:𝐴𝐵 ∧ ∀𝑣𝐴 𝑣 ⊆ (𝑓𝑣)) → 𝐴Ref𝐵))
5049exlimdv 1934 . . 3 ((𝐴𝑉 𝐵 𝐴) → (∃𝑓(𝑓:𝐴𝐵 ∧ ∀𝑣𝐴 𝑣 ⊆ (𝑓𝑣)) → 𝐴Ref𝐵))
5150impr 458 . 2 ((𝐴𝑉 ∧ ( 𝐵 𝐴 ∧ ∃𝑓(𝑓:𝐴𝐵 ∧ ∀𝑣𝐴 𝑣 ⊆ (𝑓𝑣)))) → 𝐴Ref𝐵)
5212, 51impbida 800 1 (𝐴𝑉 → (𝐴Ref𝐵 ↔ ( 𝐵 𝐴 ∧ ∃𝑓(𝑓:𝐴𝐵 ∧ ∀𝑣𝐴 𝑣 ⊆ (𝑓𝑣)))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538  ∃wex 1781   ∈ wcel 2111  ∀wral 3070  ∃wrex 3071   ⊆ wss 3860  ∪ cuni 4801   class class class wbr 5036  ⟶wf 6336  ‘cfv 6340  Refcref 22215 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-rep 5160  ax-sep 5173  ax-nul 5180  ax-pow 5238  ax-pr 5302  ax-un 7465  ax-reg 9102  ax-inf2 9150  ax-ac2 9936 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-ral 3075  df-rex 3076  df-reu 3077  df-rmo 3078  df-rab 3079  df-v 3411  df-sbc 3699  df-csb 3808  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-pss 3879  df-nul 4228  df-if 4424  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4802  df-int 4842  df-iun 4888  df-iin 4889  df-br 5037  df-opab 5099  df-mpt 5117  df-tr 5143  df-id 5434  df-eprel 5439  df-po 5447  df-so 5448  df-fr 5487  df-se 5488  df-we 5489  df-xp 5534  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-rn 5539  df-res 5540  df-ima 5541  df-pred 6131  df-ord 6177  df-on 6178  df-lim 6179  df-suc 6180  df-iota 6299  df-fun 6342  df-fn 6343  df-f 6344  df-f1 6345  df-fo 6346  df-f1o 6347  df-fv 6348  df-isom 6349  df-riota 7114  df-om 7586  df-wrecs 7963  df-recs 8024  df-rdg 8062  df-en 8541  df-r1 9239  df-rank 9240  df-card 9414  df-ac 9589  df-ref 22218 This theorem is referenced by:  locfinreflem  31323
 Copyright terms: Public domain W3C validator