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 33694. 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 22099 | . . . 4 ⊢ Rel Ref | |
2 | 1 | brrelex2i 5595 | . . 3 ⊢ (𝐴Ref𝐵 → 𝐵 ∈ V) |
3 | 2 | anim2i 618 | . 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐴Ref𝐵) → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ V)) |
4 | simpl 485 | . . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ (𝑌 = 𝑋 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦)) → 𝐴 ∈ 𝐶) | |
5 | simpr 487 | . . . . . . 7 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝑌 = 𝑋) → 𝑌 = 𝑋) | |
6 | isref.2 | . . . . . . 7 ⊢ 𝑌 = ∪ 𝐵 | |
7 | isref.1 | . . . . . . 7 ⊢ 𝑋 = ∪ 𝐴 | |
8 | 5, 6, 7 | 3eqtr3g 2879 | . . . . . 6 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝑌 = 𝑋) → ∪ 𝐵 = ∪ 𝐴) |
9 | uniexg 7452 | . . . . . . 7 ⊢ (𝐴 ∈ 𝐶 → ∪ 𝐴 ∈ V) | |
10 | 9 | adantr 483 | . . . . . 6 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝑌 = 𝑋) → ∪ 𝐴 ∈ V) |
11 | 8, 10 | eqeltrd 2913 | . . . . 5 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝑌 = 𝑋) → ∪ 𝐵 ∈ V) |
12 | uniexb 7472 | . . . . 5 ⊢ (𝐵 ∈ V ↔ ∪ 𝐵 ∈ V) | |
13 | 11, 12 | sylibr 236 | . . . 4 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝑌 = 𝑋) → 𝐵 ∈ V) |
14 | 13 | adantrr 715 | . . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ (𝑌 = 𝑋 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦)) → 𝐵 ∈ V) |
15 | 4, 14 | jca 514 | . 2 ⊢ ((𝐴 ∈ 𝐶 ∧ (𝑌 = 𝑋 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦)) → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ V)) |
16 | unieq 4835 | . . . . . 6 ⊢ (𝑎 = 𝐴 → ∪ 𝑎 = ∪ 𝐴) | |
17 | 16, 7 | syl6eqr 2874 | . . . . 5 ⊢ (𝑎 = 𝐴 → ∪ 𝑎 = 𝑋) |
18 | 17 | eqeq2d 2832 | . . . 4 ⊢ (𝑎 = 𝐴 → (∪ 𝑏 = ∪ 𝑎 ↔ ∪ 𝑏 = 𝑋)) |
19 | raleq 3405 | . . . 4 ⊢ (𝑎 = 𝐴 → (∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝑥 ⊆ 𝑦 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑏 𝑥 ⊆ 𝑦)) | |
20 | 18, 19 | anbi12d 632 | . . 3 ⊢ (𝑎 = 𝐴 → ((∪ 𝑏 = ∪ 𝑎 ∧ ∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝑥 ⊆ 𝑦) ↔ (∪ 𝑏 = 𝑋 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑏 𝑥 ⊆ 𝑦))) |
21 | unieq 4835 | . . . . . 6 ⊢ (𝑏 = 𝐵 → ∪ 𝑏 = ∪ 𝐵) | |
22 | 21, 6 | syl6eqr 2874 | . . . . 5 ⊢ (𝑏 = 𝐵 → ∪ 𝑏 = 𝑌) |
23 | 22 | eqeq1d 2823 | . . . 4 ⊢ (𝑏 = 𝐵 → (∪ 𝑏 = 𝑋 ↔ 𝑌 = 𝑋)) |
24 | rexeq 3406 | . . . . 5 ⊢ (𝑏 = 𝐵 → (∃𝑦 ∈ 𝑏 𝑥 ⊆ 𝑦 ↔ ∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦)) | |
25 | 24 | ralbidv 3197 | . . . 4 ⊢ (𝑏 = 𝐵 → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑏 𝑥 ⊆ 𝑦 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦)) |
26 | 23, 25 | anbi12d 632 | . . 3 ⊢ (𝑏 = 𝐵 → ((∪ 𝑏 = 𝑋 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑏 𝑥 ⊆ 𝑦) ↔ (𝑌 = 𝑋 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦))) |
27 | df-ref 22096 | . . 3 ⊢ Ref = {〈𝑎, 𝑏〉 ∣ (∪ 𝑏 = ∪ 𝑎 ∧ ∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝑥 ⊆ 𝑦)} | |
28 | 20, 26, 27 | brabg 5412 | . 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ V) → (𝐴Ref𝐵 ↔ (𝑌 = 𝑋 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦))) |
29 | 3, 15, 28 | pm5.21nd 800 | 1 ⊢ (𝐴 ∈ 𝐶 → (𝐴Ref𝐵 ↔ (𝑌 = 𝑋 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 = wceq 1537 ∈ wcel 2114 ∀wral 3138 ∃wrex 3139 Vcvv 3486 ⊆ wss 3924 ∪ cuni 4824 class class class wbr 5052 Refcref 22093 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 ax-sep 5189 ax-nul 5196 ax-pow 5252 ax-pr 5316 ax-un 7447 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ral 3143 df-rex 3144 df-rab 3147 df-v 3488 df-dif 3927 df-un 3929 df-in 3931 df-ss 3940 df-nul 4280 df-if 4454 df-pw 4527 df-sn 4554 df-pr 4556 df-op 4560 df-uni 4825 df-br 5053 df-opab 5115 df-xp 5547 df-rel 5548 df-ref 22096 |
This theorem is referenced by: refbas 22101 refssex 22102 ssref 22103 refref 22104 reftr 22105 refun0 22106 dissnref 22119 reff 31113 locfinreflem 31114 cmpcref 31124 fnessref 33712 refssfne 33713 |
Copyright terms: Public domain | W3C validator |