Metamath Proof Explorer

Theorem sbthfilem

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

Ref Expression
Hypotheses sbthfilem.1 ⊢A∈V
sbthfilem.2 ⊢D=x|x⊆A∧gB∖fx⊆A∖x
sbthfilem.3 ⊢H=f↾⋃D∪g-1↾A∖⋃D
sbthfilem.4 ⊢B∈V
Assertion sbthfilem ⊢B∈Fin∧A≼B∧B≼A→A≈B

Proof

Step Hyp Ref Expression
1 sbthfilem.1 ⊢A∈V
2 sbthfilem.2 ⊢D=x|x⊆A∧gB∖fx⊆A∖x
3 sbthfilem.3 ⊢H=f↾⋃D∪g-1↾A∖⋃D
4 sbthfilem.4 ⊢B∈V
5 19.42vv ⊢∃f∃gB∈Fin∧f:A⟶1-1B∧g:B⟶1-1A↔B∈Fin∧∃f∃gf:A⟶1-1B∧g:B⟶1-1A
6 3anass ⊢B∈Fin∧f:A⟶1-1B∧g:B⟶1-1A↔B∈Fin∧f:A⟶1-1B∧g:B⟶1-1A
7 6 2exbii ⊢∃f∃gB∈Fin∧f:A⟶1-1B∧g:B⟶1-1A↔∃f∃gB∈Fin∧f:A⟶1-1B∧g:B⟶1-1A
8 3anass ⊢B∈Fin∧A≼B∧B≼A↔B∈Fin∧A≼B∧B≼A
9 4 brdom ⊢A≼B↔∃ff:A⟶1-1B
10 1 brdom ⊢B≼A↔∃gg:B⟶1-1A
11 9 10 anbi12i ⊢A≼B∧B≼A↔∃ff:A⟶1-1B∧∃gg:B⟶1-1A
12 exdistrv ⊢∃f∃gf:A⟶1-1B∧g:B⟶1-1A↔∃ff:A⟶1-1B∧∃gg:B⟶1-1A
13 11 12 bitr4i ⊢A≼B∧B≼A↔∃f∃gf:A⟶1-1B∧g:B⟶1-1A
14 13 anbi2i ⊢B∈Fin∧A≼B∧B≼A↔B∈Fin∧∃f∃gf:A⟶1-1B∧g:B⟶1-1A
15 8 14 bitri ⊢B∈Fin∧A≼B∧B≼A↔B∈Fin∧∃f∃gf:A⟶1-1B∧g:B⟶1-1A
16 5 7 15 3bitr4ri ⊢B∈Fin∧A≼B∧B≼A↔∃f∃gB∈Fin∧f:A⟶1-1B∧g:B⟶1-1A
17 f1fn ⊢g:B⟶1-1A→gFnB
18 vex ⊢f∈V
19 18 resex ⊢f↾⋃D∈V
20 fnfi ⊢gFnB∧B∈Fin→g∈Fin
21 cnvfi ⊢g∈Fin→g-1∈Fin
22 resexg ⊢g-1∈Fin→g-1↾A∖⋃D∈V
23 20 21 22 3syl ⊢gFnB∧B∈Fin→g-1↾A∖⋃D∈V
24 unexg ⊢f↾⋃D∈V∧g-1↾A∖⋃D∈V→f↾⋃D∪g-1↾A∖⋃D∈V
25 19 23 24 sylancr ⊢gFnB∧B∈Fin→f↾⋃D∪g-1↾A∖⋃D∈V
26 3 25 eqeltrid ⊢gFnB∧B∈Fin→H∈V
27 26 ancoms ⊢B∈Fin∧gFnB→H∈V
28 17 27 sylan2 ⊢B∈Fin∧g:B⟶1-1A→H∈V
29 28 3adant2 ⊢B∈Fin∧f:A⟶1-1B∧g:B⟶1-1A→H∈V
30 1 2 3 sbthlem9 ⊢f:A⟶1-1B∧g:B⟶1-1A→H:A⟶1-1 ontoB
31 30 3adant1 ⊢B∈Fin∧f:A⟶1-1B∧g:B⟶1-1A→H:A⟶1-1 ontoB
32 f1oen3g ⊢H∈V∧H:A⟶1-1 ontoB→A≈B
33 29 31 32 syl2anc ⊢B∈Fin∧f:A⟶1-1B∧g:B⟶1-1A→A≈B
34 33 exlimivv ⊢∃f∃gB∈Fin∧f:A⟶1-1B∧g:B⟶1-1A→A≈B
35 16 34 sylbi ⊢B∈Fin∧A≼B∧B≼A→A≈B