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

Theorem isref 22883
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 34864. 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 22882 . . . 4 Rel Ref
21brrelex2i 5693 . . 3 (𝐴Ref𝐵𝐵 ∈ V)
32anim2i 618 . 2 ((𝐴𝐶𝐴Ref𝐵) → (𝐴𝐶𝐵 ∈ V))
4 simpl 484 . . 3 ((𝐴𝐶 ∧ (𝑌 = 𝑋 ∧ ∀𝑥𝐴𝑦𝐵 𝑥𝑦)) → 𝐴𝐶)
5 simpr 486 . . . . . . 7 ((𝐴𝐶𝑌 = 𝑋) → 𝑌 = 𝑋)
6 isref.2 . . . . . . 7 𝑌 = 𝐵
7 isref.1 . . . . . . 7 𝑋 = 𝐴
85, 6, 73eqtr3g 2796 . . . . . 6 ((𝐴𝐶𝑌 = 𝑋) → 𝐵 = 𝐴)
9 uniexg 7681 . . . . . . 7 (𝐴𝐶 𝐴 ∈ V)
109adantr 482 . . . . . 6 ((𝐴𝐶𝑌 = 𝑋) → 𝐴 ∈ V)
118, 10eqeltrd 2834 . . . . 5 ((𝐴𝐶𝑌 = 𝑋) → 𝐵 ∈ V)
12 uniexb 7702 . . . . 5 (𝐵 ∈ V ↔ 𝐵 ∈ V)
1311, 12sylibr 233 . . . 4 ((𝐴𝐶𝑌 = 𝑋) → 𝐵 ∈ V)
1413adantrr 716 . . 3 ((𝐴𝐶 ∧ (𝑌 = 𝑋 ∧ ∀𝑥𝐴𝑦𝐵 𝑥𝑦)) → 𝐵 ∈ V)
154, 14jca 513 . 2 ((𝐴𝐶 ∧ (𝑌 = 𝑋 ∧ ∀𝑥𝐴𝑦𝐵 𝑥𝑦)) → (𝐴𝐶𝐵 ∈ V))
16 unieq 4880 . . . . . 6 (𝑎 = 𝐴 𝑎 = 𝐴)
1716, 7eqtr4di 2791 . . . . 5 (𝑎 = 𝐴 𝑎 = 𝑋)
1817eqeq2d 2744 . . . 4 (𝑎 = 𝐴 → ( 𝑏 = 𝑎 𝑏 = 𝑋))
19 raleq 3308 . . . 4 (𝑎 = 𝐴 → (∀𝑥𝑎𝑦𝑏 𝑥𝑦 ↔ ∀𝑥𝐴𝑦𝑏 𝑥𝑦))
2018, 19anbi12d 632 . . 3 (𝑎 = 𝐴 → (( 𝑏 = 𝑎 ∧ ∀𝑥𝑎𝑦𝑏 𝑥𝑦) ↔ ( 𝑏 = 𝑋 ∧ ∀𝑥𝐴𝑦𝑏 𝑥𝑦)))
21 unieq 4880 . . . . . 6 (𝑏 = 𝐵 𝑏 = 𝐵)
2221, 6eqtr4di 2791 . . . . 5 (𝑏 = 𝐵 𝑏 = 𝑌)
2322eqeq1d 2735 . . . 4 (𝑏 = 𝐵 → ( 𝑏 = 𝑋𝑌 = 𝑋))
24 rexeq 3309 . . . . 5 (𝑏 = 𝐵 → (∃𝑦𝑏 𝑥𝑦 ↔ ∃𝑦𝐵 𝑥𝑦))
2524ralbidv 3171 . . . 4 (𝑏 = 𝐵 → (∀𝑥𝐴𝑦𝑏 𝑥𝑦 ↔ ∀𝑥𝐴𝑦𝐵 𝑥𝑦))
2623, 25anbi12d 632 . . 3 (𝑏 = 𝐵 → (( 𝑏 = 𝑋 ∧ ∀𝑥𝐴𝑦𝑏 𝑥𝑦) ↔ (𝑌 = 𝑋 ∧ ∀𝑥𝐴𝑦𝐵 𝑥𝑦)))
27 df-ref 22879 . . 3 Ref = {⟨𝑎, 𝑏⟩ ∣ ( 𝑏 = 𝑎 ∧ ∀𝑥𝑎𝑦𝑏 𝑥𝑦)}
2820, 26, 27brabg 5500 . 2 ((𝐴𝐶𝐵 ∈ V) → (𝐴Ref𝐵 ↔ (𝑌 = 𝑋 ∧ ∀𝑥𝐴𝑦𝐵 𝑥𝑦)))
293, 15, 28pm5.21nd 801 1 (𝐴𝐶 → (𝐴Ref𝐵 ↔ (𝑌 = 𝑋 ∧ ∀𝑥𝐴𝑦𝐵 𝑥𝑦)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397   = wceq 1542  wcel 2107  wral 3061  wrex 3070  Vcvv 3447  wss 3914   cuni 4869   class class class wbr 5109  Refcref 22876
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5260  ax-nul 5267  ax-pow 5324  ax-pr 5388  ax-un 7676
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3062  df-rex 3071  df-rab 3407  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4287  df-if 4491  df-pw 4566  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4870  df-br 5110  df-opab 5172  df-xp 5643  df-rel 5644  df-ref 22879
This theorem is referenced by:  refbas  22884  refssex  22885  ssref  22886  refref  22887  reftr  22888  refun0  22889  dissnref  22902  reff  32484  locfinreflem  32485  cmpcref  32495  fnessref  34882  refssfne  34883
  Copyright terms: Public domain W3C validator