![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > isref | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
isref.1 | ⊢ 𝑋 = ∪ 𝐴 |
isref.2 | ⊢ 𝑌 = ∪ 𝐵 |
Ref | Expression |
---|---|
isref | ⊢ (𝐴 ∈ 𝐶 → (𝐴Ref𝐵 ↔ (𝑌 = 𝑋 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | refrel 21820 | . . . 4 ⊢ Rel Ref | |
2 | 1 | brrelex2i 5459 | . . 3 ⊢ (𝐴Ref𝐵 → 𝐵 ∈ V) |
3 | 2 | anim2i 607 | . 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐴Ref𝐵) → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ V)) |
4 | simpl 475 | . . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ (𝑌 = 𝑋 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦)) → 𝐴 ∈ 𝐶) | |
5 | simpr 477 | . . . . . . 7 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝑌 = 𝑋) → 𝑌 = 𝑋) | |
6 | isref.2 | . . . . . . 7 ⊢ 𝑌 = ∪ 𝐵 | |
7 | isref.1 | . . . . . . 7 ⊢ 𝑋 = ∪ 𝐴 | |
8 | 5, 6, 7 | 3eqtr3g 2838 | . . . . . 6 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝑌 = 𝑋) → ∪ 𝐵 = ∪ 𝐴) |
9 | uniexg 7285 | . . . . . . 7 ⊢ (𝐴 ∈ 𝐶 → ∪ 𝐴 ∈ V) | |
10 | 9 | adantr 473 | . . . . . 6 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝑌 = 𝑋) → ∪ 𝐴 ∈ V) |
11 | 8, 10 | eqeltrd 2867 | . . . . 5 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝑌 = 𝑋) → ∪ 𝐵 ∈ V) |
12 | uniexb 7303 | . . . . 5 ⊢ (𝐵 ∈ V ↔ ∪ 𝐵 ∈ V) | |
13 | 11, 12 | sylibr 226 | . . . 4 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝑌 = 𝑋) → 𝐵 ∈ V) |
14 | 13 | adantrr 704 | . . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ (𝑌 = 𝑋 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦)) → 𝐵 ∈ V) |
15 | 4, 14 | jca 504 | . 2 ⊢ ((𝐴 ∈ 𝐶 ∧ (𝑌 = 𝑋 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦)) → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ V)) |
16 | unieq 4720 | . . . . . 6 ⊢ (𝑎 = 𝐴 → ∪ 𝑎 = ∪ 𝐴) | |
17 | 16, 7 | syl6eqr 2833 | . . . . 5 ⊢ (𝑎 = 𝐴 → ∪ 𝑎 = 𝑋) |
18 | 17 | eqeq2d 2789 | . . . 4 ⊢ (𝑎 = 𝐴 → (∪ 𝑏 = ∪ 𝑎 ↔ ∪ 𝑏 = 𝑋)) |
19 | raleq 3346 | . . . 4 ⊢ (𝑎 = 𝐴 → (∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝑥 ⊆ 𝑦 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑏 𝑥 ⊆ 𝑦)) | |
20 | 18, 19 | anbi12d 621 | . . 3 ⊢ (𝑎 = 𝐴 → ((∪ 𝑏 = ∪ 𝑎 ∧ ∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝑥 ⊆ 𝑦) ↔ (∪ 𝑏 = 𝑋 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑏 𝑥 ⊆ 𝑦))) |
21 | unieq 4720 | . . . . . 6 ⊢ (𝑏 = 𝐵 → ∪ 𝑏 = ∪ 𝐵) | |
22 | 21, 6 | syl6eqr 2833 | . . . . 5 ⊢ (𝑏 = 𝐵 → ∪ 𝑏 = 𝑌) |
23 | 22 | eqeq1d 2781 | . . . 4 ⊢ (𝑏 = 𝐵 → (∪ 𝑏 = 𝑋 ↔ 𝑌 = 𝑋)) |
24 | rexeq 3347 | . . . . 5 ⊢ (𝑏 = 𝐵 → (∃𝑦 ∈ 𝑏 𝑥 ⊆ 𝑦 ↔ ∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦)) | |
25 | 24 | ralbidv 3148 | . . . 4 ⊢ (𝑏 = 𝐵 → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑏 𝑥 ⊆ 𝑦 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦)) |
26 | 23, 25 | anbi12d 621 | . . 3 ⊢ (𝑏 = 𝐵 → ((∪ 𝑏 = 𝑋 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑏 𝑥 ⊆ 𝑦) ↔ (𝑌 = 𝑋 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦))) |
27 | df-ref 21817 | . . 3 ⊢ Ref = {〈𝑎, 𝑏〉 ∣ (∪ 𝑏 = ∪ 𝑎 ∧ ∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝑥 ⊆ 𝑦)} | |
28 | 20, 26, 27 | brabg 5280 | . 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ V) → (𝐴Ref𝐵 ↔ (𝑌 = 𝑋 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦))) |
29 | 3, 15, 28 | pm5.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 |