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 ( ( 𝐴 Fne 𝐵 ∧ 𝐵 Fne 𝐶 ) → 𝐴 Fne 𝐶 )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ∪ 𝐴 = ∪ 𝐴
2 eqid ⊢ ∪ 𝐵 = ∪ 𝐵
3 1 2 fnebas ⊢ ( 𝐴 Fne 𝐵 → ∪ 𝐴 = ∪ 𝐵 )
4 eqid ⊢ ∪ 𝐶 = ∪ 𝐶
5 2 4 fnebas ⊢ ( 𝐵 Fne 𝐶 → ∪ 𝐵 = ∪ 𝐶 )
6 3 5 sylan9eq ⊢ ( ( 𝐴 Fne 𝐵 ∧ 𝐵 Fne 𝐶 ) → ∪ 𝐴 = ∪ 𝐶 )
7 fnerel ⊢ Rel Fne
8 7 brrelex2i ⊢ ( 𝐴 Fne 𝐵 → 𝐵 ∈ V )
9 1 2 isfne4b ⊢ ( 𝐵 ∈ V → ( 𝐴 Fne 𝐵 ↔ ( ∪ 𝐴 = ∪ 𝐵 ∧ ( topGen ‘ 𝐴 ) ⊆ ( topGen ‘ 𝐵 ) ) ) )
10 9 simplbda ⊢ ( ( 𝐵 ∈ V ∧ 𝐴 Fne 𝐵 ) → ( topGen ‘ 𝐴 ) ⊆ ( topGen ‘ 𝐵 ) )
11 8 10 mpancom ⊢ ( 𝐴 Fne 𝐵 → ( topGen ‘ 𝐴 ) ⊆ ( topGen ‘ 𝐵 ) )
12 7 brrelex2i ⊢ ( 𝐵 Fne 𝐶 → 𝐶 ∈ V )
13 2 4 isfne4b ⊢ ( 𝐶 ∈ V → ( 𝐵 Fne 𝐶 ↔ ( ∪ 𝐵 = ∪ 𝐶 ∧ ( topGen ‘ 𝐵 ) ⊆ ( topGen ‘ 𝐶 ) ) ) )
14 13 simplbda ⊢ ( ( 𝐶 ∈ V ∧ 𝐵 Fne 𝐶 ) → ( topGen ‘ 𝐵 ) ⊆ ( topGen ‘ 𝐶 ) )
15 12 14 mpancom ⊢ ( 𝐵 Fne 𝐶 → ( topGen ‘ 𝐵 ) ⊆ ( topGen ‘ 𝐶 ) )
16 11 15 sylan9ss ⊢ ( ( 𝐴 Fne 𝐵 ∧ 𝐵 Fne 𝐶 ) → ( topGen ‘ 𝐴 ) ⊆ ( topGen ‘ 𝐶 ) )
17 12 adantl ⊢ ( ( 𝐴 Fne 𝐵 ∧ 𝐵 Fne 𝐶 ) → 𝐶 ∈ V )
18 1 4 isfne4b ⊢ ( 𝐶 ∈ V → ( 𝐴 Fne 𝐶 ↔ ( ∪ 𝐴 = ∪ 𝐶 ∧ ( topGen ‘ 𝐴 ) ⊆ ( topGen ‘ 𝐶 ) ) ) )
19 17 18 syl ⊢ ( ( 𝐴 Fne 𝐵 ∧ 𝐵 Fne 𝐶 ) → ( 𝐴 Fne 𝐶 ↔ ( ∪ 𝐴 = ∪ 𝐶 ∧ ( topGen ‘ 𝐴 ) ⊆ ( topGen ‘ 𝐶 ) ) ) )
20 6 16 19 mpbir2and ⊢ ( ( 𝐴 Fne 𝐵 ∧ 𝐵 Fne 𝐶 ) → 𝐴 Fne 𝐶 )