Metamath Proof Explorer

Theorem sbthfi

Description: Schroeder-Bernstein Theorem for finite sets, proved without using the Axiom of Power Sets (unlike sbth ). (Contributed by BTernaryTau, 4-Nov-2024)

Ref Expression
Assertion sbthfi ⊢ B ∈ Fin ∧ A ≼ B ∧ B ≼ A → A ≈ B

Proof

Step Hyp Ref Expression
1 reldom ⊢ Rel ⁡ ≼
2 1 brrelex1i ⊢ A ≼ B → A ∈ V
3 1 brrelex1i ⊢ B ≼ A → B ∈ V
4 breq1 ⊢ z = A → z ≼ w ↔ A ≼ w
5 breq2 ⊢ z = A → w ≼ z ↔ w ≼ A
6 4 5 3anbi23d ⊢ z = A → w ∈ Fin ∧ z ≼ w ∧ w ≼ z ↔ w ∈ Fin ∧ A ≼ w ∧ w ≼ A
7 breq1 ⊢ z = A → z ≈ w ↔ A ≈ w
8 6 7 imbi12d ⊢ z = A → w ∈ Fin ∧ z ≼ w ∧ w ≼ z → z ≈ w ↔ w ∈ Fin ∧ A ≼ w ∧ w ≼ A → A ≈ w
9 eleq1 ⊢ w = B → w ∈ Fin ↔ B ∈ Fin
10 breq2 ⊢ w = B → A ≼ w ↔ A ≼ B
11 breq1 ⊢ w = B → w ≼ A ↔ B ≼ A
12 9 10 11 3anbi123d ⊢ w = B → w ∈ Fin ∧ A ≼ w ∧ w ≼ A ↔ B ∈ Fin ∧ A ≼ B ∧ B ≼ A
13 breq2 ⊢ w = B → A ≈ w ↔ A ≈ B
14 12 13 imbi12d ⊢ w = B → w ∈ Fin ∧ A ≼ w ∧ w ≼ A → A ≈ w ↔ B ∈ Fin ∧ A ≼ B ∧ B ≼ A → A ≈ B
15 vex ⊢ z ∈ V
16 sseq1 ⊢ y = x → y ⊆ z ↔ x ⊆ z
17 imaeq2 ⊢ y = x → f y = f x
18 17 difeq2d ⊢ y = x → w ∖ f y = w ∖ f x
19 18 imaeq2d ⊢ y = x → g w ∖ f y = g w ∖ f x
20 difeq2 ⊢ y = x → z ∖ y = z ∖ x
21 19 20 sseq12d ⊢ y = x → g w ∖ f y ⊆ z ∖ y ↔ g w ∖ f x ⊆ z ∖ x
22 16 21 anbi12d ⊢ y = x → y ⊆ z ∧ g w ∖ f y ⊆ z ∖ y ↔ x ⊆ z ∧ g w ∖ f x ⊆ z ∖ x
23 22 cbvabv ⊢ y | y ⊆ z ∧ g w ∖ f y ⊆ z ∖ y = x | x ⊆ z ∧ g w ∖ f x ⊆ z ∖ x
24 eqid ⊢ f ↾ ⋃ y | y ⊆ z ∧ g w ∖ f y ⊆ z ∖ y ∪ g -1 ↾ z ∖ ⋃ y | y ⊆ z ∧ g w ∖ f y ⊆ z ∖ y = f ↾ ⋃ y | y ⊆ z ∧ g w ∖ f y ⊆ z ∖ y ∪ g -1 ↾ z ∖ ⋃ y | y ⊆ z ∧ g w ∖ f y ⊆ z ∖ y
25 vex ⊢ w ∈ V
26 15 23 24 25 sbthfilem ⊢ w ∈ Fin ∧ z ≼ w ∧ w ≼ z → z ≈ w
27 8 14 26 vtocl2g ⊢ A ∈ V ∧ B ∈ V → B ∈ Fin ∧ A ≼ B ∧ B ≼ A → A ≈ B
28 2 3 27 syl2an ⊢ A ≼ B ∧ B ≼ A → B ∈ Fin ∧ A ≼ B ∧ B ≼ A → A ≈ B
29 28 3adant1 ⊢ B ∈ Fin ∧ A ≼ B ∧ B ≼ A → B ∈ Fin ∧ A ≼ B ∧ B ≼ A → A ≈ B
30 29 pm2.43i ⊢ B ∈ Fin ∧ A ≼ B ∧ B ≼ A → A ≈ B