Metamath Proof Explorer

Theorem reff

Description: For any cover refinement, there exists a function associating with each set in the refinement a set in the original cover containing it. This is sometimes used as a definition of refinement. Note that this definition uses the axiom of choice through ac6sg . (Contributed by Thierry Arnoux, 12-Jan-2020) Remove dependency on ax-reg and ax-inf2 . (Revised by Timothy J. O'Malley, 15-Oct-2026)

Ref Expression
Assertion reff ⊢ A ∈ V → A Ref B ↔ ⋃ B ⊆ ⋃ A ∧ ∃ f f : A ⟶ B ∧ ∀ v ∈ A v ⊆ f ⁡ v

Proof

Step Hyp Ref Expression
1 eqid ⊢ ⋃ A = ⋃ A
2 eqid ⊢ ⋃ B = ⋃ B
3 1 2 isref ⊢ A ∈ V → A Ref B ↔ ⋃ B = ⋃ A ∧ ∀ v ∈ A ∃ u ∈ B v ⊆ u
4 3 simprbda ⊢ A ∈ V ∧ A Ref B → ⋃ B = ⋃ A
5 4 eqimssd ⊢ A ∈ V ∧ A Ref B → ⋃ B ⊆ ⋃ A
6 simpl ⊢ A ∈ V ∧ A Ref B → A ∈ V
7 uniexg ⊢ A ∈ V → ⋃ A ∈ V
8 pwexg ⊢ ⋃ A ∈ V → 𝒫 ⋃ A ∈ V
9 6 7 8 3syl ⊢ A ∈ V ∧ A Ref B → 𝒫 ⋃ A ∈ V
10 sspwuni ⊢ B ⊆ 𝒫 ⋃ A ↔ ⋃ B ⊆ ⋃ A
11 5 10 sylibr ⊢ A ∈ V ∧ A Ref B → B ⊆ 𝒫 ⋃ A
12 9 11 ssexd ⊢ A ∈ V ∧ A Ref B → B ∈ V
13 3 simplbda ⊢ A ∈ V ∧ A Ref B → ∀ v ∈ A ∃ u ∈ B v ⊆ u
14 sseq2 ⊢ u = f ⁡ v → v ⊆ u ↔ v ⊆ f ⁡ v
15 14 ac6 ⊢ A ∈ V ∧ B ∈ V ∧ ∀ v ∈ A ∃ u ∈ B v ⊆ u → ∃ f f : A ⟶ B ∧ ∀ v ∈ A v ⊆ f ⁡ v
16 6 12 13 15 syl3anc ⊢ A ∈ V ∧ A Ref B → ∃ f f : A ⟶ B ∧ ∀ v ∈ A v ⊆ f ⁡ v
17 5 16 jca ⊢ A ∈ V ∧ A Ref B → ⋃ B ⊆ ⋃ A ∧ ∃ f f : A ⟶ B ∧ ∀ v ∈ A v ⊆ f ⁡ v
18 simplr ⊢ A ∈ V ∧ ⋃ B ⊆ ⋃ A ∧ f : A ⟶ B ∧ ∀ v ∈ A v ⊆ f ⁡ v → ⋃ B ⊆ ⋃ A
19 nfv ⊢ Ⅎ v A ∈ V ∧ ⋃ B ⊆ ⋃ A
20 nfv ⊢ Ⅎ v f : A ⟶ B
21 nfra1 ⊢ Ⅎ v ∀ v ∈ A v ⊆ f ⁡ v
22 20 21 nfan ⊢ Ⅎ v f : A ⟶ B ∧ ∀ v ∈ A v ⊆ f ⁡ v
23 19 22 nfan ⊢ Ⅎ v A ∈ V ∧ ⋃ B ⊆ ⋃ A ∧ f : A ⟶ B ∧ ∀ v ∈ A v ⊆ f ⁡ v
24 nfv ⊢ Ⅎ v x ∈ ⋃ A
25 23 24 nfan ⊢ Ⅎ v A ∈ V ∧ ⋃ B ⊆ ⋃ A ∧ f : A ⟶ B ∧ ∀ v ∈ A v ⊆ f ⁡ v ∧ x ∈ ⋃ A
26 eleq2 ⊢ u = f ⁡ v → x ∈ u ↔ x ∈ f ⁡ v
27 simplrl ⊢ A ∈ V ∧ ⋃ B ⊆ ⋃ A ∧ f : A ⟶ B ∧ ∀ v ∈ A v ⊆ f ⁡ v ∧ v ∈ A → f : A ⟶ B
28 simpr ⊢ A ∈ V ∧ ⋃ B ⊆ ⋃ A ∧ f : A ⟶ B ∧ ∀ v ∈ A v ⊆ f ⁡ v ∧ v ∈ A → v ∈ A
29 27 28 ffvelcdmd ⊢ A ∈ V ∧ ⋃ B ⊆ ⋃ A ∧ f : A ⟶ B ∧ ∀ v ∈ A v ⊆ f ⁡ v ∧ v ∈ A → f ⁡ v ∈ B
30 29 ad4ant13 ⊢ A ∈ V ∧ ⋃ B ⊆ ⋃ A ∧ f : A ⟶ B ∧ ∀ v ∈ A v ⊆ f ⁡ v ∧ x ∈ ⋃ A ∧ v ∈ A ∧ x ∈ v → f ⁡ v ∈ B
31 simplrr ⊢ A ∈ V ∧ ⋃ B ⊆ ⋃ A ∧ f : A ⟶ B ∧ ∀ v ∈ A v ⊆ f ⁡ v ∧ v ∈ A → ∀ v ∈ A v ⊆ f ⁡ v
32 31 adantlr ⊢ A ∈ V ∧ ⋃ B ⊆ ⋃ A ∧ f : A ⟶ B ∧ ∀ v ∈ A v ⊆ f ⁡ v ∧ x ∈ ⋃ A ∧ v ∈ A → ∀ v ∈ A v ⊆ f ⁡ v
33 rspa ⊢ ∀ v ∈ A v ⊆ f ⁡ v ∧ v ∈ A → v ⊆ f ⁡ v
34 32 33 sylancom ⊢ A ∈ V ∧ ⋃ B ⊆ ⋃ A ∧ f : A ⟶ B ∧ ∀ v ∈ A v ⊆ f ⁡ v ∧ x ∈ ⋃ A ∧ v ∈ A → v ⊆ f ⁡ v
35 34 sselda ⊢ A ∈ V ∧ ⋃ B ⊆ ⋃ A ∧ f : A ⟶ B ∧ ∀ v ∈ A v ⊆ f ⁡ v ∧ x ∈ ⋃ A ∧ v ∈ A ∧ x ∈ v → x ∈ f ⁡ v
36 26 30 35 rspcedvdw ⊢ A ∈ V ∧ ⋃ B ⊆ ⋃ A ∧ f : A ⟶ B ∧ ∀ v ∈ A v ⊆ f ⁡ v ∧ x ∈ ⋃ A ∧ v ∈ A ∧ x ∈ v → ∃ u ∈ B x ∈ u
37 eluni2 ⊢ x ∈ ⋃ A ↔ ∃ v ∈ A x ∈ v
38 37 bilani ⊢ A ∈ V ∧ ⋃ B ⊆ ⋃ A ∧ f : A ⟶ B ∧ ∀ v ∈ A v ⊆ f ⁡ v ∧ x ∈ ⋃ A → ∃ v ∈ A x ∈ v
39 25 36 38 r19.29af ⊢ A ∈ V ∧ ⋃ B ⊆ ⋃ A ∧ f : A ⟶ B ∧ ∀ v ∈ A v ⊆ f ⁡ v ∧ x ∈ ⋃ A → ∃ u ∈ B x ∈ u
40 eluni2 ⊢ x ∈ ⋃ B ↔ ∃ u ∈ B x ∈ u
41 39 40 sylibr ⊢ A ∈ V ∧ ⋃ B ⊆ ⋃ A ∧ f : A ⟶ B ∧ ∀ v ∈ A v ⊆ f ⁡ v ∧ x ∈ ⋃ A → x ∈ ⋃ B
42 18 41 eqelssd ⊢ A ∈ V ∧ ⋃ B ⊆ ⋃ A ∧ f : A ⟶ B ∧ ∀ v ∈ A v ⊆ f ⁡ v → ⋃ B = ⋃ A
43 31 33 sylancom ⊢ A ∈ V ∧ ⋃ B ⊆ ⋃ A ∧ f : A ⟶ B ∧ ∀ v ∈ A v ⊆ f ⁡ v ∧ v ∈ A → v ⊆ f ⁡ v
44 14 29 43 rspcedvdw ⊢ A ∈ V ∧ ⋃ B ⊆ ⋃ A ∧ f : A ⟶ B ∧ ∀ v ∈ A v ⊆ f ⁡ v ∧ v ∈ A → ∃ u ∈ B v ⊆ u
45 23 44 ralrimia ⊢ A ∈ V ∧ ⋃ B ⊆ ⋃ A ∧ f : A ⟶ B ∧ ∀ v ∈ A v ⊆ f ⁡ v → ∀ v ∈ A ∃ u ∈ B v ⊆ u
46 3 ad2antrr ⊢ A ∈ V ∧ ⋃ B ⊆ ⋃ A ∧ f : A ⟶ B ∧ ∀ v ∈ A v ⊆ f ⁡ v → A Ref B ↔ ⋃ B = ⋃ A ∧ ∀ v ∈ A ∃ u ∈ B v ⊆ u
47 42 45 46 mpbir2and ⊢ A ∈ V ∧ ⋃ B ⊆ ⋃ A ∧ f : A ⟶ B ∧ ∀ v ∈ A v ⊆ f ⁡ v → A Ref B
48 47 ex ⊢ A ∈ V ∧ ⋃ B ⊆ ⋃ A → f : A ⟶ B ∧ ∀ v ∈ A v ⊆ f ⁡ v → A Ref B
49 48 exlimdv ⊢ A ∈ V ∧ ⋃ B ⊆ ⋃ A → ∃ f f : A ⟶ B ∧ ∀ v ∈ A v ⊆ f ⁡ v → A Ref B
50 49 impr ⊢ A ∈ V ∧ ⋃ B ⊆ ⋃ A ∧ ∃ f f : A ⟶ B ∧ ∀ v ∈ A v ⊆ f ⁡ v → A Ref B
51 17 50 impbida ⊢ A ∈ V → A Ref B ↔ ⋃ B ⊆ ⋃ A ∧ ∃ f f : A ⟶ B ∧ ∀ v ∈ A v ⊆ f ⁡ v