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

Metamath Proof Explorer

Theorem isfne

Description: The predicate " B is finer than A ". This property is, in a sense, the opposite of refinement, as refinement requires every element to be a subset of an element of the original and fineness requires that every element of the original have a subset in the finer cover containing every point. I do not know of a literature reference for this. (Contributed by Jeff Hankins, 28-Sep-2009)

Ref Expression
Hypotheses isfne.1 
|- X = U. A
isfne.2 
|- Y = U. B
Assertion isfne 
|- ( B e. C -> ( A Fne B <-> ( X = Y /\ A. x e. A x C_ U. ( B i^i ~P x ) ) ) )

Proof

Step Hyp Ref Expression
1 isfne.1 
 |-  X = U. A
2 isfne.2 
 |-  Y = U. B
3 fnerel 
 |-  Rel Fne
4 3 brrelex1i 
 |-  ( A Fne B -> A e. _V )
5 4 anim1i 
 |-  ( ( A Fne B /\ B e. C ) -> ( A e. _V /\ B e. C ) )
6 5 ancoms 
 |-  ( ( B e. C /\ A Fne B ) -> ( A e. _V /\ B e. C ) )
7 simpr 
 |-  ( ( B e. C /\ X = Y ) -> X = Y )
8 7 1 2 3eqtr3g 
 |-  ( ( B e. C /\ X = Y ) -> U. A = U. B )
9 simpr 
 |-  ( ( B e. C /\ U. A = U. B ) -> U. A = U. B )
10 uniexg 
 |-  ( B e. C -> U. B e. _V )
11 10 adantr 
 |-  ( ( B e. C /\ U. A = U. B ) -> U. B e. _V )
12 9 11 eqeltrd 
 |-  ( ( B e. C /\ U. A = U. B ) -> U. A e. _V )
13 uniexb 
 |-  ( A e. _V <-> U. A e. _V )
14 12 13 sylibr 
 |-  ( ( B e. C /\ U. A = U. B ) -> A e. _V )
15 simpl 
 |-  ( ( B e. C /\ U. A = U. B ) -> B e. C )
16 14 15 jca 
 |-  ( ( B e. C /\ U. A = U. B ) -> ( A e. _V /\ B e. C ) )
17 8 16 syldan 
 |-  ( ( B e. C /\ X = Y ) -> ( A e. _V /\ B e. C ) )
18 17 adantrr 
 |-  ( ( B e. C /\ ( X = Y /\ A. x e. A x C_ U. ( B i^i ~P x ) ) ) -> ( A e. _V /\ B e. C ) )
19 unieq 
 |-  ( r = A -> U. r = U. A )
20 19 1 eqtr4di 
 |-  ( r = A -> U. r = X )
21 20 eqeq1d 
 |-  ( r = A -> ( U. r = U. s <-> X = U. s ) )
22 raleq 
 |-  ( r = A -> ( A. x e. r x C_ U. ( s i^i ~P x ) <-> A. x e. A x C_ U. ( s i^i ~P x ) ) )
23 21 22 anbi12d 
 |-  ( r = A -> ( ( U. r = U. s /\ A. x e. r x C_ U. ( s i^i ~P x ) ) <-> ( X = U. s /\ A. x e. A x C_ U. ( s i^i ~P x ) ) ) )
24 unieq 
 |-  ( s = B -> U. s = U. B )
25 24 2 eqtr4di 
 |-  ( s = B -> U. s = Y )
26 25 eqeq2d 
 |-  ( s = B -> ( X = U. s <-> X = Y ) )
27 ineq1 
 |-  ( s = B -> ( s i^i ~P x ) = ( B i^i ~P x ) )
28 27 unieqd 
 |-  ( s = B -> U. ( s i^i ~P x ) = U. ( B i^i ~P x ) )
29 28 sseq2d 
 |-  ( s = B -> ( x C_ U. ( s i^i ~P x ) <-> x C_ U. ( B i^i ~P x ) ) )
30 29 ralbidv 
 |-  ( s = B -> ( A. x e. A x C_ U. ( s i^i ~P x ) <-> A. x e. A x C_ U. ( B i^i ~P x ) ) )
31 26 30 anbi12d 
 |-  ( s = B -> ( ( X = U. s /\ A. x e. A x C_ U. ( s i^i ~P x ) ) <-> ( X = Y /\ A. x e. A x C_ U. ( B i^i ~P x ) ) ) )
32 df-fne 
 |-  Fne = { <. r , s >. | ( U. r = U. s /\ A. x e. r x C_ U. ( s i^i ~P x ) ) }
33 23 31 32 brabg 
 |-  ( ( A e. _V /\ B e. C ) -> ( A Fne B <-> ( X = Y /\ A. x e. A x C_ U. ( B i^i ~P x ) ) ) )
34 6 18 33 pm5.21nd 
 |-  ( B e. C -> ( A Fne B <-> ( X = Y /\ A. x e. A x C_ U. ( B i^i ~P x ) ) ) )