This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sbthfilem

Description: Lemma for sbthfi . (Contributed by BTernaryTau, 4-Nov-2024)

Ref Expression
Hypotheses sbthfilem.1 
|- A e. _V
sbthfilem.2 
|- D = { x | ( x C_ A /\ ( g " ( B \ ( f " x ) ) ) C_ ( A \ x ) ) }
sbthfilem.3 
|- H = ( ( f |` U. D ) u. ( `' g |` ( A \ U. D ) ) )
sbthfilem.4 
|- B e. _V
Assertion sbthfilem 
|- ( ( B e. Fin /\ A ~<_ B /\ B ~<_ A ) -> A ~~ B )

Proof

Step Hyp Ref Expression
1 sbthfilem.1 
 |-  A e. _V
2 sbthfilem.2 
 |-  D = { x | ( x C_ A /\ ( g " ( B \ ( f " x ) ) ) C_ ( A \ x ) ) }
3 sbthfilem.3 
 |-  H = ( ( f |` U. D ) u. ( `' g |` ( A \ U. D ) ) )
4 sbthfilem.4 
 |-  B e. _V
5 19.42vv 
 |-  ( E. f E. g ( B e. Fin /\ ( f : A -1-1-> B /\ g : B -1-1-> A ) ) <-> ( B e. Fin /\ E. f E. g ( f : A -1-1-> B /\ g : B -1-1-> A ) ) )
6 3anass 
 |-  ( ( B e. Fin /\ f : A -1-1-> B /\ g : B -1-1-> A ) <-> ( B e. Fin /\ ( f : A -1-1-> B /\ g : B -1-1-> A ) ) )
7 6 2exbii 
 |-  ( E. f E. g ( B e. Fin /\ f : A -1-1-> B /\ g : B -1-1-> A ) <-> E. f E. g ( B e. Fin /\ ( f : A -1-1-> B /\ g : B -1-1-> A ) ) )
8 3anass 
 |-  ( ( B e. Fin /\ A ~<_ B /\ B ~<_ A ) <-> ( B e. Fin /\ ( A ~<_ B /\ B ~<_ A ) ) )
9 4 brdom 
 |-  ( A ~<_ B <-> E. f f : A -1-1-> B )
10 1 brdom 
 |-  ( B ~<_ A <-> E. g g : B -1-1-> A )
11 9 10 anbi12i 
 |-  ( ( A ~<_ B /\ B ~<_ A ) <-> ( E. f f : A -1-1-> B /\ E. g g : B -1-1-> A ) )
12 exdistrv 
 |-  ( E. f E. g ( f : A -1-1-> B /\ g : B -1-1-> A ) <-> ( E. f f : A -1-1-> B /\ E. g g : B -1-1-> A ) )
13 11 12 bitr4i 
 |-  ( ( A ~<_ B /\ B ~<_ A ) <-> E. f E. g ( f : A -1-1-> B /\ g : B -1-1-> A ) )
14 13 anbi2i 
 |-  ( ( B e. Fin /\ ( A ~<_ B /\ B ~<_ A ) ) <-> ( B e. Fin /\ E. f E. g ( f : A -1-1-> B /\ g : B -1-1-> A ) ) )
15 8 14 bitri 
 |-  ( ( B e. Fin /\ A ~<_ B /\ B ~<_ A ) <-> ( B e. Fin /\ E. f E. g ( f : A -1-1-> B /\ g : B -1-1-> A ) ) )
16 5 7 15 3bitr4ri 
 |-  ( ( B e. Fin /\ A ~<_ B /\ B ~<_ A ) <-> E. f E. g ( B e. Fin /\ f : A -1-1-> B /\ g : B -1-1-> A ) )
17 f1fn 
 |-  ( g : B -1-1-> A -> g Fn B )
18 vex 
 |-  f e. _V
19 18 resex 
 |-  ( f |` U. D ) e. _V
20 fnfi 
 |-  ( ( g Fn B /\ B e. Fin ) -> g e. Fin )
21 cnvfi 
 |-  ( g e. Fin -> `' g e. Fin )
22 resexg 
 |-  ( `' g e. Fin -> ( `' g |` ( A \ U. D ) ) e. _V )
23 20 21 22 3syl 
 |-  ( ( g Fn B /\ B e. Fin ) -> ( `' g |` ( A \ U. D ) ) e. _V )
24 unexg 
 |-  ( ( ( f |` U. D ) e. _V /\ ( `' g |` ( A \ U. D ) ) e. _V ) -> ( ( f |` U. D ) u. ( `' g |` ( A \ U. D ) ) ) e. _V )
25 19 23 24 sylancr 
 |-  ( ( g Fn B /\ B e. Fin ) -> ( ( f |` U. D ) u. ( `' g |` ( A \ U. D ) ) ) e. _V )
26 3 25 eqeltrid 
 |-  ( ( g Fn B /\ B e. Fin ) -> H e. _V )
27 26 ancoms 
 |-  ( ( B e. Fin /\ g Fn B ) -> H e. _V )
28 17 27 sylan2 
 |-  ( ( B e. Fin /\ g : B -1-1-> A ) -> H e. _V )
29 28 3adant2 
 |-  ( ( B e. Fin /\ f : A -1-1-> B /\ g : B -1-1-> A ) -> H e. _V )
30 1 2 3 sbthlem9 
 |-  ( ( f : A -1-1-> B /\ g : B -1-1-> A ) -> H : A -1-1-onto-> B )
31 30 3adant1 
 |-  ( ( B e. Fin /\ f : A -1-1-> B /\ g : B -1-1-> A ) -> H : A -1-1-onto-> B )
32 f1oen3g 
 |-  ( ( H e. _V /\ H : A -1-1-onto-> B ) -> A ~~ B )
33 29 31 32 syl2anc 
 |-  ( ( B e. Fin /\ f : A -1-1-> B /\ g : B -1-1-> A ) -> A ~~ B )
34 33 exlimivv 
 |-  ( E. f E. g ( B e. Fin /\ f : A -1-1-> B /\ g : B -1-1-> A ) -> A ~~ B )
35 16 34 sylbi 
 |-  ( ( B e. Fin /\ A ~<_ B /\ B ~<_ A ) -> A ~~ B )