Metamath Proof Explorer

Theorem fnetr

Description: Transitivity of the fineness relation. (Contributed by Jeff Hankins, 5-Oct-2009) (Proof shortened by Mario Carneiro, 11-Sep-2015)

Ref Expression
Assertion fnetr 
|- ( ( A Fne B /\ B Fne C ) -> A Fne C )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  U. A = U. A
2 eqid 
 |-  U. B = U. B
3 1 2 fnebas 
 |-  ( A Fne B -> U. A = U. B )
4 eqid 
 |-  U. C = U. C
5 2 4 fnebas 
 |-  ( B Fne C -> U. B = U. C )
6 3 5 sylan9eq 
 |-  ( ( A Fne B /\ B Fne C ) -> U. A = U. C )
7 fnerel 
 |-  Rel Fne
8 7 brrelex2i 
 |-  ( A Fne B -> B e. _V )
9 1 2 isfne4b 
 |-  ( B e. _V -> ( A Fne B <-> ( U. A = U. B /\ ( topGen ` A ) C_ ( topGen ` B ) ) ) )
10 9 simplbda 
 |-  ( ( B e. _V /\ A Fne B ) -> ( topGen ` A ) C_ ( topGen ` B ) )
11 8 10 mpancom 
 |-  ( A Fne B -> ( topGen ` A ) C_ ( topGen ` B ) )
12 7 brrelex2i 
 |-  ( B Fne C -> C e. _V )
13 2 4 isfne4b 
 |-  ( C e. _V -> ( B Fne C <-> ( U. B = U. C /\ ( topGen ` B ) C_ ( topGen ` C ) ) ) )
14 13 simplbda 
 |-  ( ( C e. _V /\ B Fne C ) -> ( topGen ` B ) C_ ( topGen ` C ) )
15 12 14 mpancom 
 |-  ( B Fne C -> ( topGen ` B ) C_ ( topGen ` C ) )
16 11 15 sylan9ss 
 |-  ( ( A Fne B /\ B Fne C ) -> ( topGen ` A ) C_ ( topGen ` C ) )
17 12 adantl 
 |-  ( ( A Fne B /\ B Fne C ) -> C e. _V )
18 1 4 isfne4b 
 |-  ( C e. _V -> ( A Fne C <-> ( U. A = U. C /\ ( topGen ` A ) C_ ( topGen ` C ) ) ) )
19 17 18 syl 
 |-  ( ( A Fne B /\ B Fne C ) -> ( A Fne C <-> ( U. A = U. C /\ ( topGen ` A ) C_ ( topGen ` C ) ) ) )
20 6 16 19 mpbir2and 
 |-  ( ( A Fne B /\ B Fne C ) -> A Fne C )