Metamath Proof Explorer

Theorem isref

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 . 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
Hypotheses isref.1 ⊢ X = ⋃ A
isref.2 ⊢ Y = ⋃ B
Assertion isref ⊢ A ∈ C → A Ref B ↔ Y = X ∧ ∀ x ∈ A ∃ y ∈ B x ⊆ y

Proof

Step Hyp Ref Expression
1 isref.1 ⊢ X = ⋃ A
2 isref.2 ⊢ Y = ⋃ B
3 refrel ⊢ Rel ⁡ Ref
4 3 brrelex2i ⊢ A Ref B → B ∈ V
5 4 anim2i ⊢ A ∈ C ∧ A Ref B → A ∈ C ∧ B ∈ V
6 simpl ⊢ A ∈ C ∧ Y = X ∧ ∀ x ∈ A ∃ y ∈ B x ⊆ y → A ∈ C
7 simpr ⊢ A ∈ C ∧ Y = X → Y = X
8 7 2 1 3eqtr3g ⊢ A ∈ C ∧ Y = X → ⋃ B = ⋃ A
9 uniexg ⊢ A ∈ C → ⋃ A ∈ V
10 9 adantr ⊢ A ∈ C ∧ Y = X → ⋃ A ∈ V
11 8 10 eqeltrd ⊢ A ∈ C ∧ Y = X → ⋃ B ∈ V
12 uniexb ⊢ B ∈ V ↔ ⋃ B ∈ V
13 11 12 sylibr ⊢ A ∈ C ∧ Y = X → B ∈ V
14 13 adantrr ⊢ A ∈ C ∧ Y = X ∧ ∀ x ∈ A ∃ y ∈ B x ⊆ y → B ∈ V
15 6 14 jca ⊢ A ∈ C ∧ Y = X ∧ ∀ x ∈ A ∃ y ∈ B x ⊆ y → A ∈ C ∧ B ∈ V
16 unieq ⊢ a = A → ⋃ a = ⋃ A
17 16 1 eqtr4di ⊢ a = A → ⋃ a = X
18 17 eqeq2d ⊢ a = A → ⋃ b = ⋃ a ↔ ⋃ b = X
19 raleq ⊢ a = A → ∀ x ∈ a ∃ y ∈ b x ⊆ y ↔ ∀ x ∈ A ∃ y ∈ b x ⊆ y
20 18 19 anbi12d ⊢ a = A → ⋃ b = ⋃ a ∧ ∀ x ∈ a ∃ y ∈ b x ⊆ y ↔ ⋃ b = X ∧ ∀ x ∈ A ∃ y ∈ b x ⊆ y
21 unieq ⊢ b = B → ⋃ b = ⋃ B
22 21 2 eqtr4di ⊢ b = B → ⋃ b = Y
23 22 eqeq1d ⊢ b = B → ⋃ b = X ↔ Y = X
24 rexeq ⊢ b = B → ∃ y ∈ b x ⊆ y ↔ ∃ y ∈ B x ⊆ y
25 24 ralbidv ⊢ b = B → ∀ x ∈ A ∃ y ∈ b x ⊆ y ↔ ∀ x ∈ A ∃ y ∈ B x ⊆ y
26 23 25 anbi12d ⊢ b = B → ⋃ b = X ∧ ∀ x ∈ A ∃ y ∈ b x ⊆ y ↔ Y = X ∧ ∀ x ∈ A ∃ y ∈ B x ⊆ y
27 df-ref ⊢ Ref = a b | ⋃ b = ⋃ a ∧ ∀ x ∈ a ∃ y ∈ b x ⊆ y
28 20 26 27 brabg ⊢ A ∈ C ∧ B ∈ V → A Ref B ↔ Y = X ∧ ∀ x ∈ A ∃ y ∈ B x ⊆ y
29 5 15 28 pm5.21nd ⊢ A ∈ C → A Ref B ↔ Y = X ∧ ∀ x ∈ A ∃ y ∈ B x ⊆ y