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