Metamath Proof Explorer


Theorem sbthlem9

Description: Lemma for sbth . (Contributed by NM, 28-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 sbthlem9 f : A 1-1 B g : B 1-1 A H : A 1-1 onto B

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 1 2 3 sbthlem7 Fun f Fun g -1 Fun H
5 1 2 3 sbthlem5 dom f = A ran g A dom H = A
6 5 adantrl dom f = A Fun g dom g = B ran g A dom H = A
7 4 6 anim12i Fun f Fun g -1 dom f = A Fun g dom g = B ran g A Fun H dom H = A
8 7 an42s Fun f dom f = A Fun g dom g = B ran g A Fun g -1 Fun H dom H = A
9 8 adantlr Fun f dom f = A ran f B Fun g dom g = B ran g A Fun g -1 Fun H dom H = A
10 9 adantlr Fun f dom f = A ran f B Fun f -1 Fun g dom g = B ran g A Fun g -1 Fun H dom H = A
11 1 2 3 sbthlem8 Fun f -1 Fun g dom g = B ran g A Fun g -1 Fun H -1
12 11 adantll Fun f dom f = A ran f B Fun f -1 Fun g dom g = B ran g A Fun g -1 Fun H -1
13 simpr Fun g dom g = B dom g = B
14 13 anim1i Fun g dom g = B ran g A dom g = B ran g A
15 df-rn ran H = dom H -1
16 1 2 3 sbthlem6 ran f B dom g = B ran g A Fun g -1 ran H = B
17 15 16 eqtr3id ran f B dom g = B ran g A Fun g -1 dom H -1 = B
18 14 17 sylanr1 ran f B Fun g dom g = B ran g A Fun g -1 dom H -1 = B
19 18 adantll Fun f dom f = A ran f B Fun g dom g = B ran g A Fun g -1 dom H -1 = B
20 19 adantlr Fun f dom f = A ran f B Fun f -1 Fun g dom g = B ran g A Fun g -1 dom H -1 = B
21 10 12 20 jca32 Fun f dom f = A ran f B Fun f -1 Fun g dom g = B ran g A Fun g -1 Fun H dom H = A Fun H -1 dom H -1 = B
22 df-f1 f : A 1-1 B f : A B Fun f -1
23 df-f f : A B f Fn A ran f B
24 df-fn f Fn A Fun f dom f = A
25 24 anbi1i f Fn A ran f B Fun f dom f = A ran f B
26 23 25 bitri f : A B Fun f dom f = A ran f B
27 26 anbi1i f : A B Fun f -1 Fun f dom f = A ran f B Fun f -1
28 22 27 bitri f : A 1-1 B Fun f dom f = A ran f B Fun f -1
29 df-f1 g : B 1-1 A g : B A Fun g -1
30 df-f g : B A g Fn B ran g A
31 df-fn g Fn B Fun g dom g = B
32 31 anbi1i g Fn B ran g A Fun g dom g = B ran g A
33 30 32 bitri g : B A Fun g dom g = B ran g A
34 33 anbi1i g : B A Fun g -1 Fun g dom g = B ran g A Fun g -1
35 29 34 bitri g : B 1-1 A Fun g dom g = B ran g A Fun g -1
36 28 35 anbi12i f : A 1-1 B g : B 1-1 A Fun f dom f = A ran f B Fun f -1 Fun g dom g = B ran g A Fun g -1
37 dff1o4 H : A 1-1 onto B H Fn A H -1 Fn B
38 df-fn H Fn A Fun H dom H = A
39 df-fn H -1 Fn B Fun H -1 dom H -1 = B
40 38 39 anbi12i H Fn A H -1 Fn B Fun H dom H = A Fun H -1 dom H -1 = B
41 37 40 bitri H : A 1-1 onto B Fun H dom H = A Fun H -1 dom H -1 = B
42 21 36 41 3imtr4i f : A 1-1 B g : B 1-1 A H : A 1-1 onto B