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→BRefA↔∃cB⊆c∧AFnec∧cRefA

Proof

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