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

Proof

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