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→ARefB↔⋃B⊆⋃A∧∃ff:A⟶B∧∀v∈Av⊆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→ARefB↔⋃B=⋃A∧∀v∈A∃u∈Bv⊆u
5 4 simprbda ⊢A∈V∧ARefB→⋃B=⋃A
6 1 5 sseqtrid ⊢A∈V∧ARefB→⋃B⊆⋃A
7 4 simplbda ⊢A∈V∧ARefB→∀v∈A∃u∈Bv⊆u
8 sseq2 ⊢u=f⁡v→v⊆u↔v⊆f⁡v
9 8 ac6sg ⊢A∈V→∀v∈A∃u∈Bv⊆u→∃ff:A⟶B∧∀v∈Av⊆f⁡v
10 9 adantr ⊢A∈V∧ARefB→∀v∈A∃u∈Bv⊆u→∃ff:A⟶B∧∀v∈Av⊆f⁡v
11 7 10 mpd ⊢A∈V∧ARefB→∃ff:A⟶B∧∀v∈Av⊆f⁡v
12 6 11 jca ⊢A∈V∧ARefB→⋃B⊆⋃A∧∃ff:A⟶B∧∀v∈Av⊆f⁡v
13 simplr ⊢A∈V∧⋃B⊆⋃A∧f:A⟶B∧∀v∈Av⊆f⁡v→⋃B⊆⋃A
14 nfv ⊢ℲvA∈V∧⋃B⊆⋃A
15 nfv ⊢Ⅎvf:A⟶B
16 nfra1 ⊢Ⅎv∀v∈Av⊆f⁡v
17 15 16 nfan ⊢Ⅎvf:A⟶B∧∀v∈Av⊆f⁡v
18 14 17 nfan ⊢ℲvA∈V∧⋃B⊆⋃A∧f:A⟶B∧∀v∈Av⊆f⁡v
19 nfv ⊢Ⅎvx∈⋃A
20 18 19 nfan ⊢ℲvA∈V∧⋃B⊆⋃A∧f:A⟶B∧∀v∈Av⊆f⁡v∧x∈⋃A
21 simplrl ⊢A∈V∧⋃B⊆⋃A∧f:A⟶B∧∀v∈Av⊆f⁡v∧v∈A→f:A⟶B
22 simpr ⊢A∈V∧⋃B⊆⋃A∧f:A⟶B∧∀v∈Av⊆f⁡v∧v∈A→v∈A
23 21 22 ffvelcdmd ⊢A∈V∧⋃B⊆⋃A∧f:A⟶B∧∀v∈Av⊆f⁡v∧v∈A→f⁡v∈B
24 23 adantlr ⊢A∈V∧⋃B⊆⋃A∧f:A⟶B∧∀v∈Av⊆f⁡v∧x∈⋃A∧v∈A→f⁡v∈B
25 24 adantr ⊢A∈V∧⋃B⊆⋃A∧f:A⟶B∧∀v∈Av⊆f⁡v∧x∈⋃A∧v∈A∧x∈v→f⁡v∈B
26 simplrr ⊢A∈V∧⋃B⊆⋃A∧f:A⟶B∧∀v∈Av⊆f⁡v∧v∈A→∀v∈Av⊆f⁡v
27 26 adantlr ⊢A∈V∧⋃B⊆⋃A∧f:A⟶B∧∀v∈Av⊆f⁡v∧x∈⋃A∧v∈A→∀v∈Av⊆f⁡v
28 simpr ⊢A∈V∧⋃B⊆⋃A∧f:A⟶B∧∀v∈Av⊆f⁡v∧x∈⋃A∧v∈A→v∈A
29 rspa ⊢∀v∈Av⊆f⁡v∧v∈A→v⊆f⁡v
30 27 28 29 syl2anc ⊢A∈V∧⋃B⊆⋃A∧f:A⟶B∧∀v∈Av⊆f⁡v∧x∈⋃A∧v∈A→v⊆f⁡v
31 30 sselda ⊢A∈V∧⋃B⊆⋃A∧f:A⟶B∧∀v∈Av⊆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∈Bx∈u
34 25 31 33 syl2anc ⊢A∈V∧⋃B⊆⋃A∧f:A⟶B∧∀v∈Av⊆f⁡v∧x∈⋃A∧v∈A∧x∈v→∃u∈Bx∈u
35 simpr ⊢A∈V∧⋃B⊆⋃A∧f:A⟶B∧∀v∈Av⊆f⁡v∧x∈⋃A→x∈⋃A
36 eluni2 ⊢x∈⋃A↔∃v∈Ax∈v
37 35 36 sylib ⊢A∈V∧⋃B⊆⋃A∧f:A⟶B∧∀v∈Av⊆f⁡v∧x∈⋃A→∃v∈Ax∈v
38 20 34 37 r19.29af ⊢A∈V∧⋃B⊆⋃A∧f:A⟶B∧∀v∈Av⊆f⁡v∧x∈⋃A→∃u∈Bx∈u
39 eluni2 ⊢x∈⋃B↔∃u∈Bx∈u
40 38 39 sylibr ⊢A∈V∧⋃B⊆⋃A∧f:A⟶B∧∀v∈Av⊆f⁡v∧x∈⋃A→x∈⋃B
41 13 40 eqelssd ⊢A∈V∧⋃B⊆⋃A∧f:A⟶B∧∀v∈Av⊆f⁡v→⋃B=⋃A
42 26 22 29 syl2anc ⊢A∈V∧⋃B⊆⋃A∧f:A⟶B∧∀v∈Av⊆f⁡v∧v∈A→v⊆f⁡v
43 8 rspcev ⊢f⁡v∈B∧v⊆f⁡v→∃u∈Bv⊆u
44 23 42 43 syl2anc ⊢A∈V∧⋃B⊆⋃A∧f:A⟶B∧∀v∈Av⊆f⁡v∧v∈A→∃u∈Bv⊆u
45 44 ex ⊢A∈V∧⋃B⊆⋃A∧f:A⟶B∧∀v∈Av⊆f⁡v→v∈A→∃u∈Bv⊆u
46 18 45 ralrimi ⊢A∈V∧⋃B⊆⋃A∧f:A⟶B∧∀v∈Av⊆f⁡v→∀v∈A∃u∈Bv⊆u
47 4 ad2antrr ⊢A∈V∧⋃B⊆⋃A∧f:A⟶B∧∀v∈Av⊆f⁡v→ARefB↔⋃B=⋃A∧∀v∈A∃u∈Bv⊆u
48 41 46 47 mpbir2and ⊢A∈V∧⋃B⊆⋃A∧f:A⟶B∧∀v∈Av⊆f⁡v→ARefB
49 48 ex ⊢A∈V∧⋃B⊆⋃A→f:A⟶B∧∀v∈Av⊆f⁡v→ARefB
50 49 exlimdv ⊢A∈V∧⋃B⊆⋃A→∃ff:A⟶B∧∀v∈Av⊆f⁡v→ARefB
51 50 impr ⊢A∈V∧⋃B⊆⋃A∧∃ff:A⟶B∧∀v∈Av⊆f⁡v→ARefB
52 12 51 impbida ⊢A∈V→ARefB↔⋃B⊆⋃A∧∃ff:A⟶B∧∀v∈Av⊆f⁡v