Theorem phplem3OLD

Description: Obsolete version of phplem1 as of 23-Sep-2024. (Contributed by NM, 26-May-1998) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	phplem2OLD.1	$$⊢A\in \mathrm{V}$$
	phplem2OLD.2	$$⊢B\in \mathrm{V}$$
Assertion	phplem3OLD	$$⊢\left(A\in \mathrm{\omega }\wedge B\in \mathrm{suc}A\right)\to A\approx \left(\mathrm{suc}A\setminus \left\{B\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		phplem2OLD.1	$$⊢A\in \mathrm{V}$$
2		phplem2OLD.2	$$⊢B\in \mathrm{V}$$
3		elsuci	$$⊢B\in \mathrm{suc}A\to \left(B\in A\vee B=A\right)$$
4	1 2	phplem2OLD	$$⊢\left(A\in \mathrm{\omega }\wedge B\in A\right)\to A\approx \left(\mathrm{suc}A\setminus \left\{B\right\}\right)$$
5	1	enref	$$⊢A\approx A$$
6		nnord	$$⊢A\in \mathrm{\omega }\to \mathrm{Ord}A$$
7		orddif	$$⊢\mathrm{Ord}A\to A=\mathrm{suc}A\setminus \left\{A\right\}$$
8	6 7	syl	$$⊢A\in \mathrm{\omega }\to A=\mathrm{suc}A\setminus \left\{A\right\}$$
9		sneq	$$⊢A=B\to \left\{A\right\}=\left\{B\right\}$$
10	9	difeq2d	$$⊢A=B\to \mathrm{suc}A\setminus \left\{A\right\}=\mathrm{suc}A\setminus \left\{B\right\}$$
11	10	eqcoms	$$⊢B=A\to \mathrm{suc}A\setminus \left\{A\right\}=\mathrm{suc}A\setminus \left\{B\right\}$$
12	8 11	sylan9eq	$$⊢\left(A\in \mathrm{\omega }\wedge B=A\right)\to A=\mathrm{suc}A\setminus \left\{B\right\}$$
13	5 12	breqtrid	$$⊢\left(A\in \mathrm{\omega }\wedge B=A\right)\to A\approx \left(\mathrm{suc}A\setminus \left\{B\right\}\right)$$
14	4 13	jaodan	$$⊢\left(A\in \mathrm{\omega }\wedge \left(B\in A\vee B=A\right)\right)\to A\approx \left(\mathrm{suc}A\setminus \left\{B\right\}\right)$$
15	3 14	sylan2	$$⊢\left(A\in \mathrm{\omega }\wedge B\in \mathrm{suc}A\right)\to A\approx \left(\mathrm{suc}A\setminus \left\{B\right\}\right)$$