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

Proof

Step Hyp Ref Expression
1 refssfne.1 
 |-  X = U. A
2 refssfne.2 
 |-  Y = U. B
3 refrel 
 |-  Rel Ref
4 3 brrelex2i 
 |-  ( B Ref A -> A e. _V )
5 4 adantl 
 |-  ( ( X = Y /\ B Ref A ) -> A e. _V )
6 3 brrelex1i 
 |-  ( B Ref A -> B e. _V )
7 6 adantl 
 |-  ( ( X = Y /\ B Ref A ) -> B e. _V )
8 unexg 
 |-  ( ( A e. _V /\ B e. _V ) -> ( A u. B ) e. _V )
9 5 7 8 syl2anc 
 |-  ( ( X = Y /\ B Ref A ) -> ( A u. B ) e. _V )
10 ssun2 
 |-  B C_ ( A u. B )
11 10 a1i 
 |-  ( ( X = Y /\ B Ref A ) -> B C_ ( A u. B ) )
12 ssun1 
 |-  A C_ ( A u. B )
13 12 a1i 
 |-  ( ( X = Y /\ B Ref A ) -> A C_ ( A u. B ) )
14 eqimss2 
 |-  ( X = Y -> Y C_ X )
15 14 adantr 
 |-  ( ( X = Y /\ B Ref A ) -> Y C_ X )
16 ssequn2 
 |-  ( Y C_ X <-> ( X u. Y ) = X )
17 15 16 sylib 
 |-  ( ( X = Y /\ B Ref A ) -> ( X u. Y ) = X )
18 17 eqcomd 
 |-  ( ( X = Y /\ B Ref A ) -> X = ( X u. Y ) )
19 1 2 uneq12i 
 |-  ( X u. Y ) = ( U. A u. U. B )
20 uniun 
 |-  U. ( A u. B ) = ( U. A u. U. B )
21 19 20 eqtr4i 
 |-  ( X u. Y ) = U. ( A u. B )
22 1 21 fness 
 |-  ( ( ( A u. B ) e. _V /\ A C_ ( A u. B ) /\ X = ( X u. Y ) ) -> A Fne ( A u. B ) )
23 9 13 18 22 syl3anc 
 |-  ( ( X = Y /\ B Ref A ) -> A Fne ( A u. B ) )
24 elun 
 |-  ( x e. ( A u. B ) <-> ( x e. A \/ x e. B ) )
25 ssid 
 |-  x C_ x
26 sseq2 
 |-  ( y = x -> ( x C_ y <-> x C_ x ) )
27 26 rspcev 
 |-  ( ( x e. A /\ x C_ x ) -> E. y e. A x C_ y )
28 25 27 mpan2 
 |-  ( x e. A -> E. y e. A x C_ y )
29 28 a1i 
 |-  ( ( X = Y /\ B Ref A ) -> ( x e. A -> E. y e. A x C_ y ) )
30 refssex 
 |-  ( ( B Ref A /\ x e. B ) -> E. y e. A x C_ y )
31 30 ex 
 |-  ( B Ref A -> ( x e. B -> E. y e. A x C_ y ) )
32 31 adantl 
 |-  ( ( X = Y /\ B Ref A ) -> ( x e. B -> E. y e. A x C_ y ) )
33 29 32 jaod 
 |-  ( ( X = Y /\ B Ref A ) -> ( ( x e. A \/ x e. B ) -> E. y e. A x C_ y ) )
34 24 33 syl5bi 
 |-  ( ( X = Y /\ B Ref A ) -> ( x e. ( A u. B ) -> E. y e. A x C_ y ) )
35 34 ralrimiv 
 |-  ( ( X = Y /\ B Ref A ) -> A. x e. ( A u. B ) E. y e. A x C_ y )
36 21 1 isref 
 |-  ( ( A u. B ) e. _V -> ( ( A u. B ) Ref A <-> ( X = ( X u. Y ) /\ A. x e. ( A u. B ) E. y e. A x C_ y ) ) )
37 9 36 syl 
 |-  ( ( X = Y /\ B Ref A ) -> ( ( A u. B ) Ref A <-> ( X = ( X u. Y ) /\ A. x e. ( A u. B ) E. y e. A x C_ y ) ) )
