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 ( 𝐴 ∈ 𝑉 → ( 𝐴 Ref 𝐵 ↔ ( ∪ 𝐵 ⊆ ∪ 𝐴 ∧ ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑣 ∈ 𝐴 𝑣 ⊆ ( 𝑓 ‘ 𝑣 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ssid ⊢ ∪ 𝐵 ⊆ ∪ 𝐵
2 eqid ⊢ ∪ 𝐴 = ∪ 𝐴
3 eqid ⊢ ∪ 𝐵 = ∪ 𝐵
4 2 3 isref ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 Ref 𝐵 ↔ ( ∪ 𝐵 = ∪ 𝐴 ∧ ∀ 𝑣 ∈ 𝐴 ∃ 𝑢 ∈ 𝐵 𝑣 ⊆ 𝑢 ) ) )
5 4 simprbda ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 Ref 𝐵 ) → ∪ 𝐵 = ∪ 𝐴 )
6 1 5 sseqtrid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 Ref 𝐵 ) → ∪ 𝐵 ⊆ ∪ 𝐴 )
7 4 simplbda ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 Ref 𝐵 ) → ∀ 𝑣 ∈ 𝐴 ∃ 𝑢 ∈ 𝐵 𝑣 ⊆ 𝑢 )
8 sseq2 ⊢ ( 𝑢 = ( 𝑓 ‘ 𝑣 ) → ( 𝑣 ⊆ 𝑢 ↔ 𝑣 ⊆ ( 𝑓 ‘ 𝑣 ) ) )
9 8 ac6sg ⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑣 ∈ 𝐴 ∃ 𝑢 ∈ 𝐵 𝑣 ⊆ 𝑢 → ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑣 ∈ 𝐴 𝑣 ⊆ ( 𝑓 ‘ 𝑣 ) ) ) )
10 9 adantr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 Ref 𝐵 ) → ( ∀ 𝑣 ∈ 𝐴 ∃ 𝑢 ∈ 𝐵 𝑣 ⊆ 𝑢 → ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑣 ∈ 𝐴 𝑣 ⊆ ( 𝑓 ‘ 𝑣 ) ) ) )
11 7 10 mpd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 Ref 𝐵 ) → ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑣 ∈ 𝐴 𝑣 ⊆ ( 𝑓 ‘ 𝑣 ) ) )
12 6 11 jca ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 Ref 𝐵 ) → ( ∪ 𝐵 ⊆ ∪ 𝐴 ∧ ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑣 ∈ 𝐴 𝑣 ⊆ ( 𝑓 ‘ 𝑣 ) ) ) )
13 simplr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝐵 ⊆ ∪ 𝐴 ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑣 ∈ 𝐴 𝑣 ⊆ ( 𝑓 ‘ 𝑣 ) ) ) → ∪ 𝐵 ⊆ ∪ 𝐴 )
14 nfv ⊢ Ⅎ 𝑣 ( 𝐴 ∈ 𝑉 ∧ ∪ 𝐵 ⊆ ∪ 𝐴 )
15 nfv ⊢ Ⅎ 𝑣 𝑓 : 𝐴 ⟶ 𝐵
16 nfra1 ⊢ Ⅎ 𝑣 ∀ 𝑣 ∈ 𝐴 𝑣 ⊆ ( 𝑓 ‘ 𝑣 )
17 15 16 nfan ⊢ Ⅎ 𝑣 ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑣 ∈ 𝐴 𝑣 ⊆ ( 𝑓 ‘ 𝑣 ) )
18 14 17 nfan ⊢ Ⅎ 𝑣 ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝐵 ⊆ ∪ 𝐴 ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑣 ∈ 𝐴 𝑣 ⊆ ( 𝑓 ‘ 𝑣 ) ) )
19 nfv ⊢ Ⅎ 𝑣 𝑥 ∈ ∪ 𝐴
20 18 19 nfan ⊢ Ⅎ 𝑣 ( ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝐵 ⊆ ∪ 𝐴 ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑣 ∈ 𝐴 𝑣 ⊆ ( 𝑓 ‘ 𝑣 ) ) ) ∧ 𝑥 ∈ ∪ 𝐴 )
21 simplrl ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝐵 ⊆ ∪ 𝐴 ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑣 ∈ 𝐴 𝑣 ⊆ ( 𝑓 ‘ 𝑣 ) ) ) ∧ 𝑣 ∈ 𝐴 ) → 𝑓 : 𝐴 ⟶ 𝐵 )
22 simpr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝐵 ⊆ ∪ 𝐴 ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑣 ∈ 𝐴 𝑣 ⊆ ( 𝑓 ‘ 𝑣 ) ) ) ∧ 𝑣 ∈ 𝐴 ) → 𝑣 ∈ 𝐴 )
23 21 22 ffvelrnd ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝐵 ⊆ ∪ 𝐴 ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑣 ∈ 𝐴 𝑣 ⊆ ( 𝑓 ‘ 𝑣 ) ) ) ∧ 𝑣 ∈ 𝐴 ) → ( 𝑓 ‘ 𝑣 ) ∈ 𝐵 )
24 23 adantlr ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝐵 ⊆ ∪ 𝐴 ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑣 ∈ 𝐴 𝑣 ⊆ ( 𝑓 ‘ 𝑣 ) ) ) ∧ 𝑥 ∈ ∪ 𝐴 ) ∧ 𝑣 ∈ 𝐴 ) → ( 𝑓 ‘ 𝑣 ) ∈ 𝐵 )
25 24 adantr ⊢ ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝐵 ⊆ ∪ 𝐴 ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑣 ∈ 𝐴 𝑣 ⊆ ( 𝑓 ‘ 𝑣 ) ) ) ∧ 𝑥 ∈ ∪ 𝐴 ) ∧ 𝑣 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝑣 ) → ( 𝑓 ‘ 𝑣 ) ∈ 𝐵 )
26 simplrr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝐵 ⊆ ∪ 𝐴 ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑣 ∈ 𝐴 𝑣 ⊆ ( 𝑓 ‘ 𝑣 ) ) ) ∧ 𝑣 ∈ 𝐴 ) → ∀ 𝑣 ∈ 𝐴 𝑣 ⊆ ( 𝑓 ‘ 𝑣 ) )
27 26 adantlr ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝐵 ⊆ ∪ 𝐴 ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑣 ∈ 𝐴 𝑣 ⊆ ( 𝑓 ‘ 𝑣 ) ) ) ∧ 𝑥 ∈ ∪ 𝐴 ) ∧ 𝑣 ∈ 𝐴 ) → ∀ 𝑣 ∈ 𝐴 𝑣 ⊆ ( 𝑓 ‘ 𝑣 ) )
28 simpr ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝐵 ⊆ ∪ 𝐴 ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑣 ∈ 𝐴 𝑣 ⊆ ( 𝑓 ‘ 𝑣 ) ) ) ∧ 𝑥 ∈ ∪ 𝐴 ) ∧ 𝑣 ∈ 𝐴 ) → 𝑣 ∈ 𝐴 )
29 rspa ⊢ ( ( ∀ 𝑣 ∈ 𝐴 𝑣 ⊆ ( 𝑓 ‘ 𝑣 ) ∧ 𝑣 ∈ 𝐴 ) → 𝑣 ⊆ ( 𝑓 ‘ 𝑣 ) )
30 27 28 29 syl2anc ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝐵 ⊆ ∪ 𝐴 ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑣 ∈ 𝐴 𝑣 ⊆ ( 𝑓 ‘ 𝑣 ) ) ) ∧ 𝑥 ∈ ∪ 𝐴 ) ∧ 𝑣 ∈ 𝐴 ) → 𝑣 ⊆ ( 𝑓 ‘ 𝑣 ) )
31 30 sselda ⊢ ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝐵 ⊆ ∪ 𝐴 ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑣 ∈ 𝐴 𝑣 ⊆ ( 𝑓 ‘ 𝑣 ) ) ) ∧ 𝑥 ∈ ∪ 𝐴 ) ∧ 𝑣 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝑣 ) → 𝑥 ∈ ( 𝑓 ‘ 𝑣 ) )
32 eleq2 ⊢ ( 𝑢 = ( 𝑓 ‘ 𝑣 ) → ( 𝑥 ∈ 𝑢 ↔ 𝑥 ∈ ( 𝑓 ‘ 𝑣 ) ) )
33 32 rspcev ⊢ ( ( ( 𝑓 ‘ 𝑣 ) ∈ 𝐵 ∧ 𝑥 ∈ ( 𝑓 ‘ 𝑣 ) ) → ∃ 𝑢 ∈ 𝐵 𝑥 ∈ 𝑢 )
34 25 31 33 syl2anc ⊢ ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝐵 ⊆ ∪ 𝐴 ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑣 ∈ 𝐴 𝑣 ⊆ ( 𝑓 ‘ 𝑣 ) ) ) ∧ 𝑥 ∈ ∪ 𝐴 ) ∧ 𝑣 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝑣 ) → ∃ 𝑢 ∈ 𝐵 𝑥 ∈ 𝑢 )
35 simpr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝐵 ⊆ ∪ 𝐴 ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑣 ∈ 𝐴 𝑣 ⊆ ( 𝑓 ‘ 𝑣 ) ) ) ∧ 𝑥 ∈ ∪ 𝐴 ) → 𝑥 ∈ ∪ 𝐴 )
36 eluni2 ⊢ ( 𝑥 ∈ ∪ 𝐴 ↔ ∃ 𝑣 ∈ 𝐴 𝑥 ∈ 𝑣 )
37 35 36 sylib ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝐵 ⊆ ∪ 𝐴 ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑣 ∈ 𝐴 𝑣 ⊆ ( 𝑓 ‘ 𝑣 ) ) ) ∧ 𝑥 ∈ ∪ 𝐴 ) → ∃ 𝑣 ∈ 𝐴 𝑥 ∈ 𝑣 )
38 20 34 37 r19.29af ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝐵 ⊆ ∪ 𝐴 ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑣 ∈ 𝐴 𝑣 ⊆ ( 𝑓 ‘ 𝑣 ) ) ) ∧ 𝑥 ∈ ∪ 𝐴 ) → ∃ 𝑢 ∈ 𝐵 𝑥 ∈ 𝑢 )
39 eluni2 ⊢ ( 𝑥 ∈ ∪ 𝐵 ↔ ∃ 𝑢 ∈ 𝐵 𝑥 ∈ 𝑢 )
40 38 39 sylibr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝐵 ⊆ ∪ 𝐴 ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑣 ∈ 𝐴 𝑣 ⊆ ( 𝑓 ‘ 𝑣 ) ) ) ∧ 𝑥 ∈ ∪ 𝐴 ) → 𝑥 ∈ ∪ 𝐵 )
41 13 40 eqelssd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝐵 ⊆ ∪ 𝐴 ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑣 ∈ 𝐴 𝑣 ⊆ ( 𝑓 ‘ 𝑣 ) ) ) → ∪ 𝐵 = ∪ 𝐴 )
42 26 22 29 syl2anc ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝐵 ⊆ ∪ 𝐴 ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑣 ∈ 𝐴 𝑣 ⊆ ( 𝑓 ‘ 𝑣 ) ) ) ∧ 𝑣 ∈ 𝐴 ) → 𝑣 ⊆ ( 𝑓 ‘ 𝑣 ) )
43 8 rspcev ⊢ ( ( ( 𝑓 ‘ 𝑣 ) ∈ 𝐵 ∧ 𝑣 ⊆ ( 𝑓 ‘ 𝑣 ) ) → ∃ 𝑢 ∈ 𝐵 𝑣 ⊆ 𝑢 )
44 23 42 43 syl2anc ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝐵 ⊆ ∪ 𝐴 ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑣 ∈ 𝐴 𝑣 ⊆ ( 𝑓 ‘ 𝑣 ) ) ) ∧ 𝑣 ∈ 𝐴 ) → ∃ 𝑢 ∈ 𝐵 𝑣 ⊆ 𝑢 )
45 44 ex ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝐵 ⊆ ∪ 𝐴 ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑣 ∈ 𝐴 𝑣 ⊆ ( 𝑓 ‘ 𝑣 ) ) ) → ( 𝑣 ∈ 𝐴 → ∃ 𝑢 ∈ 𝐵 𝑣 ⊆ 𝑢 ) )
46 18 45 ralrimi ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝐵 ⊆ ∪ 𝐴 ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑣 ∈ 𝐴 𝑣 ⊆ ( 𝑓 ‘ 𝑣 ) ) ) → ∀ 𝑣 ∈ 𝐴 ∃ 𝑢 ∈ 𝐵 𝑣 ⊆ 𝑢 )
47 4 ad2antrr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝐵 ⊆ ∪ 𝐴 ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑣 ∈ 𝐴 𝑣 ⊆ ( 𝑓 ‘ 𝑣 ) ) ) → ( 𝐴 Ref 𝐵 ↔ ( ∪ 𝐵 = ∪ 𝐴 ∧ ∀ 𝑣 ∈ 𝐴 ∃ 𝑢 ∈ 𝐵 𝑣 ⊆ 𝑢 ) ) )
48 41 46 47 mpbir2and ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝐵 ⊆ ∪ 𝐴 ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑣 ∈ 𝐴 𝑣 ⊆ ( 𝑓 ‘ 𝑣 ) ) ) → 𝐴 Ref 𝐵 )
49 48 ex ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝐵 ⊆ ∪ 𝐴 ) → ( ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑣 ∈ 𝐴 𝑣 ⊆ ( 𝑓 ‘ 𝑣 ) ) → 𝐴 Ref 𝐵 ) )
50 49 exlimdv ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝐵 ⊆ ∪ 𝐴 ) → ( ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑣 ∈ 𝐴 𝑣 ⊆ ( 𝑓 ‘ 𝑣 ) ) → 𝐴 Ref 𝐵 ) )
51 50 impr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( ∪ 𝐵 ⊆ ∪ 𝐴 ∧ ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑣 ∈ 𝐴 𝑣 ⊆ ( 𝑓 ‘ 𝑣 ) ) ) ) → 𝐴 Ref 𝐵 )
52 12 51 impbida ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 Ref 𝐵 ↔ ( ∪ 𝐵 ⊆ ∪ 𝐴 ∧ ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑣 ∈ 𝐴 𝑣 ⊆ ( 𝑓 ‘ 𝑣 ) ) ) ) )