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	⊢ ( ( 𝐵 ∈ Fin ∧ 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴 ) → 𝐴 ≈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		reldom	⊢ Rel ≼
2	1	brrelex1i	⊢ ( 𝐴 ≼ 𝐵 → 𝐴 ∈ V )
3	1	brrelex1i	⊢ ( 𝐵 ≼ 𝐴 → 𝐵 ∈ V )
4		breq1	⊢ ( 𝑧 = 𝐴 → ( 𝑧 ≼ 𝑤 ↔ 𝐴 ≼ 𝑤 ) )
5		breq2	⊢ ( 𝑧 = 𝐴 → ( 𝑤 ≼ 𝑧 ↔ 𝑤 ≼ 𝐴 ) )
6	4 5	3anbi23d	⊢ ( 𝑧 = 𝐴 → ( ( 𝑤 ∈ Fin ∧ 𝑧 ≼ 𝑤 ∧ 𝑤 ≼ 𝑧 ) ↔ ( 𝑤 ∈ Fin ∧ 𝐴 ≼ 𝑤 ∧ 𝑤 ≼ 𝐴 ) ) )
7		breq1	⊢ ( 𝑧 = 𝐴 → ( 𝑧 ≈ 𝑤 ↔ 𝐴 ≈ 𝑤 ) )
8	6 7	imbi12d	⊢ ( 𝑧 = 𝐴 → ( ( ( 𝑤 ∈ Fin ∧ 𝑧 ≼ 𝑤 ∧ 𝑤 ≼ 𝑧 ) → 𝑧 ≈ 𝑤 ) ↔ ( ( 𝑤 ∈ Fin ∧ 𝐴 ≼ 𝑤 ∧ 𝑤 ≼ 𝐴 ) → 𝐴 ≈ 𝑤 ) ) )
9		eleq1	⊢ ( 𝑤 = 𝐵 → ( 𝑤 ∈ Fin ↔ 𝐵 ∈ Fin ) )
10		breq2	⊢ ( 𝑤 = 𝐵 → ( 𝐴 ≼ 𝑤 ↔ 𝐴 ≼ 𝐵 ) )
11		breq1	⊢ ( 𝑤 = 𝐵 → ( 𝑤 ≼ 𝐴 ↔ 𝐵 ≼ 𝐴 ) )
12	9 10 11	3anbi123d	⊢ ( 𝑤 = 𝐵 → ( ( 𝑤 ∈ Fin ∧ 𝐴 ≼ 𝑤 ∧ 𝑤 ≼ 𝐴 ) ↔ ( 𝐵 ∈ Fin ∧ 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴 ) ) )
13		breq2	⊢ ( 𝑤 = 𝐵 → ( 𝐴 ≈ 𝑤 ↔ 𝐴 ≈ 𝐵 ) )
14	12 13	imbi12d	⊢ ( 𝑤 = 𝐵 → ( ( ( 𝑤 ∈ Fin ∧ 𝐴 ≼ 𝑤 ∧ 𝑤 ≼ 𝐴 ) → 𝐴 ≈ 𝑤 ) ↔ ( ( 𝐵 ∈ Fin ∧ 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴 ) → 𝐴 ≈ 𝐵 ) ) )
15		vex	⊢ 𝑧 ∈ V
16		sseq1	⊢ ( 𝑦 = 𝑥 → ( 𝑦 ⊆ 𝑧 ↔ 𝑥 ⊆ 𝑧 ) )
17		imaeq2	⊢ ( 𝑦 = 𝑥 → ( 𝑓 “ 𝑦 ) = ( 𝑓 “ 𝑥 ) )
18	17	difeq2d	⊢ ( 𝑦 = 𝑥 → ( 𝑤 ∖ ( 𝑓 “ 𝑦 ) ) = ( 𝑤 ∖ ( 𝑓 “ 𝑥 ) ) )
19	18	imaeq2d	⊢ ( 𝑦 = 𝑥 → ( 𝑔 “ ( 𝑤 ∖ ( 𝑓 “ 𝑦 ) ) ) = ( 𝑔 “ ( 𝑤 ∖ ( 𝑓 “ 𝑥 ) ) ) )
20		difeq2	⊢ ( 𝑦 = 𝑥 → ( 𝑧 ∖ 𝑦 ) = ( 𝑧 ∖ 𝑥 ) )
21	19 20	sseq12d	⊢ ( 𝑦 = 𝑥 → ( ( 𝑔 “ ( 𝑤 ∖ ( 𝑓 “ 𝑦 ) ) ) ⊆ ( 𝑧 ∖ 𝑦 ) ↔ ( 𝑔 “ ( 𝑤 ∖ ( 𝑓 “ 𝑥 ) ) ) ⊆ ( 𝑧 ∖ 𝑥 ) ) )
22	16 21	anbi12d	⊢ ( 𝑦 = 𝑥 → ( ( 𝑦 ⊆ 𝑧 ∧ ( 𝑔 “ ( 𝑤 ∖ ( 𝑓 “ 𝑦 ) ) ) ⊆ ( 𝑧 ∖ 𝑦 ) ) ↔ ( 𝑥 ⊆ 𝑧 ∧ ( 𝑔 “ ( 𝑤 ∖ ( 𝑓 “ 𝑥 ) ) ) ⊆ ( 𝑧 ∖ 𝑥 ) ) ) )
23	22	cbvabv	⊢ { 𝑦 ∣ ( 𝑦 ⊆ 𝑧 ∧ ( 𝑔 “ ( 𝑤 ∖ ( 𝑓 “ 𝑦 ) ) ) ⊆ ( 𝑧 ∖ 𝑦 ) ) } = { 𝑥 ∣ ( 𝑥 ⊆ 𝑧 ∧ ( 𝑔 “ ( 𝑤 ∖ ( 𝑓 “ 𝑥 ) ) ) ⊆ ( 𝑧 ∖ 𝑥 ) ) }
24		eqid	⊢ ( ( 𝑓 ↾ ∪ { 𝑦 ∣ ( 𝑦 ⊆ 𝑧 ∧ ( 𝑔 “ ( 𝑤 ∖ ( 𝑓 “ 𝑦 ) ) ) ⊆ ( 𝑧 ∖ 𝑦 ) ) } ) ∪ ( ◡ 𝑔 ↾ ( 𝑧 ∖ ∪ { 𝑦 ∣ ( 𝑦 ⊆ 𝑧 ∧ ( 𝑔 “ ( 𝑤 ∖ ( 𝑓 “ 𝑦 ) ) ) ⊆ ( 𝑧 ∖ 𝑦 ) ) } ) ) ) = ( ( 𝑓 ↾ ∪ { 𝑦 ∣ ( 𝑦 ⊆ 𝑧 ∧ ( 𝑔 “ ( 𝑤 ∖ ( 𝑓 “ 𝑦 ) ) ) ⊆ ( 𝑧 ∖ 𝑦 ) ) } ) ∪ ( ◡ 𝑔 ↾ ( 𝑧 ∖ ∪ { 𝑦 ∣ ( 𝑦 ⊆ 𝑧 ∧ ( 𝑔 “ ( 𝑤 ∖ ( 𝑓 “ 𝑦 ) ) ) ⊆ ( 𝑧 ∖ 𝑦 ) ) } ) ) )
25		vex	⊢ 𝑤 ∈ V
26	15 23 24 25	sbthfilem	⊢ ( ( 𝑤 ∈ Fin ∧ 𝑧 ≼ 𝑤 ∧ 𝑤 ≼ 𝑧 ) → 𝑧 ≈ 𝑤 )
27	8 14 26	vtocl2g	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( ( 𝐵 ∈ Fin ∧ 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴 ) → 𝐴 ≈ 𝐵 ) )
28	2 3 27	syl2an	⊢ ( ( 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴 ) → ( ( 𝐵 ∈ Fin ∧ 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴 ) → 𝐴 ≈ 𝐵 ) )
29	28	3adant1	⊢ ( ( 𝐵 ∈ Fin ∧ 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴 ) → ( ( 𝐵 ∈ Fin ∧ 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴 ) → 𝐴 ≈ 𝐵 ) )
30	29	pm2.43i	⊢ ( ( 𝐵 ∈ Fin ∧ 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴 ) → 𝐴 ≈ 𝐵 )