Theorem phplem2OLD

Description: Obsolete lemma for php . (Contributed by NM, 11-Jun-1998) (Revised by Mario Carneiro, 16-Nov-2014) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	phplem2OLD.1	⊢ 𝐴 ∈ V
	phplem2OLD.2	⊢ 𝐵 ∈ V
Assertion	phplem2OLD	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴 ) → 𝐴 ≈ ( suc 𝐴 ∖ { 𝐵 } ) )

Proof

Step	Hyp	Ref	Expression
1		phplem2OLD.1	⊢ 𝐴 ∈ V
2		phplem2OLD.2	⊢ 𝐵 ∈ V
3		snex	⊢ { ⟨ 𝐵 , 𝐴 ⟩ } ∈ V
4	2 1	f1osn	⊢ { ⟨ 𝐵 , 𝐴 ⟩ } : { 𝐵 } –1-1-onto→ { 𝐴 }
5		f1oen3g	⊢ ( ( { ⟨ 𝐵 , 𝐴 ⟩ } ∈ V ∧ { ⟨ 𝐵 , 𝐴 ⟩ } : { 𝐵 } –1-1-onto→ { 𝐴 } ) → { 𝐵 } ≈ { 𝐴 } )
6	3 4 5	mp2an	⊢ { 𝐵 } ≈ { 𝐴 }
7	1	difexi	⊢ ( 𝐴 ∖ { 𝐵 } ) ∈ V
8	7	enref	⊢ ( 𝐴 ∖ { 𝐵 } ) ≈ ( 𝐴 ∖ { 𝐵 } )
9	6 8	pm3.2i	⊢ ( { 𝐵 } ≈ { 𝐴 } ∧ ( 𝐴 ∖ { 𝐵 } ) ≈ ( 𝐴 ∖ { 𝐵 } ) )
10		incom	⊢ ( { 𝐴 } ∩ ( 𝐴 ∖ { 𝐵 } ) ) = ( ( 𝐴 ∖ { 𝐵 } ) ∩ { 𝐴 } )
11		difss	⊢ ( 𝐴 ∖ { 𝐵 } ) ⊆ 𝐴
12		ssrin	⊢ ( ( 𝐴 ∖ { 𝐵 } ) ⊆ 𝐴 → ( ( 𝐴 ∖ { 𝐵 } ) ∩ { 𝐴 } ) ⊆ ( 𝐴 ∩ { 𝐴 } ) )
13	11 12	ax-mp	⊢ ( ( 𝐴 ∖ { 𝐵 } ) ∩ { 𝐴 } ) ⊆ ( 𝐴 ∩ { 𝐴 } )
14		nnord	⊢ ( 𝐴 ∈ ω → Ord 𝐴 )
15		orddisj	⊢ ( Ord 𝐴 → ( 𝐴 ∩ { 𝐴 } ) = ∅ )
16	14 15	syl	⊢ ( 𝐴 ∈ ω → ( 𝐴 ∩ { 𝐴 } ) = ∅ )
17	13 16	sseqtrid	⊢ ( 𝐴 ∈ ω → ( ( 𝐴 ∖ { 𝐵 } ) ∩ { 𝐴 } ) ⊆ ∅ )
18		ss0	⊢ ( ( ( 𝐴 ∖ { 𝐵 } ) ∩ { 𝐴 } ) ⊆ ∅ → ( ( 𝐴 ∖ { 𝐵 } ) ∩ { 𝐴 } ) = ∅ )
19	17 18	syl	⊢ ( 𝐴 ∈ ω → ( ( 𝐴 ∖ { 𝐵 } ) ∩ { 𝐴 } ) = ∅ )
20	10 19	eqtrid	⊢ ( 𝐴 ∈ ω → ( { 𝐴 } ∩ ( 𝐴 ∖ { 𝐵 } ) ) = ∅ )
21		disjdif	⊢ ( { 𝐵 } ∩ ( 𝐴 ∖ { 𝐵 } ) ) = ∅
22	20 21	jctil	⊢ ( 𝐴 ∈ ω → ( ( { 𝐵 } ∩ ( 𝐴 ∖ { 𝐵 } ) ) = ∅ ∧ ( { 𝐴 } ∩ ( 𝐴 ∖ { 𝐵 } ) ) = ∅ ) )
23		unen	⊢ ( ( ( { 𝐵 } ≈ { 𝐴 } ∧ ( 𝐴 ∖ { 𝐵 } ) ≈ ( 𝐴 ∖ { 𝐵 } ) ) ∧ ( ( { 𝐵 } ∩ ( 𝐴 ∖ { 𝐵 } ) ) = ∅ ∧ ( { 𝐴 } ∩ ( 𝐴 ∖ { 𝐵 } ) ) = ∅ ) ) → ( { 𝐵 } ∪ ( 𝐴 ∖ { 𝐵 } ) ) ≈ ( { 𝐴 } ∪ ( 𝐴 ∖ { 𝐵 } ) ) )
24	9 22 23	sylancr	⊢ ( 𝐴 ∈ ω → ( { 𝐵 } ∪ ( 𝐴 ∖ { 𝐵 } ) ) ≈ ( { 𝐴 } ∪ ( 𝐴 ∖ { 𝐵 } ) ) )
25	24	adantr	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴 ) → ( { 𝐵 } ∪ ( 𝐴 ∖ { 𝐵 } ) ) ≈ ( { 𝐴 } ∪ ( 𝐴 ∖ { 𝐵 } ) ) )
26		uncom	⊢ ( { 𝐵 } ∪ ( 𝐴 ∖ { 𝐵 } ) ) = ( ( 𝐴 ∖ { 𝐵 } ) ∪ { 𝐵 } )
27		difsnid	⊢ ( 𝐵 ∈ 𝐴 → ( ( 𝐴 ∖ { 𝐵 } ) ∪ { 𝐵 } ) = 𝐴 )
28	26 27	eqtrid	⊢ ( 𝐵 ∈ 𝐴 → ( { 𝐵 } ∪ ( 𝐴 ∖ { 𝐵 } ) ) = 𝐴 )
29	28	adantl	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴 ) → ( { 𝐵 } ∪ ( 𝐴 ∖ { 𝐵 } ) ) = 𝐴 )
30		phplem1OLD	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴 ) → ( { 𝐴 } ∪ ( 𝐴 ∖ { 𝐵 } ) ) = ( suc 𝐴 ∖ { 𝐵 } ) )
31	25 29 30	3brtr3d	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴 ) → 𝐴 ≈ ( suc 𝐴 ∖ { 𝐵 } ) )