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 A Fne B c c B A Fne c c Ref A

Proof

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