38 18 35 37 mpbir2and 
 |-  ( ( X = Y /\ B Ref A ) -> ( A u. B ) Ref A )
39 11 23 38 jca32 
 |-  ( ( X = Y /\ B Ref A ) -> ( B C_ ( A u. B ) /\ ( A Fne ( A u. B ) /\ ( A u. B ) Ref A ) ) )
40 sseq2 
 |-  ( c = ( A u. B ) -> ( B C_ c <-> B C_ ( A u. B ) ) )
41 breq2 
 |-  ( c = ( A u. B ) -> ( A Fne c <-> A Fne ( A u. B ) ) )
42 breq1 
 |-  ( c = ( A u. B ) -> ( c Ref A <-> ( A u. B ) Ref A ) )
43 41 42 anbi12d 
 |-  ( c = ( A u. B ) -> ( ( A Fne c /\ c Ref A ) <-> ( A Fne ( A u. B ) /\ ( A u. B ) Ref A ) ) )
44 40 43 anbi12d 
 |-  ( c = ( A u. B ) -> ( ( B C_ c /\ ( A Fne c /\ c Ref A ) ) <-> ( B C_ ( A u. B ) /\ ( A Fne ( A u. B ) /\ ( A u. B ) Ref A ) ) ) )
45 44 spcegv 
 |-  ( ( A u. B ) e. _V -> ( ( B C_ ( A u. B ) /\ ( A Fne ( A u. B ) /\ ( A u. B ) Ref A ) ) -> E. c ( B C_ c /\ ( A Fne c /\ c Ref A ) ) ) )
46 9 39 45 sylc 
 |-  ( ( X = Y /\ B Ref A ) -> E. c ( B C_ c /\ ( A Fne c /\ c Ref A ) ) )
47 46 ex 
 |-  ( X = Y -> ( B Ref A -> E. c ( B C_ c /\ ( A Fne c /\ c Ref A ) ) ) )
48 vex 
 |-  c e. _V
49 48 ssex 
 |-  ( B C_ c -> B e. _V )
50 49 ad2antrl 
 |-  ( ( X = Y /\ ( B C_ c /\ ( A Fne c /\ c Ref A ) ) ) -> B e. _V )
51 simprl 
 |-  ( ( X = Y /\ ( B C_ c /\ ( A Fne c /\ c Ref A ) ) ) -> B C_ c )
52 simpl 
 |-  ( ( X = Y /\ ( B C_ c /\ ( A Fne c /\ c Ref A ) ) ) -> X = Y )
53 eqid 
 |-  U. c = U. c
54 53 1 refbas 
 |-  ( c Ref A -> X = U. c )
55 54 adantl 
 |-  ( ( A Fne c /\ c Ref A ) -> X = U. c )
56 55 ad2antll 
 |-  ( ( X = Y /\ ( B C_ c /\ ( A Fne c /\ c Ref A ) ) ) -> X = U. c )
57 52 56 eqtr3d 
 |-  ( ( X = Y /\ ( B C_ c /\ ( A Fne c /\ c Ref A ) ) ) -> Y = U. c )
58 2 53 ssref 
 |-  ( ( B e. _V /\ B C_ c /\ Y = U. c ) -> B Ref c )
59 50 51 57 58 syl3anc 
 |-  ( ( X = Y /\ ( B C_ c /\ ( A Fne c /\ c Ref A ) ) ) -> B Ref c )
60 simprrr 
 |-  ( ( X = Y /\ ( B C_ 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_ c /\ ( A Fne c /\ c Ref A ) ) ) -> B Ref A )
63 62 ex 
 |-  ( X = Y -> ( ( B C_ c /\ ( A Fne c /\ c Ref A ) ) -> B Ref A ) )
64 63 exlimdv 
 |-  ( X = Y -> ( E. c ( B C_ c /\ ( A Fne c /\ c Ref A ) ) -> B Ref A ) )
65 47 64 impbid 
 |-  ( X = Y -> ( B Ref A <-> E. c ( B C_ c /\ ( A Fne c /\ c Ref A ) ) ) )