Theorem limsssuc

Description: A class includes a limit ordinal iff the successor of the class includes it. (Contributed by NM, 30-Oct-2003)

	Ref	Expression
Assertion	limsssuc	⊢ ( Lim 𝐴 → ( 𝐴 ⊆ 𝐵 ↔ 𝐴 ⊆ suc 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		sssucid	⊢ 𝐵 ⊆ suc 𝐵
2		sstr2	⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐵 ⊆ suc 𝐵 → 𝐴 ⊆ suc 𝐵 ) )
3	1 2	mpi	⊢ ( 𝐴 ⊆ 𝐵 → 𝐴 ⊆ suc 𝐵 )
4		eleq1	⊢ ( 𝑥 = 𝐵 → ( 𝑥 ∈ 𝐴 ↔ 𝐵 ∈ 𝐴 ) )
5	4	biimpcd	⊢ ( 𝑥 ∈ 𝐴 → ( 𝑥 = 𝐵 → 𝐵 ∈ 𝐴 ) )
6		limsuc	⊢ ( Lim 𝐴 → ( 𝐵 ∈ 𝐴 ↔ suc 𝐵 ∈ 𝐴 ) )
7	6	biimpa	⊢ ( ( Lim 𝐴 ∧ 𝐵 ∈ 𝐴 ) → suc 𝐵 ∈ 𝐴 )
8		limord	⊢ ( Lim 𝐴 → Ord 𝐴 )
9		ordelord	⊢ ( ( Ord 𝐴 ∧ 𝐵 ∈ 𝐴 ) → Ord 𝐵 )
10	8 9	sylan	⊢ ( ( Lim 𝐴 ∧ 𝐵 ∈ 𝐴 ) → Ord 𝐵 )
11		ordsuc	⊢ ( Ord 𝐵 ↔ Ord suc 𝐵 )
12	10 11	sylib	⊢ ( ( Lim 𝐴 ∧ 𝐵 ∈ 𝐴 ) → Ord suc 𝐵 )
13		ordtri1	⊢ ( ( Ord 𝐴 ∧ Ord suc 𝐵 ) → ( 𝐴 ⊆ suc 𝐵 ↔ ¬ suc 𝐵 ∈ 𝐴 ) )
14	8 12 13	syl2an2r	⊢ ( ( Lim 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( 𝐴 ⊆ suc 𝐵 ↔ ¬ suc 𝐵 ∈ 𝐴 ) )
15	14	con2bid	⊢ ( ( Lim 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( suc 𝐵 ∈ 𝐴 ↔ ¬ 𝐴 ⊆ suc 𝐵 ) )
16	7 15	mpbid	⊢ ( ( Lim 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ¬ 𝐴 ⊆ suc 𝐵 )
17	16	ex	⊢ ( Lim 𝐴 → ( 𝐵 ∈ 𝐴 → ¬ 𝐴 ⊆ suc 𝐵 ) )
18	5 17	sylan9r	⊢ ( ( Lim 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 = 𝐵 → ¬ 𝐴 ⊆ suc 𝐵 ) )
19	18	con2d	⊢ ( ( Lim 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐴 ⊆ suc 𝐵 → ¬ 𝑥 = 𝐵 ) )
20	19	ex	⊢ ( Lim 𝐴 → ( 𝑥 ∈ 𝐴 → ( 𝐴 ⊆ suc 𝐵 → ¬ 𝑥 = 𝐵 ) ) )
21	20	com23	⊢ ( Lim 𝐴 → ( 𝐴 ⊆ suc 𝐵 → ( 𝑥 ∈ 𝐴 → ¬ 𝑥 = 𝐵 ) ) )
22	21	imp31	⊢ ( ( ( Lim 𝐴 ∧ 𝐴 ⊆ suc 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ¬ 𝑥 = 𝐵 )
23		ssel2	⊢ ( ( 𝐴 ⊆ suc 𝐵 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ suc 𝐵 )
24		vex	⊢ 𝑥 ∈ V
25	24	elsuc	⊢ ( 𝑥 ∈ suc 𝐵 ↔ ( 𝑥 ∈ 𝐵 ∨ 𝑥 = 𝐵 ) )
26	23 25	sylib	⊢ ( ( 𝐴 ⊆ suc 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ∈ 𝐵 ∨ 𝑥 = 𝐵 ) )
27	26	ord	⊢ ( ( 𝐴 ⊆ suc 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ( ¬ 𝑥 ∈ 𝐵 → 𝑥 = 𝐵 ) )
28	27	con1d	⊢ ( ( 𝐴 ⊆ suc 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ( ¬ 𝑥 = 𝐵 → 𝑥 ∈ 𝐵 ) )
29	28	adantll	⊢ ( ( ( Lim 𝐴 ∧ 𝐴 ⊆ suc 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( ¬ 𝑥 = 𝐵 → 𝑥 ∈ 𝐵 ) )
30	22 29	mpd	⊢ ( ( ( Lim 𝐴 ∧ 𝐴 ⊆ suc 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐵 )
31	30	ex	⊢ ( ( Lim 𝐴 ∧ 𝐴 ⊆ suc 𝐵 ) → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) )
32	31	ssrdv	⊢ ( ( Lim 𝐴 ∧ 𝐴 ⊆ suc 𝐵 ) → 𝐴 ⊆ 𝐵 )
33	32	ex	⊢ ( Lim 𝐴 → ( 𝐴 ⊆ suc 𝐵 → 𝐴 ⊆ 𝐵 ) )
34	3 33	impbid2	⊢ ( Lim 𝐴 → ( 𝐴 ⊆ 𝐵 ↔ 𝐴 ⊆ suc 𝐵 ) )