Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem sbthlem2 3350

Description: Lemma for Schroeder-Bernstein Theorem.

**Hypotheses**
Ref	Expression
sbthlem.1
sbthlem.2	$/\$

**Assertion**
Ref	Expression
sbthlem2

Distinct variable group(s):

**Proof of Theorem sbthlem2**
Step	Hyp	Ref	Expression
1		sbthlem.1	. . . . . . . . . . 11
2		sbthlem.2	. . . . . . . . . . 11 $/\$
3	1, 2	sbthlem1 3349	. . . . . . . . . 10
4		imass2 2622	. . . . . . . . . 10
5	3, 4	ax-mp 6	. . . . . . . . 9
6		sscon 1599	. . . . . . . . 9
7	5, 6	ax-mp 6	. . . . . . . 8
8		imass2 2622	. . . . . . . 8
9	7, 8	ax-mp 6	. . . . . . 7
10		sscon 1599	. . . . . . 7
11	9, 10	ax-mp 6	. . . . . 6
12		imassrn 2611	. . . . . . . 8
13		sstr2 1510	. . . . . . . 8
14	12, 13	ax-mp 6	. . . . . . 7
15		difss 1596	. . . . . . . 8
16		ssconb 1598	. . . . . . . 8 $/\$
17	15, 16	mpan2 519	. . . . . . 7
18	14, 17	syl 12	. . . . . 6
19	11, 18	mpbiri 169	. . . . 5
20	19, 15	jctil 240	. . . 4 $/\$
21	1, 15	ssexi 1701	. . . . 5
22		sseq1 1521	. . . . . 6
23		difeq2 1583	. . . . . . . 8
24	23	sseq2d 1528	. . . . . . 7
25		imaeq2 2603	. . . . . . . . 9
26	25	difeq2d 1588	. . . . . . . 8
27		imaeq2 2603	. . . . . . . 8
28		sseq1 1521	. . . . . . . 8
29	26, 27, 28	3syl 21	. . . . . . 7
30	24, 29	bitrd 406	. . . . . 6
31	22, 30	anbi12d 476	. . . . 5 $/\$