MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  isref Structured version   Visualization version   GIF version

Theorem isref 21821
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 33205. 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.)
Hypotheses
Ref Expression
isref.1 𝑋 = 𝐴
isref.2 𝑌 = 𝐵
Assertion
Ref Expression
isref (𝐴𝐶 → (𝐴Ref𝐵 ↔ (𝑌 = 𝑋 ∧ ∀𝑥𝐴𝑦𝐵 𝑥𝑦)))
Distinct variable groups:   𝑥,𝐴   𝑥,𝑦,𝐵
Allowed substitution hints:   𝐴(𝑦)   𝐶(𝑥,𝑦)   𝑋(𝑥,𝑦)   𝑌(𝑥,𝑦)

Proof of Theorem isref
Dummy variables 𝑎 𝑏 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 refrel 21820 . . . 4 Rel Ref
21brrelex2i 5459 . . 3 (𝐴Ref𝐵𝐵 ∈ V)
32anim2i 607 . 2 ((𝐴𝐶𝐴Ref𝐵) → (𝐴𝐶𝐵 ∈ V))
4 simpl 475 . . 3 ((𝐴𝐶 ∧ (𝑌 = 𝑋 ∧ ∀𝑥𝐴𝑦𝐵 𝑥𝑦)) → 𝐴𝐶)
5 simpr 477 . . . . . . 7 ((𝐴𝐶𝑌 = 𝑋) → 𝑌 = 𝑋)
6 isref.2 . . . . . . 7 𝑌 = 𝐵
7 isref.1 . . . . . . 7 𝑋 = 𝐴
85, 6, 73eqtr3g 2838 . . . . . 6 ((𝐴𝐶𝑌 = 𝑋) → 𝐵 = 𝐴)
9 uniexg 7285 . . . . . . 7 (𝐴𝐶 𝐴 ∈ V)
109adantr 473 . . . . . 6 ((𝐴𝐶𝑌 = 𝑋) → 𝐴 ∈ V)
118, 10eqeltrd 2867 . . . . 5 ((𝐴𝐶𝑌 = 𝑋) → 𝐵 ∈ V)
12 uniexb 7303 . . . . 5 (𝐵 ∈ V ↔ 𝐵 ∈ V)
1311, 12sylibr 226 . . . 4 ((𝐴𝐶𝑌 = 𝑋) → 𝐵 ∈ V)
1413adantrr 704 . . 3 ((𝐴𝐶 ∧ (𝑌 = 𝑋 ∧ ∀𝑥𝐴𝑦𝐵 𝑥𝑦)) → 𝐵 ∈ V)
154, 14jca 504 . 2 ((𝐴𝐶 ∧ (𝑌 = 𝑋 ∧ ∀𝑥𝐴𝑦𝐵 𝑥𝑦)) → (𝐴𝐶𝐵 ∈ V))
16 unieq 4720 . . . . . 6 (𝑎 = 𝐴 𝑎 = 𝐴)
1716, 7syl6eqr 2833 . . . . 5 (𝑎 = 𝐴 𝑎 = 𝑋)
1817eqeq2d 2789 . . . 4 (𝑎 = 𝐴 → ( 𝑏 = 𝑎 𝑏 = 𝑋))
19 raleq 3346 . . . 4 (𝑎 = 𝐴 → (∀𝑥𝑎𝑦𝑏 𝑥𝑦 ↔ ∀𝑥𝐴𝑦𝑏 𝑥𝑦))
2018, 19anbi12d 621 . . 3 (𝑎 = 𝐴 → (( 𝑏 = 𝑎 ∧ ∀𝑥𝑎𝑦𝑏 𝑥𝑦) ↔ ( 𝑏 = 𝑋 ∧ ∀𝑥𝐴𝑦𝑏 𝑥𝑦)))
21 unieq 4720 . . . . . 6 (𝑏 = 𝐵 𝑏 = 𝐵)
2221, 6syl6eqr 2833 . . . . 5 (𝑏 = 𝐵 𝑏 = 𝑌)
2322eqeq1d 2781 . . . 4 (𝑏 = 𝐵 → ( 𝑏 = 𝑋𝑌 = 𝑋))
24 rexeq 3347 . . . . 5 (𝑏 = 𝐵 → (∃𝑦𝑏 𝑥𝑦 ↔ ∃𝑦𝐵 𝑥𝑦))
2524ralbidv 3148 . . . 4 (𝑏 = 𝐵 → (∀𝑥𝐴𝑦𝑏 𝑥𝑦 ↔ ∀𝑥𝐴𝑦𝐵 𝑥𝑦))
2623, 25anbi12d 621 . . 3 (𝑏 = 𝐵 → (( 𝑏 = 𝑋 ∧ ∀𝑥𝐴𝑦𝑏 𝑥𝑦) ↔ (𝑌 = 𝑋 ∧ ∀𝑥𝐴𝑦𝐵 𝑥𝑦)))
27 df-ref 21817 . . 3 Ref = {⟨𝑎, 𝑏⟩ ∣ ( 𝑏 = 𝑎 ∧ ∀𝑥𝑎𝑦𝑏 𝑥𝑦)}
2820, 26, 27brabg 5280 . 2 ((𝐴𝐶𝐵 ∈ V) → (𝐴Ref𝐵 ↔ (𝑌 = 𝑋 ∧ ∀𝑥𝐴𝑦𝐵 𝑥𝑦)))
293, 15, 28pm5.21nd 789 1 (𝐴𝐶 → (𝐴Ref𝐵 ↔ (𝑌 = 𝑋 ∧ ∀𝑥𝐴𝑦𝐵 𝑥𝑦)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 387   = wceq 1507  wcel 2050  wral 3089  wrex 3090  Vcvv 3416  wss 3830   cuni 4712   class class class wbr 4929  Refcref 21814
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2751  ax-sep 5060  ax-nul 5067  ax-pow 5119  ax-pr 5186  ax-un 7279
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2760  df-cleq 2772  df-clel 2847  df-nfc 2919  df-ral 3094  df-rex 3095  df-rab 3098  df-v 3418  df-dif 3833  df-un 3835  df-in 3837  df-ss 3844  df-nul 4180  df-if 4351  df-pw 4424  df-sn 4442  df-pr 4444  df-op 4448  df-uni 4713  df-br 4930  df-opab 4992  df-xp 5413  df-rel 5414  df-ref 21817
This theorem is referenced by:  refbas  21822  refssex  21823  ssref  21824  refref  21825  reftr  21826  refun0  21827  dissnref  21840  reff  30744  locfinreflem  30745  cmpcref  30755  fnessref  33223  refssfne  33224
  Copyright terms: Public domain W3C validator