This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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