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 ∧ g B ∖ f x ⊆ 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 ∧ g B ∖ f x ⊆ A ∖ x
3 sbthfilem.3 ⊢ H = f ↾ ⋃ D ∪ g -1 ↾ A ∖ ⋃ D
4 sbthfilem.4 ⊢ B ∈ V
5 19.42vv ⊢ ∃ f ∃ g B ∈ Fin ∧ f : A ⟶ 1-1 B ∧ g : B ⟶ 1-1 A ↔ B ∈ Fin ∧ ∃ f ∃ g f : A ⟶ 1-1 B ∧ g : B ⟶ 1-1 A
6 3anass ⊢ B ∈ Fin ∧ f : A ⟶ 1-1 B ∧ g : B ⟶ 1-1 A ↔ B ∈ Fin ∧ f : A ⟶ 1-1 B ∧ g : B ⟶ 1-1 A
7 6 2exbii ⊢ ∃ f ∃ g B ∈ Fin ∧ f : A ⟶ 1-1 B ∧ g : B ⟶ 1-1 A ↔ ∃ f ∃ g B ∈ Fin ∧ f : A ⟶ 1-1 B ∧ g : B ⟶ 1-1 A
8 3anass ⊢ B ∈ Fin ∧ A ≼ B ∧ B ≼ A ↔ B ∈ Fin ∧ A ≼ B ∧ B ≼ A
9 4 brdom ⊢ A ≼ B ↔ ∃ f f : A ⟶ 1-1 B
10 1 brdom ⊢ B ≼ A ↔ ∃ g g : B ⟶ 1-1 A
11 9 10 anbi12i ⊢ A ≼ B ∧ B ≼ A ↔ ∃ f f : A ⟶ 1-1 B ∧ ∃ g g : B ⟶ 1-1 A
12 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
13 11 12 bitr4i ⊢ A ≼ B ∧ B ≼ A ↔ ∃ f ∃ g f : A ⟶ 1-1 B ∧ g : B ⟶ 1-1 A
14 13 anbi2i ⊢ B ∈ Fin ∧ A ≼ B ∧ B ≼ A ↔ B ∈ Fin ∧ ∃ f ∃ g f : A ⟶ 1-1 B ∧ g : B ⟶ 1-1 A
15 8 14 bitri ⊢ B ∈ Fin ∧ A ≼ B ∧ B ≼ A ↔ B ∈ Fin ∧ ∃ f ∃ g f : A ⟶ 1-1 B ∧ g : B ⟶ 1-1 A
16 5 7 15 3bitr4ri ⊢ B ∈ Fin ∧ A ≼ B ∧ B ≼ A ↔ ∃ f ∃ g B ∈ Fin ∧ f : A ⟶ 1-1 B ∧ g : B ⟶ 1-1 A
17 f1fn ⊢ g : B ⟶ 1-1 A → g Fn B
18 vex ⊢ f ∈ V
19 18 resex ⊢ f ↾ ⋃ D ∈ V
20 fnfi ⊢ g Fn B ∧ 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 ⊢ g Fn B ∧ 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 ⊢ g Fn B ∧ B ∈ Fin → f ↾ ⋃ D ∪ g -1 ↾ A ∖ ⋃ D ∈ V
26 3 25 eqeltrid ⊢ g Fn B ∧ B ∈ Fin → H ∈ V
27 26 ancoms ⊢ B ∈ Fin ∧ g Fn B → H ∈ V
28 17 27 sylan2 ⊢ B ∈ Fin ∧ g : B ⟶ 1-1 A → H ∈ V
29 28 3adant2 ⊢ B ∈ Fin ∧ f : A ⟶ 1-1 B ∧ g : B ⟶ 1-1 A → H ∈ 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 ∈ Fin ∧ f : A ⟶ 1-1 B ∧ g : B ⟶ 1-1 A → H : A ⟶ 1-1 onto B
32 f1oen3g ⊢ H ∈ V ∧ H : A ⟶ 1-1 onto B → A ≈ B
33 29 31 32 syl2anc ⊢ B ∈ Fin ∧ f : A ⟶ 1-1 B ∧ g : B ⟶ 1-1 A → A ≈ B
34 33 exlimivv ⊢ ∃ f ∃ g B ∈ Fin ∧ f : A ⟶ 1-1 B ∧ g : B ⟶ 1-1 A → A ≈ B
35 16 34 sylbi ⊢ B ∈ Fin ∧ A ≼ B ∧ B ≼ A → A ≈ B