Theorem phpOLD

Description: Obsolete version of php as of 18-Nov-2024. (Contributed by NM, 29-May-1998) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	phpOLD	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴 ) → ¬ 𝐴 ≈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		0ss	⊢ ∅ ⊆ 𝐵
2		sspsstr	⊢ ( ( ∅ ⊆ 𝐵 ∧ 𝐵 ⊊ 𝐴 ) → ∅ ⊊ 𝐴 )
3	1 2	mpan	⊢ ( 𝐵 ⊊ 𝐴 → ∅ ⊊ 𝐴 )
4		0pss	⊢ ( ∅ ⊊ 𝐴 ↔ 𝐴 ≠ ∅ )
5		df-ne	⊢ ( 𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅ )
6	4 5	bitri	⊢ ( ∅ ⊊ 𝐴 ↔ ¬ 𝐴 = ∅ )
7	3 6	sylib	⊢ ( 𝐵 ⊊ 𝐴 → ¬ 𝐴 = ∅ )
8		nn0suc	⊢ ( 𝐴 ∈ ω → ( 𝐴 = ∅ ∨ ∃ 𝑥 ∈ ω 𝐴 = suc 𝑥 ) )
9	8	orcanai	⊢ ( ( 𝐴 ∈ ω ∧ ¬ 𝐴 = ∅ ) → ∃ 𝑥 ∈ ω 𝐴 = suc 𝑥 )
10	7 9	sylan2	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴 ) → ∃ 𝑥 ∈ ω 𝐴 = suc 𝑥 )
11		pssnel	⊢ ( 𝐵 ⊊ suc 𝑥 → ∃ 𝑦 ( 𝑦 ∈ suc 𝑥 ∧ ¬ 𝑦 ∈ 𝐵 ) )
12		pssss	⊢ ( 𝐵 ⊊ suc 𝑥 → 𝐵 ⊆ suc 𝑥 )
13		ssdif	⊢ ( 𝐵 ⊆ suc 𝑥 → ( 𝐵 ∖ { 𝑦 } ) ⊆ ( suc 𝑥 ∖ { 𝑦 } ) )
14		disjsn	⊢ ( ( 𝐵 ∩ { 𝑦 } ) = ∅ ↔ ¬ 𝑦 ∈ 𝐵 )
15		disj3	⊢ ( ( 𝐵 ∩ { 𝑦 } ) = ∅ ↔ 𝐵 = ( 𝐵 ∖ { 𝑦 } ) )
16	14 15	bitr3i	⊢ ( ¬ 𝑦 ∈ 𝐵 ↔ 𝐵 = ( 𝐵 ∖ { 𝑦 } ) )
17		sseq1	⊢ ( 𝐵 = ( 𝐵 ∖ { 𝑦 } ) → ( 𝐵 ⊆ ( suc 𝑥 ∖ { 𝑦 } ) ↔ ( 𝐵 ∖ { 𝑦 } ) ⊆ ( suc 𝑥 ∖ { 𝑦 } ) ) )
18	16 17	sylbi	⊢ ( ¬ 𝑦 ∈ 𝐵 → ( 𝐵 ⊆ ( suc 𝑥 ∖ { 𝑦 } ) ↔ ( 𝐵 ∖ { 𝑦 } ) ⊆ ( suc 𝑥 ∖ { 𝑦 } ) ) )
19	13 18	syl5ibr	⊢ ( ¬ 𝑦 ∈ 𝐵 → ( 𝐵 ⊆ suc 𝑥 → 𝐵 ⊆ ( suc 𝑥 ∖ { 𝑦 } ) ) )
20		vex	⊢ 𝑥 ∈ V
21	20	sucex	⊢ suc 𝑥 ∈ V
22	21	difexi	⊢ ( suc 𝑥 ∖ { 𝑦 } ) ∈ V
23		ssdomg	⊢ ( ( suc 𝑥 ∖ { 𝑦 } ) ∈ V → ( 𝐵 ⊆ ( suc 𝑥 ∖ { 𝑦 } ) → 𝐵 ≼ ( suc 𝑥 ∖ { 𝑦 } ) ) )
24	22 23	ax-mp	⊢ ( 𝐵 ⊆ ( suc 𝑥 ∖ { 𝑦 } ) → 𝐵 ≼ ( suc 𝑥 ∖ { 𝑦 } ) )
25	12 19 24	syl56	⊢ ( ¬ 𝑦 ∈ 𝐵 → ( 𝐵 ⊊ suc 𝑥 → 𝐵 ≼ ( suc 𝑥 ∖ { 𝑦 } ) ) )
26	25	imp	⊢ ( ( ¬ 𝑦 ∈ 𝐵 ∧ 𝐵 ⊊ suc 𝑥 ) → 𝐵 ≼ ( suc 𝑥 ∖ { 𝑦 } ) )
27		vex	⊢ 𝑦 ∈ V
28	20 27	phplem3OLD	⊢ ( ( 𝑥 ∈ ω ∧ 𝑦 ∈ suc 𝑥 ) → 𝑥 ≈ ( suc 𝑥 ∖ { 𝑦 } ) )
29	28	ensymd	⊢ ( ( 𝑥 ∈ ω ∧ 𝑦 ∈ suc 𝑥 ) → ( suc 𝑥 ∖ { 𝑦 } ) ≈ 𝑥 )
30		domentr	⊢ ( ( 𝐵 ≼ ( suc 𝑥 ∖ { 𝑦 } ) ∧ ( suc 𝑥 ∖ { 𝑦 } ) ≈ 𝑥 ) → 𝐵 ≼ 𝑥 )
31	26 29 30	syl2an	⊢ ( ( ( ¬ 𝑦 ∈ 𝐵 ∧ 𝐵 ⊊ suc 𝑥 ) ∧ ( 𝑥 ∈ ω ∧ 𝑦 ∈ suc 𝑥 ) ) → 𝐵 ≼ 𝑥 )
32	31	exp43	⊢ ( ¬ 𝑦 ∈ 𝐵 → ( 𝐵 ⊊ suc 𝑥 → ( 𝑥 ∈ ω → ( 𝑦 ∈ suc 𝑥 → 𝐵 ≼ 𝑥 ) ) ) )
33	32	com4r	⊢ ( 𝑦 ∈ suc 𝑥 → ( ¬ 𝑦 ∈ 𝐵 → ( 𝐵 ⊊ suc 𝑥 → ( 𝑥 ∈ ω → 𝐵 ≼ 𝑥 ) ) ) )
34	33	imp	⊢ ( ( 𝑦 ∈ suc 𝑥 ∧ ¬ 𝑦 ∈ 𝐵 ) → ( 𝐵 ⊊ suc 𝑥 → ( 𝑥 ∈ ω → 𝐵 ≼ 𝑥 ) ) )
35	34	exlimiv	⊢ ( ∃ 𝑦 ( 𝑦 ∈ suc 𝑥 ∧ ¬ 𝑦 ∈ 𝐵 ) → ( 𝐵 ⊊ suc 𝑥 → ( 𝑥 ∈ ω → 𝐵 ≼ 𝑥 ) ) )
36	11 35	mpcom	⊢ ( 𝐵 ⊊ suc 𝑥 → ( 𝑥 ∈ ω → 𝐵 ≼ 𝑥 ) )
37		endomtr	⊢ ( ( suc 𝑥 ≈ 𝐵 ∧ 𝐵 ≼ 𝑥 ) → suc 𝑥 ≼ 𝑥 )
38		sssucid	⊢ 𝑥 ⊆ suc 𝑥
39		ssdomg	⊢ ( suc 𝑥 ∈ V → ( 𝑥 ⊆ suc 𝑥 → 𝑥 ≼ suc 𝑥 ) )
40	21 38 39	mp2	⊢ 𝑥 ≼ suc 𝑥
41		sbth	⊢ ( ( suc 𝑥 ≼ 𝑥 ∧ 𝑥 ≼ suc 𝑥 ) → suc 𝑥 ≈ 𝑥 )
42	37 40 41	sylancl	⊢ ( ( suc 𝑥 ≈ 𝐵 ∧ 𝐵 ≼ 𝑥 ) → suc 𝑥 ≈ 𝑥 )
43	42	expcom	⊢ ( 𝐵 ≼ 𝑥 → ( suc 𝑥 ≈ 𝐵 → suc 𝑥 ≈ 𝑥 ) )
44		peano2b	⊢ ( 𝑥 ∈ ω ↔ suc 𝑥 ∈ ω )
45		nnord	⊢ ( suc 𝑥 ∈ ω → Ord suc 𝑥 )
46	44 45	sylbi	⊢ ( 𝑥 ∈ ω → Ord suc 𝑥 )
47	20	sucid	⊢ 𝑥 ∈ suc 𝑥
48		nordeq	⊢ ( ( Ord suc 𝑥 ∧ 𝑥 ∈ suc 𝑥 ) → suc 𝑥 ≠ 𝑥 )
49	46 47 48	sylancl	⊢ ( 𝑥 ∈ ω → suc 𝑥 ≠ 𝑥 )
50		nneneqOLD	⊢ ( ( suc 𝑥 ∈ ω ∧ 𝑥 ∈ ω ) → ( suc 𝑥 ≈ 𝑥 ↔ suc 𝑥 = 𝑥 ) )
51	44 50	sylanb	⊢ ( ( 𝑥 ∈ ω ∧ 𝑥 ∈ ω ) → ( suc 𝑥 ≈ 𝑥 ↔ suc 𝑥 = 𝑥 ) )
52	51	anidms	⊢ ( 𝑥 ∈ ω → ( suc 𝑥 ≈ 𝑥 ↔ suc 𝑥 = 𝑥 ) )
53	52	necon3bbid	⊢ ( 𝑥 ∈ ω → ( ¬ suc 𝑥 ≈ 𝑥 ↔ suc 𝑥 ≠ 𝑥 ) )
54	49 53	mpbird	⊢ ( 𝑥 ∈ ω → ¬ suc 𝑥 ≈ 𝑥 )
55	43 54	nsyli	⊢ ( 𝐵 ≼ 𝑥 → ( 𝑥 ∈ ω → ¬ suc 𝑥 ≈ 𝐵 ) )
56	36 55	syli	⊢ ( 𝐵 ⊊ suc 𝑥 → ( 𝑥 ∈ ω → ¬ suc 𝑥 ≈ 𝐵 ) )
57	56	com12	⊢ ( 𝑥 ∈ ω → ( 𝐵 ⊊ suc 𝑥 → ¬ suc 𝑥 ≈ 𝐵 ) )
58		psseq2	⊢ ( 𝐴 = suc 𝑥 → ( 𝐵 ⊊ 𝐴 ↔ 𝐵 ⊊ suc 𝑥 ) )
59		breq1	⊢ ( 𝐴 = suc 𝑥 → ( 𝐴 ≈ 𝐵 ↔ suc 𝑥 ≈ 𝐵 ) )
60	59	notbid	⊢ ( 𝐴 = suc 𝑥 → ( ¬ 𝐴 ≈ 𝐵 ↔ ¬ suc 𝑥 ≈ 𝐵 ) )
61	58 60	imbi12d	⊢ ( 𝐴 = suc 𝑥 → ( ( 𝐵 ⊊ 𝐴 → ¬ 𝐴 ≈ 𝐵 ) ↔ ( 𝐵 ⊊ suc 𝑥 → ¬ suc 𝑥 ≈ 𝐵 ) ) )
62	57 61	syl5ibrcom	⊢ ( 𝑥 ∈ ω → ( 𝐴 = suc 𝑥 → ( 𝐵 ⊊ 𝐴 → ¬ 𝐴 ≈ 𝐵 ) ) )
63	62	rexlimiv	⊢ ( ∃ 𝑥 ∈ ω 𝐴 = suc 𝑥 → ( 𝐵 ⊊ 𝐴 → ¬ 𝐴 ≈ 𝐵 ) )
64	10 63	syl	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴 ) → ( 𝐵 ⊊ 𝐴 → ¬ 𝐴 ≈ 𝐵 ) )
65	64	ex	⊢ ( 𝐴 ∈ ω → ( 𝐵 ⊊ 𝐴 → ( 𝐵 ⊊ 𝐴 → ¬ 𝐴 ≈ 𝐵 ) ) )
66	65	pm2.43d	⊢ ( 𝐴 ∈ ω → ( 𝐵 ⊊ 𝐴 → ¬ 𝐴 ≈ 𝐵 ) )
67	66	imp	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴 ) → ¬ 𝐴 ≈ 𝐵 )