This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = U. A
fnessref.2 
|- Y = U. B
Assertion fnessref 
|- ( X = Y -> ( A Fne B <-> E. c ( c C_ B /\ ( A Fne c /\ c Ref A ) ) ) )

Proof

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