Metamath Proof Explorer

Theorem refssfne

Description: A cover is a refinement iff it is a subcover of something which is both finer and a refinement. (Contributed by Jeff Hankins, 18-Jan-2010) (Revised by Thierry Arnoux, 3-Feb-2020)

Ref Expression
Hypotheses refssfne.1 ⊢ X = ⋃ A
refssfne.2 ⊢ Y = ⋃ B
Assertion refssfne ⊢ X = Y → B Ref A ↔ ∃ c B ⊆ c ∧ A Fne c ∧ c Ref A

Proof

Step Hyp Ref Expression
1 refssfne.1 ⊢ X = ⋃ A
2 refssfne.2 ⊢ Y = ⋃ B
3 refrel ⊢ Rel ⁡ Ref
4 3 brrelex2i ⊢ B Ref A → A ∈ V
5 4 adantl ⊢ X = Y ∧ B Ref A → A ∈ V
6 3 brrelex1i ⊢ B Ref A → B ∈ V
7 6 adantl ⊢ X = Y ∧ B Ref A → B ∈ V
8 unexg ⊢ A ∈ V ∧ B ∈ V → A ∪ B ∈ V
9 5 7 8 syl2anc ⊢ X = Y ∧ B Ref A → A ∪ B ∈ V
10 ssun2 ⊢ B ⊆ A ∪ B
11 10 a1i ⊢ X = Y ∧ B Ref A → B ⊆ A ∪ B
12 ssun1 ⊢ A ⊆ A ∪ B
13 12 a1i ⊢ X = Y ∧ B Ref A → A ⊆ A ∪ B
14 eqimss2 ⊢ X = Y → Y ⊆ X
15 14 adantr ⊢ X = Y ∧ B Ref A → Y ⊆ X
16 ssequn2 ⊢ Y ⊆ X ↔ X ∪ Y = X
17 15 16 sylib ⊢ X = Y ∧ B Ref A → X ∪ Y = X
18 17 eqcomd ⊢ X = Y ∧ B Ref A → X = X ∪ Y
19 1 2 uneq12i ⊢ X ∪ Y = ⋃ A ∪ ⋃ B
20 uniun ⊢ ⋃ A ∪ B = ⋃ A ∪ ⋃ B
21 19 20 eqtr4i ⊢ X ∪ Y = ⋃ A ∪ B
22 1 21 fness ⊢ A ∪ B ∈ V ∧ A ⊆ A ∪ B ∧ X = X ∪ Y → A Fne A ∪ B
23 9 13 18 22 syl3anc ⊢ X = Y ∧ B Ref A → A Fne A ∪ B
24 elun ⊢ x ∈ A ∪ B ↔ x ∈ A ∨ x ∈ B
25 ssid ⊢ x ⊆ x
26 sseq2 ⊢ y = x → x ⊆ y ↔ x ⊆ x
27 26 rspcev ⊢ x ∈ A ∧ x ⊆ x → ∃ y ∈ A x ⊆ y
28 25 27 mpan2 ⊢ x ∈ A → ∃ y ∈ A x ⊆ y
29 28 a1i ⊢ X = Y ∧ B Ref A → x ∈ A → ∃ y ∈ A x ⊆ y
30 refssex ⊢ B Ref A ∧ x ∈ B → ∃ y ∈ A x ⊆ y
31 30 ex ⊢ B Ref A → x ∈ B → ∃ y ∈ A x ⊆ y
32 31 adantl ⊢ X = Y ∧ B Ref A → x ∈ B → ∃ y ∈ A x ⊆ y
33 29 32 jaod ⊢ X = Y ∧ B Ref A → x ∈ A ∨ x ∈ B → ∃ y ∈ A x ⊆ y
34 24 33 biimtrid ⊢ X = Y ∧ B Ref A → x ∈ A ∪ B → ∃ y ∈ A x ⊆ y
35 34 ralrimiv ⊢ X = Y ∧ B Ref A → ∀ x ∈ A ∪ B ∃ y ∈ A x ⊆ y
36 21 1 isref ⊢ A ∪ B ∈ V → A ∪ B Ref A ↔ X = X ∪ Y ∧ ∀ x ∈ A ∪ B ∃ y ∈ A x ⊆ y
37 9 36 syl ⊢ X = Y ∧ B Ref A → A ∪ B Ref A ↔ X = X ∪ Y ∧ ∀ x ∈ A ∪ B ∃ y ∈ A x ⊆ y
38 18 35 37 mpbir2and ⊢ X = Y ∧ B Ref A → A ∪ B Ref A
39 11 23 38 jca32 ⊢ X = Y ∧ B Ref A → B ⊆ A ∪ B ∧ A Fne A ∪ B ∧ A ∪ B Ref A
40 sseq2 ⊢ c = A ∪ B → B ⊆ c ↔ B ⊆ A ∪ B
41 breq2 ⊢ c = A ∪ B → A Fne c ↔ A Fne A ∪ B
42 breq1 ⊢ c = A ∪ B → c Ref A ↔ A ∪ B Ref A
43 41 42 anbi12d ⊢ c = A ∪ B → A Fne c ∧ c Ref A ↔ A Fne A ∪ B ∧ A ∪ B Ref A
44 40 43 anbi12d ⊢ c = A ∪ B → B ⊆ c ∧ A Fne c ∧ c Ref A ↔ B ⊆ A ∪ B ∧ A Fne A ∪ B ∧ A ∪ B Ref A
45 44 spcegv ⊢ A ∪ B ∈ V → B ⊆ A ∪ B ∧ A Fne A ∪ B ∧ A ∪ B Ref A → ∃ c B ⊆ c ∧ A Fne c ∧ c Ref A
46 9 39 45 sylc ⊢ X = Y ∧ B Ref A → ∃ c B ⊆ c ∧ A Fne c ∧ c Ref A
47 46 ex ⊢ X = Y → B Ref A → ∃ c B ⊆ c ∧ A Fne c ∧ c Ref A
48 vex ⊢ c ∈ V
49 48 ssex ⊢ B ⊆ c → B ∈ V
50 49 ad2antrl ⊢ X = Y ∧ B ⊆ c ∧ A Fne c ∧ c Ref A → B ∈ V
51 simprl ⊢ X = Y ∧ B ⊆ c ∧ A Fne c ∧ c Ref A → B ⊆ c
52 simpl ⊢ X = Y ∧ B ⊆ c ∧ A Fne c ∧ c Ref A → X = Y
53 eqid ⊢ ⋃ c = ⋃ c
54 53 1 refbas ⊢ c Ref A → X = ⋃ c
55 54 adantl ⊢ A Fne c ∧ c Ref A → X = ⋃ c
56 55 ad2antll ⊢ X = Y ∧ B ⊆ c ∧ A Fne c ∧ c Ref A → X = ⋃ c
57 52 56 eqtr3d ⊢ X = Y ∧ B ⊆ c ∧ A Fne c ∧ c Ref A → Y = ⋃ c
58 2 53 ssref ⊢ B ∈ V ∧ B ⊆ c ∧ Y = ⋃ c → B Ref c
59 50 51 57 58 syl3anc ⊢ X = Y ∧ B ⊆ c ∧ A Fne c ∧ c Ref A → B Ref c
60 simprrr ⊢ X = Y ∧ B ⊆ c ∧ A Fne c ∧ c Ref A → c Ref A
61 reftr ⊢ B Ref c ∧ c Ref A → B Ref A
62 59 60 61 syl2anc ⊢ X = Y ∧ B ⊆ c ∧ A Fne c ∧ c Ref A → B Ref A
63 62 ex ⊢ X = Y → B ⊆ c ∧ A Fne c ∧ c Ref A → B Ref A
64 63 exlimdv ⊢ X = Y → ∃ c B ⊆ c ∧ A Fne c ∧ c Ref A → B Ref A
65 47 64 impbid ⊢ X = Y → B Ref A ↔ ∃ c B ⊆ c ∧ A Fne c ∧ c Ref A