Metamath Proof Explorer


Theorem sbthlem10

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
sbthlem.4 B V
Assertion sbthlem10 A B B A A 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 sbthlem.4 B V
5 4 brdom A B f f : A 1-1 B
6 1 brdom B A g g : B 1-1 A
7 5 6 anbi12i A B B A f f : A 1-1 B g g : B 1-1 A
8 exdistrv f g f : A 1-1 B g : B 1-1 A f f : A 1-1 B g g : B 1-1 A
9 7 8 bitr4i A B B A f g f : A 1-1 B g : B 1-1 A
10 vex f V
11 10 resex f D V
12 vex g V
13 12 cnvex g -1 V
14 13 resex g -1 A D V
15 11 14 unex f D g -1 A D V
16 3 15 eqeltri H V
17 1 2 3 sbthlem9 f : A 1-1 B g : B 1-1 A H : A 1-1 onto B
18 f1oen3g H V H : A 1-1 onto B A B
19 16 17 18 sylancr f : A 1-1 B g : B 1-1 A A B
20 19 exlimivv f g f : A 1-1 B g : B 1-1 A A B
21 9 20 sylbi A B B A A B