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

Theorem isref 22117
 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 33795. 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 22116 . . . 4 Rel Ref
21brrelex2i 5577 . . 3 (𝐴Ref𝐵𝐵 ∈ V)
32anim2i 619 . 2 ((𝐴𝐶𝐴Ref𝐵) → (𝐴𝐶𝐵 ∈ V))
4 simpl 486 . . 3 ((𝐴𝐶 ∧ (𝑌 = 𝑋 ∧ ∀𝑥𝐴𝑦𝐵 𝑥𝑦)) → 𝐴𝐶)
5 simpr 488 . . . . . . 7 ((𝐴𝐶𝑌 = 𝑋) → 𝑌 = 𝑋)
6 isref.2 . . . . . . 7 𝑌 = 𝐵
7 isref.1 . . . . . . 7 𝑋 = 𝐴
85, 6, 73eqtr3g 2859 . . . . . 6 ((𝐴𝐶𝑌 = 𝑋) → 𝐵 = 𝐴)
9 uniexg 7450 . . . . . . 7 (𝐴𝐶 𝐴 ∈ V)
109adantr 484 . . . . . 6 ((𝐴𝐶𝑌 = 𝑋) → 𝐴 ∈ V)
118, 10eqeltrd 2893 . . . . 5 ((𝐴𝐶𝑌 = 𝑋) → 𝐵 ∈ V)
12 uniexb 7470 . . . . 5 (𝐵 ∈ V ↔ 𝐵 ∈ V)
1311, 12sylibr 237 . . . 4 ((𝐴𝐶𝑌 = 𝑋) → 𝐵 ∈ V)
1413adantrr 716 . . 3 ((𝐴𝐶 ∧ (𝑌 = 𝑋 ∧ ∀𝑥𝐴𝑦𝐵 𝑥𝑦)) → 𝐵 ∈ V)
154, 14jca 515 . 2 ((𝐴𝐶 ∧ (𝑌 = 𝑋 ∧ ∀𝑥𝐴𝑦𝐵 𝑥𝑦)) → (𝐴𝐶𝐵 ∈ V))
16 unieq 4814 . . . . . 6 (𝑎 = 𝐴 𝑎 = 𝐴)
1716, 7eqtr4di 2854 . . . . 5 (𝑎 = 𝐴 𝑎 = 𝑋)
1817eqeq2d 2812 . . . 4 (𝑎 = 𝐴 → ( 𝑏 = 𝑎 𝑏 = 𝑋))
19 raleq 3361 . . . 4 (𝑎 = 𝐴 → (∀𝑥𝑎𝑦𝑏 𝑥𝑦 ↔ ∀𝑥𝐴𝑦𝑏 𝑥𝑦))
2018, 19anbi12d 633 . . 3 (𝑎 = 𝐴 → (( 𝑏 = 𝑎 ∧ ∀𝑥𝑎𝑦𝑏 𝑥𝑦) ↔ ( 𝑏 = 𝑋 ∧ ∀𝑥𝐴𝑦𝑏 𝑥𝑦)))
21 unieq 4814 . . . . . 6 (𝑏 = 𝐵 𝑏 = 𝐵)
2221, 6eqtr4di 2854 . . . . 5 (𝑏 = 𝐵 𝑏 = 𝑌)
2322eqeq1d 2803 . . . 4 (𝑏 = 𝐵 → ( 𝑏 = 𝑋𝑌 = 𝑋))
24 rexeq 3362 . . . . 5 (𝑏 = 𝐵 → (∃𝑦𝑏 𝑥𝑦 ↔ ∃𝑦𝐵 𝑥𝑦))
2524ralbidv 3165 . . . 4 (𝑏 = 𝐵 → (∀𝑥𝐴𝑦𝑏 𝑥𝑦 ↔ ∀𝑥𝐴𝑦𝐵 𝑥𝑦))
2623, 25anbi12d 633 . . 3 (𝑏 = 𝐵 → (( 𝑏 = 𝑋 ∧ ∀𝑥𝐴𝑦𝑏 𝑥𝑦) ↔ (𝑌 = 𝑋 ∧ ∀𝑥𝐴𝑦𝐵 𝑥𝑦)))
27 df-ref 22113 . . 3 Ref = {⟨𝑎, 𝑏⟩ ∣ ( 𝑏 = 𝑎 ∧ ∀𝑥𝑎𝑦𝑏 𝑥𝑦)}
2820, 26, 27brabg 5394 . 2 ((𝐴𝐶𝐵 ∈ V) → (𝐴Ref𝐵 ↔ (𝑌 = 𝑋 ∧ ∀𝑥𝐴𝑦𝐵 𝑥𝑦)))
293, 15, 28pm5.21nd 801 1 (𝐴𝐶 → (𝐴Ref𝐵 ↔ (𝑌 = 𝑋 ∧ ∀𝑥𝐴𝑦𝐵 𝑥𝑦)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2112  ∀wral 3109  ∃wrex 3110  Vcvv 3444   ⊆ wss 3884  ∪ cuni 4803   class class class wbr 5033  Refcref 22110 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 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ral 3114  df-rex 3115  df-rab 3118  df-v 3446  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-br 5034  df-opab 5096  df-xp 5529  df-rel 5530  df-ref 22113 This theorem is referenced by:  refbas  22118  refssex  22119  ssref  22120  refref  22121  reftr  22122  refun0  22123  dissnref  22136  reff  31192  locfinreflem  31193  cmpcref  31203  fnessref  33813  refssfne  33814
 Copyright terms: Public domain W3C validator