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 ⊢ ⋃ A = ⋃ A
2 eqid ⊢ ⋃ B = ⋃ B
3 1 2 fnebas ⊢ A Fne B → ⋃ A = ⋃ B
4 eqid ⊢ ⋃ C = ⋃ C
5 2 4 fnebas ⊢ B Fne C → ⋃ B = ⋃ C
6 3 5 sylan9eq ⊢ A Fne B ∧ B Fne C → ⋃ A = ⋃ C
7 fnerel ⊢ Rel ⁡ Fne
8 7 brrelex2i ⊢ A Fne B → B ∈ V
9 1 2 isfne4b ⊢ B ∈ V → A Fne B ↔ ⋃ A = ⋃ B ∧ topGen ⁡ A ⊆ topGen ⁡ B
10 9 simplbda ⊢ B ∈ V ∧ A Fne B → topGen ⁡ A ⊆ topGen ⁡ B
11 8 10 mpancom ⊢ A Fne B → topGen ⁡ A ⊆ topGen ⁡ B
12 7 brrelex2i ⊢ B Fne C → C ∈ V
13 2 4 isfne4b ⊢ C ∈ V → B Fne C ↔ ⋃ B = ⋃ C ∧ topGen ⁡ B ⊆ topGen ⁡ C
14 13 simplbda ⊢ C ∈ V ∧ B Fne C → topGen ⁡ B ⊆ topGen ⁡ C
15 12 14 mpancom ⊢ B Fne C → topGen ⁡ B ⊆ topGen ⁡ C
16 11 15 sylan9ss ⊢ A Fne B ∧ B Fne C → topGen ⁡ A ⊆ topGen ⁡ C
17 12 adantl ⊢ A Fne B ∧ B Fne C → C ∈ V
18 1 4 isfne4b ⊢ C ∈ V → A Fne C ↔ ⋃ A = ⋃ C ∧ topGen ⁡ A ⊆ topGen ⁡ C
19 17 18 syl ⊢ A Fne B ∧ B Fne C → A Fne C ↔ ⋃ A = ⋃ C ∧ topGen ⁡ A ⊆ topGen ⁡ C
20 6 16 19 mpbir2and ⊢ A Fne B ∧ B Fne C → A Fne C