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)

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 ssid ⊢ ⋃ B ⊆ ⋃ B
2 eqid ⊢ ⋃ A = ⋃ A
3 eqid ⊢ ⋃ B = ⋃ B
4 2 3 isref ⊢ A ∈ V → A Ref B ↔ ⋃ B = ⋃ A ∧ ∀ v ∈ A ∃ u ∈ B v ⊆ u
5 4 simprbda ⊢ A ∈ V ∧ A Ref B → ⋃ B = ⋃ A
6 1 5 sseqtrid ⊢ A ∈ V ∧ A Ref B → ⋃ B ⊆ ⋃ A
7 4 simplbda ⊢ A ∈ V ∧ A Ref B → ∀ v ∈ A ∃ u ∈ B v ⊆ u
8 sseq2 ⊢ u = f ⁡ v → v ⊆ u ↔ v ⊆ f ⁡ v
9 8 ac6sg ⊢ A ∈ V → ∀ v ∈ A ∃ u ∈ B v ⊆ u → ∃ f f : A ⟶ B ∧ ∀ v ∈ A v ⊆ f ⁡ v
10 9 adantr ⊢ A ∈ V ∧ A Ref B → ∀ v ∈ A ∃ u ∈ B v ⊆ u → ∃ f f : A ⟶ B ∧ ∀ v ∈ A v ⊆ f ⁡ v
11 7 10 mpd ⊢ A ∈ V ∧ A Ref B → ∃ f f : A ⟶ B ∧ ∀ v ∈ A v ⊆ f ⁡ v
12 6 11 jca ⊢ A ∈ V ∧ A Ref B → ⋃ B ⊆ ⋃ A ∧ ∃ f f : A ⟶ B ∧ ∀ v ∈ A v ⊆ f ⁡ v
13 simplr ⊢ A ∈ V ∧ ⋃ B ⊆ ⋃ A ∧ f : A ⟶ B ∧ ∀ v ∈ A v ⊆ f ⁡ v → ⋃ B ⊆ ⋃ A
14 nfv ⊢ Ⅎ v A ∈ V ∧ ⋃ B ⊆ ⋃ A
15 nfv ⊢ Ⅎ v f : A ⟶ B
16 nfra1 ⊢ Ⅎ v ∀ v ∈ A v ⊆ f ⁡ v
17 15 16 nfan ⊢ Ⅎ v f : A ⟶ B ∧ ∀ v ∈ A v ⊆ f ⁡ v
18 14 17 nfan ⊢ Ⅎ v A ∈ V ∧ ⋃ B ⊆ ⋃ A ∧ f : A ⟶ B ∧ ∀ v ∈ A v ⊆ f ⁡ v
19 nfv ⊢ Ⅎ v x ∈ ⋃ A
20 18 19 nfan ⊢ Ⅎ v A ∈ V ∧ ⋃ B ⊆ ⋃ A ∧ f : A ⟶ B ∧ ∀ v ∈ A v ⊆ f ⁡ v ∧ x ∈ ⋃ A
21 simplrl ⊢ A ∈ V ∧ ⋃ B ⊆ ⋃ A ∧ f : A ⟶ B ∧ ∀ v ∈ A v ⊆ f ⁡ v ∧ v ∈ A → f : A ⟶ B
22 simpr ⊢ A ∈ V ∧ ⋃ B ⊆ ⋃ A ∧ f : A ⟶ B ∧ ∀ v ∈ A v ⊆ f ⁡ v ∧ v ∈ A → v ∈ A
23 21 22 ffvelcdmd ⊢ A ∈ V ∧ ⋃ B ⊆ ⋃ A ∧ f : A ⟶ B ∧ ∀ v ∈ A v ⊆ f ⁡ v ∧ v ∈ A → f ⁡ v ∈ B
24 23 adantlr ⊢ A ∈ V ∧ ⋃ B ⊆ ⋃ A ∧ f : A ⟶ B ∧ ∀ v ∈ A v ⊆ f ⁡ v ∧ x ∈ ⋃ A ∧ v ∈ A → f ⁡ v ∈ B
25 24 adantr ⊢ A ∈ V ∧ ⋃ B ⊆ ⋃ A ∧ f : A ⟶ B ∧ ∀ v ∈ A v ⊆ f ⁡ v ∧ x ∈ ⋃ A ∧ v ∈ A ∧ x ∈ v → f ⁡ v ∈ B
26 simplrr ⊢ A ∈ V ∧ ⋃ B ⊆ ⋃ A ∧ f : A ⟶ B ∧ ∀ v ∈ A v ⊆ f ⁡ v ∧ v ∈ A → ∀ v ∈ A v ⊆ f ⁡ v
27 26 adantlr ⊢ A ∈ V ∧ ⋃ B ⊆ ⋃ A ∧ f : A ⟶ B ∧ ∀ v ∈ A v ⊆ f ⁡ v ∧ x ∈ ⋃ A ∧ v ∈ A → ∀ v ∈ A v ⊆ f ⁡ v
28 simpr ⊢ A ∈ V ∧ ⋃ B ⊆ ⋃ A ∧ f : A ⟶ B ∧ ∀ v ∈ A v ⊆ f ⁡ v ∧ x ∈ ⋃ A ∧ v ∈ A → v ∈ A
29 rspa ⊢ ∀ v ∈ A v ⊆ f ⁡ v ∧ v ∈ A → v ⊆ f ⁡ v
30 27 28 29 syl2anc ⊢ A ∈ V ∧ ⋃ B ⊆ ⋃ A ∧ f : A ⟶ B ∧ ∀ v ∈ A v ⊆ f ⁡ v ∧ x ∈ ⋃ A ∧ v ∈ A → v ⊆ f ⁡ v
31 30 sselda ⊢ A ∈ V ∧ ⋃ B ⊆ ⋃ A ∧ f : A ⟶ B ∧ ∀ v ∈ A v ⊆ f ⁡ v ∧ x ∈ ⋃ A ∧ v ∈ A ∧ x ∈ v → x ∈ f ⁡ v
32 eleq2 ⊢ u = f ⁡ v → x ∈ u ↔ x ∈ f ⁡ v
33 32 rspcev ⊢ f ⁡ v ∈ B ∧ x ∈ f ⁡ v → ∃ u ∈ B x ∈ u
34 25 31 33 syl2anc ⊢ A ∈ V ∧ ⋃ B ⊆ ⋃ A ∧ f : A ⟶ B ∧ ∀ v ∈ A v ⊆ f ⁡ v ∧ x ∈ ⋃ A ∧ v ∈ A ∧ x ∈ v → ∃ u ∈ B x ∈ u
35 eluni2 ⊢ x ∈ ⋃ A ↔ ∃ v ∈ A x ∈ v
36 35 bilani ⊢ A ∈ V ∧ ⋃ B ⊆ ⋃ A ∧ f : A ⟶ B ∧ ∀ v ∈ A v ⊆ f ⁡ v ∧ x ∈ ⋃ A → ∃ v ∈ A x ∈ v
37 20 34 36 r19.29af ⊢ A ∈ V ∧ ⋃ B ⊆ ⋃ A ∧ f : A ⟶ B ∧ ∀ v ∈ A v ⊆ f ⁡ v ∧ x ∈ ⋃ A → ∃ u ∈ B x ∈ u
38 eluni2 ⊢ x ∈ ⋃ B ↔ ∃ u ∈ B x ∈ u
39 37 38 sylibr ⊢ A ∈ V ∧ ⋃ B ⊆ ⋃ A ∧ f : A ⟶ B ∧ ∀ v ∈ A v ⊆ f ⁡ v ∧ x ∈ ⋃ A → x ∈ ⋃ B
40 13 39 eqelssd ⊢ A ∈ V ∧ ⋃ B ⊆ ⋃ A ∧ f : A ⟶ B ∧ ∀ v ∈ A v ⊆ f ⁡ v → ⋃ B = ⋃ A
41 26 22 29 syl2anc ⊢ A ∈ V ∧ ⋃ B ⊆ ⋃ A ∧ f : A ⟶ B ∧ ∀ v ∈ A v ⊆ f ⁡ v ∧ v ∈ A → v ⊆ f ⁡ v
42 8 rspcev ⊢ f ⁡ v ∈ B ∧ v ⊆ f ⁡ v → ∃ u ∈ B v ⊆ u
43 23 41 42 syl2anc ⊢ A ∈ V ∧ ⋃ B ⊆ ⋃ A ∧ f : A ⟶ B ∧ ∀ v ∈ A v ⊆ f ⁡ v ∧ v ∈ A → ∃ u ∈ B v ⊆ u
44 43 ex ⊢ A ∈ V ∧ ⋃ B ⊆ ⋃ A ∧ f : A ⟶ B ∧ ∀ v ∈ A v ⊆ f ⁡ v → v ∈ A → ∃ u ∈ B v ⊆ u
45 18 44 ralrimi ⊢ A ∈ V ∧ ⋃ B ⊆ ⋃ A ∧ f : A ⟶ B ∧ ∀ v ∈ A v ⊆ f ⁡ v → ∀ v ∈ A ∃ u ∈ B v ⊆ u
46 4 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 40 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 12 50 impbida ⊢ A ∈ V → A Ref B ↔ ⋃ B ⊆ ⋃ A ∧ ∃ f f : A ⟶ B ∧ ∀ v ∈ A v ⊆ f ⁡ v