Metamath Proof Explorer


Theorem sbthlem8

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
sbthlem.3 H = f D g -1 A D
Assertion sbthlem8 Fun f -1 Fun g dom g = B ran g A Fun g -1 Fun H -1

Proof

Step Hyp Ref Expression
1 sbthlem.1 A V
2 sbthlem.2 D = x | x A g B f x A x
3 sbthlem.3 H = f D g -1 A D
4 funres11 Fun f -1 Fun f D -1
5 funcnvcnv Fun g Fun g -1 -1
6 funres11 Fun g -1 -1 Fun g -1 A D -1
7 5 6 syl Fun g Fun g -1 A D -1
8 7 ad3antrrr Fun g dom g = B ran g A Fun g -1 Fun g -1 A D -1
9 4 8 anim12i Fun f -1 Fun g dom g = B ran g A Fun g -1 Fun f D -1 Fun g -1 A D -1
10 df-ima f D = ran f D
11 df-rn ran f D = dom f D -1
12 10 11 eqtr2i dom f D -1 = f D
13 df-ima g -1 A D = ran g -1 A D
14 df-rn ran g -1 A D = dom g -1 A D -1
15 13 14 eqtri g -1 A D = dom g -1 A D -1
16 1 2 sbthlem4 dom g = B ran g A Fun g -1 g -1 A D = B f D
17 15 16 eqtr3id dom g = B ran g A Fun g -1 dom g -1 A D -1 = B f D
18 ineq12 dom f D -1 = f D dom g -1 A D -1 = B f D dom f D -1 dom g -1 A D -1 = f D B f D
19 12 17 18 sylancr dom g = B ran g A Fun g -1 dom f D -1 dom g -1 A D -1 = f D B f D
20 disjdif f D B f D =
21 19 20 eqtrdi dom g = B ran g A Fun g -1 dom f D -1 dom g -1 A D -1 =
22 21 adantlll Fun g dom g = B ran g A Fun g -1 dom f D -1 dom g -1 A D -1 =
23 22 adantl Fun f -1 Fun g dom g = B ran g A Fun g -1 dom f D -1 dom g -1 A D -1 =
24 funun Fun f D -1 Fun g -1 A D -1 dom f D -1 dom g -1 A D -1 = Fun f D -1 g -1 A D -1
25 9 23 24 syl2anc Fun f -1 Fun g dom g = B ran g A Fun g -1 Fun f D -1 g -1 A D -1
26 3 cnveqi H -1 = f D g -1 A D -1
27 cnvun f D g -1 A D -1 = f D -1 g -1 A D -1
28 26 27 eqtri H -1 = f D -1 g -1 A D -1
29 28 funeqi Fun H -1 Fun f D -1 g -1 A D -1
30 25 29 sylibr Fun f -1 Fun g dom g = B ran g A Fun g -1 Fun H -1