Metamath Proof Explorer


Theorem sbthlem4

Description: Lemma for sbth . (Contributed by NM, 27-Mar-1998)

Ref Expression
Hypotheses sbthlem.1 A V
sbthlem.2 D = x | x A g B f x A x
Assertion sbthlem4 dom g = B ran g A Fun g -1 g -1 A D = B f D

Proof

Step Hyp Ref Expression
1 sbthlem.1 A V
2 sbthlem.2 D = x | x A g B f x A x
3 dfdm4 dom g B f D = ran g B f D -1
4 difss B f D B
5 sseq2 dom g = B B f D dom g B f D B
6 4 5 mpbiri dom g = B B f D dom g
7 ssdmres B f D dom g dom g B f D = B f D
8 6 7 sylib dom g = B dom g B f D = B f D
9 3 8 syl5reqr dom g = B B f D = ran g B f D -1
10 funcnvres Fun g -1 g B f D -1 = g -1 g B f D
11 1 2 sbthlem3 ran g A g B f D = A D
12 11 reseq2d ran g A g -1 g B f D = g -1 A D
13 10 12 sylan9eqr ran g A Fun g -1 g B f D -1 = g -1 A D
14 13 rneqd ran g A Fun g -1 ran g B f D -1 = ran g -1 A D
15 9 14 sylan9eq dom g = B ran g A Fun g -1 B f D = ran g -1 A D
16 15 anassrs dom g = B ran g A Fun g -1 B f D = ran g -1 A D
17 df-ima g -1 A D = ran g -1 A D
18 16 17 syl6reqr dom g = B ran g A Fun g -1 g -1 A D = B f D