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	⊢ 𝐴 ∈ V
	phplem2OLD.2	⊢ 𝐵 ∈ V
Assertion	phplem3OLD	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ suc 𝐴 ) → 𝐴 ≈ ( suc 𝐴 ∖ { 𝐵 } ) )

Proof

Step	Hyp	Ref	Expression
1		phplem2OLD.1	⊢ 𝐴 ∈ V
2		phplem2OLD.2	⊢ 𝐵 ∈ V
3		elsuci	⊢ ( 𝐵 ∈ suc 𝐴 → ( 𝐵 ∈ 𝐴 ∨ 𝐵 = 𝐴 ) )
4	1 2	phplem2OLD	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴 ) → 𝐴 ≈ ( suc 𝐴 ∖ { 𝐵 } ) )
5	1	enref	⊢ 𝐴 ≈ 𝐴
6		nnord	⊢ ( 𝐴 ∈ ω → Ord 𝐴 )
7		orddif	⊢ ( Ord 𝐴 → 𝐴 = ( suc 𝐴 ∖ { 𝐴 } ) )
8	6 7	syl	⊢ ( 𝐴 ∈ ω → 𝐴 = ( suc 𝐴 ∖ { 𝐴 } ) )
9		sneq	⊢ ( 𝐴 = 𝐵 → { 𝐴 } = { 𝐵 } )
10	9	difeq2d	⊢ ( 𝐴 = 𝐵 → ( suc 𝐴 ∖ { 𝐴 } ) = ( suc 𝐴 ∖ { 𝐵 } ) )
11	10	eqcoms	⊢ ( 𝐵 = 𝐴 → ( suc 𝐴 ∖ { 𝐴 } ) = ( suc 𝐴 ∖ { 𝐵 } ) )
12	8 11	sylan9eq	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 = 𝐴 ) → 𝐴 = ( suc 𝐴 ∖ { 𝐵 } ) )
13	5 12	breqtrid	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 = 𝐴 ) → 𝐴 ≈ ( suc 𝐴 ∖ { 𝐵 } ) )
14	4 13	jaodan	⊢ ( ( 𝐴 ∈ ω ∧ ( 𝐵 ∈ 𝐴 ∨ 𝐵 = 𝐴 ) ) → 𝐴 ≈ ( suc 𝐴 ∖ { 𝐵 } ) )
15	3 14	sylan2	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ suc 𝐴 ) → 𝐴 ≈ ( suc 𝐴 ∖ { 𝐵 } ) )