Metamath Proof Explorer

Theorem fnessref

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

Ref Expression
Hypotheses fnessref.1 ⊢X=⋃A
fnessref.2 ⊢Y=⋃B
Assertion fnessref ⊢X=Y→AFneB↔∃cc⊆B∧AFnec∧cRefA

Proof

Step Hyp Ref Expression
1 fnessref.1 ⊢X=⋃A
2 fnessref.2 ⊢Y=⋃B
3 fnerel ⊢Rel⁡Fne
4 3 brrelex2i ⊢AFneB→B∈V
5 4 adantl ⊢X=Y∧AFneB→B∈V
6 rabexg ⊢B∈V→x∈B|∃y∈Ax⊆y∈V
7 5 6 syl ⊢X=Y∧AFneB→x∈B|∃y∈Ax⊆y∈V
8 ssrab2 ⊢x∈B|∃y∈Ax⊆y⊆B
9 8 a1i ⊢X=Y∧AFneB→x∈B|∃y∈Ax⊆y⊆B
10 1 eleq2i ⊢t∈X↔t∈⋃A
11 eluni ⊢t∈⋃A↔∃zt∈z∧z∈A
12 10 11 bitri ⊢t∈X↔∃zt∈z∧z∈A
13 fnessex ⊢AFneB∧z∈A∧t∈z→∃x∈Bt∈x∧x⊆z
14 13 3expia ⊢AFneB∧z∈A→t∈z→∃x∈Bt∈x∧x⊆z
15 14 adantll ⊢X=Y∧AFneB∧z∈A→t∈z→∃x∈Bt∈x∧x⊆z
16 sseq2 ⊢y=z→x⊆y↔x⊆z
17 16 rspcev ⊢z∈A∧x⊆z→∃y∈Ax⊆y
18 17 ex ⊢z∈A→x⊆z→∃y∈Ax⊆y
19 18 adantl ⊢X=Y∧AFneB∧z∈A→x⊆z→∃y∈Ax⊆y
20 19 anim2d ⊢X=Y∧AFneB∧z∈A→t∈x∧x⊆z→t∈x∧∃y∈Ax⊆y
21 20 reximdv ⊢X=Y∧AFneB∧z∈A→∃x∈Bt∈x∧x⊆z→∃x∈Bt∈x∧∃y∈Ax⊆y
22 15 21 syld ⊢X=Y∧AFneB∧z∈A→t∈z→∃x∈Bt∈x∧∃y∈Ax⊆y
23 22 ex ⊢X=Y∧AFneB→z∈A→t∈z→∃x∈Bt∈x∧∃y∈Ax⊆y
24 23 com23 ⊢X=Y∧AFneB→t∈z→z∈A→∃x∈Bt∈x∧∃y∈Ax⊆y
25 24 impd ⊢X=Y∧AFneB→t∈z∧z∈A→∃x∈Bt∈x∧∃y∈Ax⊆y
26 25 exlimdv ⊢X=Y∧AFneB→∃zt∈z∧z∈A→∃x∈Bt∈x∧∃y∈Ax⊆y
27 12 26 biimtrid ⊢X=Y∧AFneB→t∈X→∃x∈Bt∈x∧∃y∈Ax⊆y
28 elunirab ⊢t∈⋃x∈B|∃y∈Ax⊆y↔∃x∈Bt∈x∧∃y∈Ax⊆y
29 27 28 syl6ibr ⊢X=Y∧AFneB→t∈X→t∈⋃x∈B|∃y∈Ax⊆y
30 29 ssrdv ⊢X=Y∧AFneB→X⊆⋃x∈B|∃y∈Ax⊆y
31 8 unissi ⊢⋃x∈B|∃y∈Ax⊆y⊆⋃B
32 simpl ⊢X=Y∧AFneB→X=Y
33 32 2 eqtr2di ⊢X=Y∧AFneB→⋃B=X
34 31 33 sseqtrid ⊢X=Y∧AFneB→⋃x∈B|∃y∈Ax⊆y⊆X
35 30 34 eqssd ⊢X=Y∧AFneB→X=⋃x∈B|∃y∈Ax⊆y
36 fnessex ⊢AFneB∧z∈A∧t∈z→∃w∈Bt∈w∧w⊆z
37 36 3expb ⊢AFneB∧z∈A∧t∈z→∃w∈Bt∈w∧w⊆z
38 37 adantll ⊢X=Y∧AFneB∧z∈A∧t∈z→∃w∈Bt∈w∧w⊆z
39 simpl ⊢w∈B∧t∈w∧w⊆z→w∈B
40 39 a1i ⊢X=Y∧AFneB∧z∈A∧t∈z→w∈B∧t∈w∧w⊆z→w∈B
41 sseq2 ⊢y=z→w⊆y↔w⊆z
42 41 rspcev ⊢z∈A∧w⊆z→∃y∈Aw⊆y
43 42 expcom ⊢w⊆z→z∈A→∃y∈Aw⊆y
44 43 ad2antll ⊢w∈B∧t∈w∧w⊆z→z∈A→∃y∈Aw⊆y
45 44 com12 ⊢z∈A→w∈B∧t∈w∧w⊆z→∃y∈Aw⊆y
46 45 ad2antrl ⊢X=Y∧AFneB∧z∈A∧t∈z→w∈B∧t∈w∧w⊆z→∃y∈Aw⊆y
47 40 46 jcad ⊢X=Y∧AFneB∧z∈A∧t∈z→w∈B∧t∈w∧w⊆z→w∈B∧∃y∈Aw⊆y
48 sseq1 ⊢x=w→x⊆y↔w⊆y
49 48 rexbidv ⊢x=w→∃y∈Ax⊆y↔∃y∈Aw⊆y
50 49 elrab ⊢w∈x∈B|∃y∈Ax⊆y↔w∈B∧∃y∈Aw⊆y
51 47 50 syl6ibr ⊢X=Y∧AFneB∧z∈A∧t∈z→w∈B∧t∈w∧w⊆z→w∈x∈B|∃y∈Ax⊆y
52 simpr ⊢w∈B∧t∈w∧w⊆z→t∈w∧w⊆z
53 52 a1i ⊢X=Y∧AFneB∧z∈A∧t∈z→w∈B∧t∈w∧w⊆z→t∈w∧w⊆z
54 51 53 jcad ⊢X=Y∧AFneB∧z∈A∧t∈z→w∈B∧t∈w∧w⊆z→w∈x∈B|∃y∈Ax⊆y∧t∈w∧w⊆z
55 54 reximdv2 ⊢X=Y∧AFneB∧z∈A∧t∈z→∃w∈Bt∈w∧w⊆z→∃w∈x∈B|∃y∈Ax⊆yt∈w∧w⊆z
56 38 55 mpd ⊢X=Y∧AFneB∧z∈A∧t∈z→∃w∈x∈B|∃y∈Ax⊆yt∈w∧w⊆z
57 56 ralrimivva ⊢X=Y∧AFneB→∀z∈A∀t∈z∃w∈x∈B|∃y∈Ax⊆yt∈w∧w⊆z
58 eqid ⊢⋃x∈B|∃y∈Ax⊆y=⋃x∈B|∃y∈Ax⊆y
59 1 58 isfne2 ⊢x∈B|∃y∈Ax⊆y∈V→AFnex∈B|∃y∈Ax⊆y↔X=⋃x∈B|∃y∈Ax⊆y∧∀z∈A∀t∈z∃w∈x∈B|∃y∈Ax⊆yt∈w∧w⊆z
60 5 6 59 3syl ⊢X=Y∧AFneB→AFnex∈B|∃y∈Ax⊆y↔X=⋃x∈B|∃y∈Ax⊆y∧∀z∈A∀t∈z∃w∈x∈B|∃y∈Ax⊆yt∈w∧w⊆z
61 35 57 60 mpbir2and ⊢X=Y∧AFneB→AFnex∈B|∃y∈Ax⊆y
62 sseq1 ⊢x=z→x⊆y↔z⊆y
63 62 rexbidv ⊢x=z→∃y∈Ax⊆y↔∃y∈Az⊆y
64 63 elrab ⊢z∈x∈B|∃y∈Ax⊆y↔z∈B∧∃y∈Az⊆y
65 sseq2 ⊢y=w→z⊆y↔z⊆w
66 65 cbvrexvw ⊢∃y∈Az⊆y↔∃w∈Az⊆w
67 66 biimpi ⊢∃y∈Az⊆y→∃w∈Az⊆w
68 67 adantl ⊢z∈B∧∃y∈Az⊆y→∃w∈Az⊆w
69 68 a1i ⊢X=Y∧AFneB→z∈B∧∃y∈Az⊆y→∃w∈Az⊆w
70 64 69 biimtrid ⊢X=Y∧AFneB→z∈x∈B|∃y∈Ax⊆y→∃w∈Az⊆w
71 70 ralrimiv ⊢X=Y∧AFneB→∀z∈x∈B|∃y∈Ax⊆y∃w∈Az⊆w
72 58 1 isref ⊢x∈B|∃y∈Ax⊆y∈V→x∈B|∃y∈Ax⊆yRefA↔X=⋃x∈B|∃y∈Ax⊆y∧∀z∈x∈B|∃y∈Ax⊆y∃w∈Az⊆w
73 5 6 72 3syl ⊢X=Y∧AFneB→x∈B|∃y∈Ax⊆yRefA↔X=⋃x∈B|∃y∈Ax⊆y∧∀z∈x∈B|∃y∈Ax⊆y∃w∈Az⊆w
74 35 71 73 mpbir2and ⊢X=Y∧AFneB→x∈B|∃y∈Ax⊆yRefA
75 9 61 74 jca32 ⊢X=Y∧AFneB→x∈B|∃y∈Ax⊆y⊆B∧AFnex∈B|∃y∈Ax⊆y∧x∈B|∃y∈Ax⊆yRefA
76 sseq1 ⊢c=x∈B|∃y∈Ax⊆y→c⊆B↔x∈B|∃y∈Ax⊆y⊆B
77 breq2 ⊢c=x∈B|∃y∈Ax⊆y→AFnec↔AFnex∈B|∃y∈Ax⊆y
78 breq1 ⊢c=x∈B|∃y∈Ax⊆y→cRefA↔x∈B|∃y∈Ax⊆yRefA
79 77 78 anbi12d ⊢c=x∈B|∃y∈Ax⊆y→AFnec∧cRefA↔AFnex∈B|∃y∈Ax⊆y∧x∈B|∃y∈Ax⊆yRefA
80 76 79 anbi12d ⊢c=x∈B|∃y∈Ax⊆y→c⊆B∧AFnec∧cRefA↔x∈B|∃y∈Ax⊆y⊆B∧AFnex∈B|∃y∈Ax⊆y∧x∈B|∃y∈Ax⊆yRefA
81 80 spcegv ⊢x∈B|∃y∈Ax⊆y∈V→x∈B|∃y∈Ax⊆y⊆B∧AFnex∈B|∃y∈Ax⊆y∧x∈B|∃y∈Ax⊆yRefA→∃cc⊆B∧AFnec∧cRefA
82 7 75 81 sylc ⊢X=Y∧AFneB→∃cc⊆B∧AFnec∧cRefA
83 82 ex ⊢X=Y→AFneB→∃cc⊆B∧AFnec∧cRefA
84 simprrl ⊢X=Y∧c⊆B∧AFnec∧cRefA→AFnec
85 eqid ⊢⋃c=⋃c
86 1 85 fnebas ⊢AFnec→X=⋃c
87 84 86 syl ⊢X=Y∧c⊆B∧AFnec∧cRefA→X=⋃c
88 simpl ⊢X=Y∧c⊆B∧AFnec∧cRefA→X=Y
89 87 88 eqtr3d ⊢X=Y∧c⊆B∧AFnec∧cRefA→⋃c=Y
90 89 2 eqtrdi ⊢X=Y∧c⊆B∧AFnec∧cRefA→⋃c=⋃B
91 vuniex ⊢⋃c∈V
92 90 91 eqeltrrdi ⊢X=Y∧c⊆B∧AFnec∧cRefA→⋃B∈V
93 uniexb ⊢B∈V↔⋃B∈V
94 92 93 sylibr ⊢X=Y∧c⊆B∧AFnec∧cRefA→B∈V
95 simprl ⊢X=Y∧c⊆B∧AFnec∧cRefA→c⊆B
96 85 2 fness ⊢B∈V∧c⊆B∧⋃c=Y→cFneB
97 94 95 89 96 syl3anc ⊢X=Y∧c⊆B∧AFnec∧cRefA→cFneB
98 fnetr ⊢AFnec∧cFneB→AFneB
99 84 97 98 syl2anc ⊢X=Y∧c⊆B∧AFnec∧cRefA→AFneB
100 99 ex ⊢X=Y→c⊆B∧AFnec∧cRefA→AFneB
101 100 exlimdv ⊢X=Y→∃cc⊆B∧AFnec∧cRefA→AFneB
102 83 101 impbid ⊢X=Y→AFneB↔∃cc⊆B∧AFnec∧cRefA