Metamath Proof Explorer


Theorem isfne3

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

Ref Expression
Hypotheses isfne.1 X = A
isfne.2 Y = B
Assertion isfne3 B C A Fne B X = Y x A y y B x = y

Proof

Step Hyp Ref Expression
1 isfne.1 X = A
2 isfne.2 Y = B
3 1 2 isfne4 A Fne B X = Y A topGen B
4 dfss3 A topGen B x A x topGen B
5 eltg3 B C x topGen B y y B x = y
6 5 ralbidv B C x A x topGen B x A y y B x = y
7 4 6 syl5bb B C A topGen B x A y y B x = y
8 7 anbi2d B C X = Y A topGen B X = Y x A y y B x = y
9 3 8 syl5bb B C A Fne B X = Y x A y y B x = y