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 ⊢AFneB∧BFneC→AFneC

Proof

Step Hyp Ref Expression
1 eqid ⊢⋃A=⋃A
2 eqid ⊢⋃B=⋃B
3 1 2 fnebas ⊢AFneB→⋃A=⋃B
4 eqid ⊢⋃C=⋃C
5 2 4 fnebas ⊢BFneC→⋃B=⋃C
6 3 5 sylan9eq ⊢AFneB∧BFneC→⋃A=⋃C
7 fnerel ⊢Rel⁡Fne
8 7 brrelex2i ⊢AFneB→B∈V
9 1 2 isfne4b ⊢B∈V→AFneB↔⋃A=⋃B∧topGen⁡A⊆topGen⁡B
10 9 simplbda ⊢B∈V∧AFneB→topGen⁡A⊆topGen⁡B
11 8 10 mpancom ⊢AFneB→topGen⁡A⊆topGen⁡B
12 7 brrelex2i ⊢BFneC→C∈V
13 2 4 isfne4b ⊢C∈V→BFneC↔⋃B=⋃C∧topGen⁡B⊆topGen⁡C
14 13 simplbda ⊢C∈V∧BFneC→topGen⁡B⊆topGen⁡C
15 12 14 mpancom ⊢BFneC→topGen⁡B⊆topGen⁡C
16 11 15 sylan9ss ⊢AFneB∧BFneC→topGen⁡A⊆topGen⁡C
17 12 adantl ⊢AFneB∧BFneC→C∈V
18 1 4 isfne4b ⊢C∈V→AFneC↔⋃A=⋃C∧topGen⁡A⊆topGen⁡C
19 17 18 syl ⊢AFneB∧BFneC→AFneC↔⋃A=⋃C∧topGen⁡A⊆topGen⁡C
20 6 16 19 mpbir2and ⊢AFneB∧BFneC→AFneC