Metamath Proof Explorer


Theorem isfne2

Description: The predicate " B is finer than A ". (Contributed by Jeff Hankins, 28-Sep-2009) (Proof shortened by Mario Carneiro, 11-Sep-2015)

Ref Expression
Hypotheses isfne.1 𝑋 = 𝐴
isfne.2 𝑌 = 𝐵
Assertion isfne2 ( 𝐵𝐶 → ( 𝐴 Fne 𝐵 ↔ ( 𝑋 = 𝑌 ∧ ∀ 𝑥𝐴𝑦𝑥𝑧𝐵 ( 𝑦𝑧𝑧𝑥 ) ) ) )

Proof

Step Hyp Ref Expression
1 isfne.1 𝑋 = 𝐴
2 isfne.2 𝑌 = 𝐵
3 1 2 isfne4 ( 𝐴 Fne 𝐵 ↔ ( 𝑋 = 𝑌𝐴 ⊆ ( topGen ‘ 𝐵 ) ) )
4 dfss3 ( 𝐴 ⊆ ( topGen ‘ 𝐵 ) ↔ ∀ 𝑥𝐴 𝑥 ∈ ( topGen ‘ 𝐵 ) )
5 eltg2b ( 𝐵𝐶 → ( 𝑥 ∈ ( topGen ‘ 𝐵 ) ↔ ∀ 𝑦𝑥𝑧𝐵 ( 𝑦𝑧𝑧𝑥 ) ) )
6 5 ralbidv ( 𝐵𝐶 → ( ∀ 𝑥𝐴 𝑥 ∈ ( topGen ‘ 𝐵 ) ↔ ∀ 𝑥𝐴𝑦𝑥𝑧𝐵 ( 𝑦𝑧𝑧𝑥 ) ) )
7 4 6 syl5bb ( 𝐵𝐶 → ( 𝐴 ⊆ ( topGen ‘ 𝐵 ) ↔ ∀ 𝑥𝐴𝑦𝑥𝑧𝐵 ( 𝑦𝑧𝑧𝑥 ) ) )
8 7 anbi2d ( 𝐵𝐶 → ( ( 𝑋 = 𝑌𝐴 ⊆ ( topGen ‘ 𝐵 ) ) ↔ ( 𝑋 = 𝑌 ∧ ∀ 𝑥𝐴𝑦𝑥𝑧𝐵 ( 𝑦𝑧𝑧𝑥 ) ) ) )
9 3 8 syl5bb ( 𝐵𝐶 → ( 𝐴 Fne 𝐵 ↔ ( 𝑋 = 𝑌 ∧ ∀ 𝑥𝐴𝑦𝑥𝑧𝐵 ( 𝑦𝑧𝑧𝑥 ) ) ) )