Metamath Proof Explorer


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 𝐵 ) )