Theorem dflim5

Description: A limit ordinal is either the proper class of ordinals or some nonzero product with omega. (Contributed by RP, 8-Jan-2025)

	Ref	Expression
Assertion	dflim5	⊢ ( Lim 𝐴 ↔ ( 𝐴 = On ∨ ∃ 𝑥 ∈ ( On ∖ 1o ) 𝐴 = ( ω ·o 𝑥 ) ) )

Proof

Step	Hyp	Ref	Expression
1		limord	⊢ ( Lim 𝐴 → Ord 𝐴 )
2		ordeleqon	⊢ ( Ord 𝐴 ↔ ( 𝐴 ∈ On ∨ 𝐴 = On ) )
3	2	biimpi	⊢ ( Ord 𝐴 → ( 𝐴 ∈ On ∨ 𝐴 = On ) )
4	3	orcomd	⊢ ( Ord 𝐴 → ( 𝐴 = On ∨ 𝐴 ∈ On ) )
5	1 4	syl	⊢ ( Lim 𝐴 → ( 𝐴 = On ∨ 𝐴 ∈ On ) )
6	5	pm4.71ri	⊢ ( Lim 𝐴 ↔ ( ( 𝐴 = On ∨ 𝐴 ∈ On ) ∧ Lim 𝐴 ) )
7		andir	⊢ ( ( ( 𝐴 = On ∨ 𝐴 ∈ On ) ∧ Lim 𝐴 ) ↔ ( ( 𝐴 = On ∧ Lim 𝐴 ) ∨ ( 𝐴 ∈ On ∧ Lim 𝐴 ) ) )
8	6 7	bitri	⊢ ( Lim 𝐴 ↔ ( ( 𝐴 = On ∧ Lim 𝐴 ) ∨ ( 𝐴 ∈ On ∧ Lim 𝐴 ) ) )
9		limon	⊢ Lim On
10		limeq	⊢ ( 𝐴 = On → ( Lim 𝐴 ↔ Lim On ) )
11	9 10	mpbiri	⊢ ( 𝐴 = On → Lim 𝐴 )
12	11	pm4.71i	⊢ ( 𝐴 = On ↔ ( 𝐴 = On ∧ Lim 𝐴 ) )
13	12	orbi1i	⊢ ( ( 𝐴 = On ∨ ( 𝐴 ∈ On ∧ Lim 𝐴 ) ) ↔ ( ( 𝐴 = On ∧ Lim 𝐴 ) ∨ ( 𝐴 ∈ On ∧ Lim 𝐴 ) ) )
14		simpl	⊢ ( ( 𝐴 ∈ On ∧ Lim 𝐴 ) → 𝐴 ∈ On )
15		omelon	⊢ ω ∈ On
16	15	a1i	⊢ ( 𝐴 ∈ On → ω ∈ On )
17		id	⊢ ( 𝐴 ∈ On → 𝐴 ∈ On )
18		peano1	⊢ ∅ ∈ ω
19	18	ne0ii	⊢ ω ≠ ∅
20	19	a1i	⊢ ( 𝐴 ∈ On → ω ≠ ∅ )
21	16 17 20	3jca	⊢ ( 𝐴 ∈ On → ( ω ∈ On ∧ 𝐴 ∈ On ∧ ω ≠ ∅ ) )
22		omeulem1	⊢ ( ( ω ∈ On ∧ 𝐴 ∈ On ∧ ω ≠ ∅ ) → ∃ 𝑥 ∈ On ∃ 𝑦 ∈ ω ( ( ω ·o 𝑥 ) +o 𝑦 ) = 𝐴 )
23	14 21 22	3syl	⊢ ( ( 𝐴 ∈ On ∧ Lim 𝐴 ) → ∃ 𝑥 ∈ On ∃ 𝑦 ∈ ω ( ( ω ·o 𝑥 ) +o 𝑦 ) = 𝐴 )
24		limeq	⊢ ( ( ( ω ·o 𝑥 ) +o 𝑦 ) = 𝐴 → ( Lim ( ( ω ·o 𝑥 ) +o 𝑦 ) ↔ Lim 𝐴 ) )
25	24	biimprd	⊢ ( ( ( ω ·o 𝑥 ) +o 𝑦 ) = 𝐴 → ( Lim 𝐴 → Lim ( ( ω ·o 𝑥 ) +o 𝑦 ) ) )
26		simplr	⊢ ( ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) ∧ ¬ ∅ ∈ 𝑥 ) → 𝑦 ∈ ω )
27		nnlim	⊢ ( 𝑦 ∈ ω → ¬ Lim 𝑦 )
28	26 27	syl	⊢ ( ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) ∧ ¬ ∅ ∈ 𝑥 ) → ¬ Lim 𝑦 )
29		on0eln0	⊢ ( 𝑥 ∈ On → ( ∅ ∈ 𝑥 ↔ 𝑥 ≠ ∅ ) )
30	29	biimprd	⊢ ( 𝑥 ∈ On → ( 𝑥 ≠ ∅ → ∅ ∈ 𝑥 ) )
31	30	necon1bd	⊢ ( 𝑥 ∈ On → ( ¬ ∅ ∈ 𝑥 → 𝑥 = ∅ ) )
32	31	adantr	⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) → ( ¬ ∅ ∈ 𝑥 → 𝑥 = ∅ ) )
33	32	imp	⊢ ( ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) ∧ ¬ ∅ ∈ 𝑥 ) → 𝑥 = ∅ )
34	33 26	jca	⊢ ( ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) ∧ ¬ ∅ ∈ 𝑥 ) → ( 𝑥 = ∅ ∧ 𝑦 ∈ ω ) )
35		simpl	⊢ ( ( 𝑥 = ∅ ∧ 𝑦 ∈ ω ) → 𝑥 = ∅ )
36	35	oveq2d	⊢ ( ( 𝑥 = ∅ ∧ 𝑦 ∈ ω ) → ( ω ·o 𝑥 ) = ( ω ·o ∅ ) )
37		om0	⊢ ( ω ∈ On → ( ω ·o ∅ ) = ∅ )
38	15 37	mp1i	⊢ ( ( 𝑥 = ∅ ∧ 𝑦 ∈ ω ) → ( ω ·o ∅ ) = ∅ )
39	36 38	eqtrd	⊢ ( ( 𝑥 = ∅ ∧ 𝑦 ∈ ω ) → ( ω ·o 𝑥 ) = ∅ )
40	39	oveq1d	⊢ ( ( 𝑥 = ∅ ∧ 𝑦 ∈ ω ) → ( ( ω ·o 𝑥 ) +o 𝑦 ) = ( ∅ +o 𝑦 ) )
41		nna0r	⊢ ( 𝑦 ∈ ω → ( ∅ +o 𝑦 ) = 𝑦 )
42	41	adantl	⊢ ( ( 𝑥 = ∅ ∧ 𝑦 ∈ ω ) → ( ∅ +o 𝑦 ) = 𝑦 )
43	40 42	eqtrd	⊢ ( ( 𝑥 = ∅ ∧ 𝑦 ∈ ω ) → ( ( ω ·o 𝑥 ) +o 𝑦 ) = 𝑦 )
44		limeq	⊢ ( ( ( ω ·o 𝑥 ) +o 𝑦 ) = 𝑦 → ( Lim ( ( ω ·o 𝑥 ) +o 𝑦 ) ↔ Lim 𝑦 ) )
45	34 43 44	3syl	⊢ ( ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) ∧ ¬ ∅ ∈ 𝑥 ) → ( Lim ( ( ω ·o 𝑥 ) +o 𝑦 ) ↔ Lim 𝑦 ) )
46	28 45	mtbird	⊢ ( ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) ∧ ¬ ∅ ∈ 𝑥 ) → ¬ Lim ( ( ω ·o 𝑥 ) +o 𝑦 ) )
47	46	ex	⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) → ( ¬ ∅ ∈ 𝑥 → ¬ Lim ( ( ω ·o 𝑥 ) +o 𝑦 ) ) )
48		ovex	⊢ ( ( ω ·o 𝑥 ) +o ∪ 𝑦 ) ∈ V
49		nlimsucg	⊢ ( ( ( ω ·o 𝑥 ) +o ∪ 𝑦 ) ∈ V → ¬ Lim suc ( ( ω ·o 𝑥 ) +o ∪ 𝑦 ) )
50	48 49	mp1i	⊢ ( ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) ∧ ¬ 𝑦 = ∅ ) → ¬ Lim suc ( ( ω ·o 𝑥 ) +o ∪ 𝑦 ) )
51		nnord	⊢ ( 𝑦 ∈ ω → Ord 𝑦 )
52		orduniorsuc	⊢ ( Ord 𝑦 → ( 𝑦 = ∪ 𝑦 ∨ 𝑦 = suc ∪ 𝑦 ) )
53	51 52	syl	⊢ ( 𝑦 ∈ ω → ( 𝑦 = ∪ 𝑦 ∨ 𝑦 = suc ∪ 𝑦 ) )
54		3ianor	⊢ ( ¬ ( Ord 𝑦 ∧ 𝑦 ≠ ∅ ∧ 𝑦 = ∪ 𝑦 ) ↔ ( ¬ Ord 𝑦 ∨ ¬ 𝑦 ≠ ∅ ∨ ¬ 𝑦 = ∪ 𝑦 ) )
55		df-lim	⊢ ( Lim 𝑦 ↔ ( Ord 𝑦 ∧ 𝑦 ≠ ∅ ∧ 𝑦 = ∪ 𝑦 ) )
56	54 55	xchnxbir	⊢ ( ¬ Lim 𝑦 ↔ ( ¬ Ord 𝑦 ∨ ¬ 𝑦 ≠ ∅ ∨ ¬ 𝑦 = ∪ 𝑦 ) )
57	27 56	sylib	⊢ ( 𝑦 ∈ ω → ( ¬ Ord 𝑦 ∨ ¬ 𝑦 ≠ ∅ ∨ ¬ 𝑦 = ∪ 𝑦 ) )
58	51	pm2.24d	⊢ ( 𝑦 ∈ ω → ( ¬ Ord 𝑦 → ( 𝑦 = ∪ 𝑦 → 𝑦 = ∅ ) ) )
59		nne	⊢ ( ¬ 𝑦 ≠ ∅ ↔ 𝑦 = ∅ )
60	59	biimpi	⊢ ( ¬ 𝑦 ≠ ∅ → 𝑦 = ∅ )
61	60	a1i13	⊢ ( 𝑦 ∈ ω → ( ¬ 𝑦 ≠ ∅ → ( 𝑦 = ∪ 𝑦 → 𝑦 = ∅ ) ) )
62		pm2.21	⊢ ( ¬ 𝑦 = ∪ 𝑦 → ( 𝑦 = ∪ 𝑦 → 𝑦 = ∅ ) )
63	62	a1i	⊢ ( 𝑦 ∈ ω → ( ¬ 𝑦 = ∪ 𝑦 → ( 𝑦 = ∪ 𝑦 → 𝑦 = ∅ ) ) )
64	58 61 63	3jaod	⊢ ( 𝑦 ∈ ω → ( ( ¬ Ord 𝑦 ∨ ¬ 𝑦 ≠ ∅ ∨ ¬ 𝑦 = ∪ 𝑦 ) → ( 𝑦 = ∪ 𝑦 → 𝑦 = ∅ ) ) )
65	57 64	mpd	⊢ ( 𝑦 ∈ ω → ( 𝑦 = ∪ 𝑦 → 𝑦 = ∅ ) )
66	65	orim1d	⊢ ( 𝑦 ∈ ω → ( ( 𝑦 = ∪ 𝑦 ∨ 𝑦 = suc ∪ 𝑦 ) → ( 𝑦 = ∅ ∨ 𝑦 = suc ∪ 𝑦 ) ) )
67	53 66	mpd	⊢ ( 𝑦 ∈ ω → ( 𝑦 = ∅ ∨ 𝑦 = suc ∪ 𝑦 ) )
68	67	ord	⊢ ( 𝑦 ∈ ω → ( ¬ 𝑦 = ∅ → 𝑦 = suc ∪ 𝑦 ) )
69	68	adantl	⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) → ( ¬ 𝑦 = ∅ → 𝑦 = suc ∪ 𝑦 ) )
70	69	imp	⊢ ( ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) ∧ ¬ 𝑦 = ∅ ) → 𝑦 = suc ∪ 𝑦 )
71	70	oveq2d	⊢ ( ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) ∧ ¬ 𝑦 = ∅ ) → ( ( ω ·o 𝑥 ) +o 𝑦 ) = ( ( ω ·o 𝑥 ) +o suc ∪ 𝑦 ) )
72		simpl	⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) → 𝑥 ∈ On )
73	72	adantr	⊢ ( ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) ∧ ¬ 𝑦 = ∅ ) → 𝑥 ∈ On )
74		omcl	⊢ ( ( ω ∈ On ∧ 𝑥 ∈ On ) → ( ω ·o 𝑥 ) ∈ On )
75	15 73 74	sylancr	⊢ ( ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) ∧ ¬ 𝑦 = ∅ ) → ( ω ·o 𝑥 ) ∈ On )
76		nnon	⊢ ( 𝑦 ∈ ω → 𝑦 ∈ On )
77		onuni	⊢ ( 𝑦 ∈ On → ∪ 𝑦 ∈ On )
78	76 77	syl	⊢ ( 𝑦 ∈ ω → ∪ 𝑦 ∈ On )
79	78	adantl	⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) → ∪ 𝑦 ∈ On )
80	79	adantr	⊢ ( ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) ∧ ¬ 𝑦 = ∅ ) → ∪ 𝑦 ∈ On )
81		oasuc	⊢ ( ( ( ω ·o 𝑥 ) ∈ On ∧ ∪ 𝑦 ∈ On ) → ( ( ω ·o 𝑥 ) +o suc ∪ 𝑦 ) = suc ( ( ω ·o 𝑥 ) +o ∪ 𝑦 ) )
82	75 80 81	syl2anc	⊢ ( ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) ∧ ¬ 𝑦 = ∅ ) → ( ( ω ·o 𝑥 ) +o suc ∪ 𝑦 ) = suc ( ( ω ·o 𝑥 ) +o ∪ 𝑦 ) )
83	71 82	eqtrd	⊢ ( ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) ∧ ¬ 𝑦 = ∅ ) → ( ( ω ·o 𝑥 ) +o 𝑦 ) = suc ( ( ω ·o 𝑥 ) +o ∪ 𝑦 ) )
84		limeq	⊢ ( ( ( ω ·o 𝑥 ) +o 𝑦 ) = suc ( ( ω ·o 𝑥 ) +o ∪ 𝑦 ) → ( Lim ( ( ω ·o 𝑥 ) +o 𝑦 ) ↔ Lim suc ( ( ω ·o 𝑥 ) +o ∪ 𝑦 ) ) )
85	83 84	syl	⊢ ( ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) ∧ ¬ 𝑦 = ∅ ) → ( Lim ( ( ω ·o 𝑥 ) +o 𝑦 ) ↔ Lim suc ( ( ω ·o 𝑥 ) +o ∪ 𝑦 ) ) )
86	50 85	mtbird	⊢ ( ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) ∧ ¬ 𝑦 = ∅ ) → ¬ Lim ( ( ω ·o 𝑥 ) +o 𝑦 ) )
87	86	ex	⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) → ( ¬ 𝑦 = ∅ → ¬ Lim ( ( ω ·o 𝑥 ) +o 𝑦 ) ) )
88	47 87	jaod	⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) → ( ( ¬ ∅ ∈ 𝑥 ∨ ¬ 𝑦 = ∅ ) → ¬ Lim ( ( ω ·o 𝑥 ) +o 𝑦 ) ) )
89	88	con2d	⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) → ( Lim ( ( ω ·o 𝑥 ) +o 𝑦 ) → ¬ ( ¬ ∅ ∈ 𝑥 ∨ ¬ 𝑦 = ∅ ) ) )
90		anor	⊢ ( ( ∅ ∈ 𝑥 ∧ 𝑦 = ∅ ) ↔ ¬ ( ¬ ∅ ∈ 𝑥 ∨ ¬ 𝑦 = ∅ ) )
91	89 90	imbitrrdi	⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) → ( Lim ( ( ω ·o 𝑥 ) +o 𝑦 ) → ( ∅ ∈ 𝑥 ∧ 𝑦 = ∅ ) ) )
92	25 91	syl9	⊢ ( ( ( ω ·o 𝑥 ) +o 𝑦 ) = 𝐴 → ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) → ( Lim 𝐴 → ( ∅ ∈ 𝑥 ∧ 𝑦 = ∅ ) ) ) )
93	92	com13	⊢ ( Lim 𝐴 → ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) → ( ( ( ω ·o 𝑥 ) +o 𝑦 ) = 𝐴 → ( ∅ ∈ 𝑥 ∧ 𝑦 = ∅ ) ) ) )
94	93	adantl	⊢ ( ( 𝐴 ∈ On ∧ Lim 𝐴 ) → ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) → ( ( ( ω ·o 𝑥 ) +o 𝑦 ) = 𝐴 → ( ∅ ∈ 𝑥 ∧ 𝑦 = ∅ ) ) ) )
95	94	3imp	⊢ ( ( ( 𝐴 ∈ On ∧ Lim 𝐴 ) ∧ ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) ∧ ( ( ω ·o 𝑥 ) +o 𝑦 ) = 𝐴 ) → ( ∅ ∈ 𝑥 ∧ 𝑦 = ∅ ) )
96		simp2	⊢ ( ( ( 𝐴 ∈ On ∧ Lim 𝐴 ) ∧ ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) ∧ ( ( ω ·o 𝑥 ) +o 𝑦 ) = 𝐴 ) → ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) )
97	96 72	syl	⊢ ( ( ( 𝐴 ∈ On ∧ Lim 𝐴 ) ∧ ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) ∧ ( ( ω ·o 𝑥 ) +o 𝑦 ) = 𝐴 ) → 𝑥 ∈ On )
98		simpl	⊢ ( ( ∅ ∈ 𝑥 ∧ 𝑦 = ∅ ) → ∅ ∈ 𝑥 )
99	97 98	anim12i	⊢ ( ( ( ( 𝐴 ∈ On ∧ Lim 𝐴 ) ∧ ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) ∧ ( ( ω ·o 𝑥 ) +o 𝑦 ) = 𝐴 ) ∧ ( ∅ ∈ 𝑥 ∧ 𝑦 = ∅ ) ) → ( 𝑥 ∈ On ∧ ∅ ∈ 𝑥 ) )
100		ondif1	⊢ ( 𝑥 ∈ ( On ∖ 1o ) ↔ ( 𝑥 ∈ On ∧ ∅ ∈ 𝑥 ) )
101	99 100	sylibr	⊢ ( ( ( ( 𝐴 ∈ On ∧ Lim 𝐴 ) ∧ ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) ∧ ( ( ω ·o 𝑥 ) +o 𝑦 ) = 𝐴 ) ∧ ( ∅ ∈ 𝑥 ∧ 𝑦 = ∅ ) ) → 𝑥 ∈ ( On ∖ 1o ) )
102		simpr	⊢ ( ( ∅ ∈ 𝑥 ∧ 𝑦 = ∅ ) → 𝑦 = ∅ )
103	102	oveq2d	⊢ ( ( ∅ ∈ 𝑥 ∧ 𝑦 = ∅ ) → ( ( ω ·o 𝑥 ) +o 𝑦 ) = ( ( ω ·o 𝑥 ) +o ∅ ) )
104	103	adantl	⊢ ( ( ( ( 𝐴 ∈ On ∧ Lim 𝐴 ) ∧ ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) ∧ ( ( ω ·o 𝑥 ) +o 𝑦 ) = 𝐴 ) ∧ ( ∅ ∈ 𝑥 ∧ 𝑦 = ∅ ) ) → ( ( ω ·o 𝑥 ) +o 𝑦 ) = ( ( ω ·o 𝑥 ) +o ∅ ) )
105		simpl3	⊢ ( ( ( ( 𝐴 ∈ On ∧ Lim 𝐴 ) ∧ ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) ∧ ( ( ω ·o 𝑥 ) +o 𝑦 ) = 𝐴 ) ∧ ( ∅ ∈ 𝑥 ∧ 𝑦 = ∅ ) ) → ( ( ω ·o 𝑥 ) +o 𝑦 ) = 𝐴 )
106	15 72 74	sylancr	⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) → ( ω ·o 𝑥 ) ∈ On )
107		oa0	⊢ ( ( ω ·o 𝑥 ) ∈ On → ( ( ω ·o 𝑥 ) +o ∅ ) = ( ω ·o 𝑥 ) )
108	96 106 107	3syl	⊢ ( ( ( 𝐴 ∈ On ∧ Lim 𝐴 ) ∧ ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) ∧ ( ( ω ·o 𝑥 ) +o 𝑦 ) = 𝐴 ) → ( ( ω ·o 𝑥 ) +o ∅ ) = ( ω ·o 𝑥 ) )
109	108	adantr	⊢ ( ( ( ( 𝐴 ∈ On ∧ Lim 𝐴 ) ∧ ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) ∧ ( ( ω ·o 𝑥 ) +o 𝑦 ) = 𝐴 ) ∧ ( ∅ ∈ 𝑥 ∧ 𝑦 = ∅ ) ) → ( ( ω ·o 𝑥 ) +o ∅ ) = ( ω ·o 𝑥 ) )
110	104 105 109	3eqtr3d	⊢ ( ( ( ( 𝐴 ∈ On ∧ Lim 𝐴 ) ∧ ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) ∧ ( ( ω ·o 𝑥 ) +o 𝑦 ) = 𝐴 ) ∧ ( ∅ ∈ 𝑥 ∧ 𝑦 = ∅ ) ) → 𝐴 = ( ω ·o 𝑥 ) )
111	101 110	jca	⊢ ( ( ( ( 𝐴 ∈ On ∧ Lim 𝐴 ) ∧ ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) ∧ ( ( ω ·o 𝑥 ) +o 𝑦 ) = 𝐴 ) ∧ ( ∅ ∈ 𝑥 ∧ 𝑦 = ∅ ) ) → ( 𝑥 ∈ ( On ∖ 1o ) ∧ 𝐴 = ( ω ·o 𝑥 ) ) )
112	95 111	mpdan	⊢ ( ( ( 𝐴 ∈ On ∧ Lim 𝐴 ) ∧ ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) ∧ ( ( ω ·o 𝑥 ) +o 𝑦 ) = 𝐴 ) → ( 𝑥 ∈ ( On ∖ 1o ) ∧ 𝐴 = ( ω ·o 𝑥 ) ) )
113	112	3exp	⊢ ( ( 𝐴 ∈ On ∧ Lim 𝐴 ) → ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) → ( ( ( ω ·o 𝑥 ) +o 𝑦 ) = 𝐴 → ( 𝑥 ∈ ( On ∖ 1o ) ∧ 𝐴 = ( ω ·o 𝑥 ) ) ) ) )
114	113	expdimp	⊢ ( ( ( 𝐴 ∈ On ∧ Lim 𝐴 ) ∧ 𝑥 ∈ On ) → ( 𝑦 ∈ ω → ( ( ( ω ·o 𝑥 ) +o 𝑦 ) = 𝐴 → ( 𝑥 ∈ ( On ∖ 1o ) ∧ 𝐴 = ( ω ·o 𝑥 ) ) ) ) )
115	114	rexlimdv	⊢ ( ( ( 𝐴 ∈ On ∧ Lim 𝐴 ) ∧ 𝑥 ∈ On ) → ( ∃ 𝑦 ∈ ω ( ( ω ·o 𝑥 ) +o 𝑦 ) = 𝐴 → ( 𝑥 ∈ ( On ∖ 1o ) ∧ 𝐴 = ( ω ·o 𝑥 ) ) ) )
116	115	expimpd	⊢ ( ( 𝐴 ∈ On ∧ Lim 𝐴 ) → ( ( 𝑥 ∈ On ∧ ∃ 𝑦 ∈ ω ( ( ω ·o 𝑥 ) +o 𝑦 ) = 𝐴 ) → ( 𝑥 ∈ ( On ∖ 1o ) ∧ 𝐴 = ( ω ·o 𝑥 ) ) ) )
117	116	reximdv2	⊢ ( ( 𝐴 ∈ On ∧ Lim 𝐴 ) → ( ∃ 𝑥 ∈ On ∃ 𝑦 ∈ ω ( ( ω ·o 𝑥 ) +o 𝑦 ) = 𝐴 → ∃ 𝑥 ∈ ( On ∖ 1o ) 𝐴 = ( ω ·o 𝑥 ) ) )
118	23 117	mpd	⊢ ( ( 𝐴 ∈ On ∧ Lim 𝐴 ) → ∃ 𝑥 ∈ ( On ∖ 1o ) 𝐴 = ( ω ·o 𝑥 ) )
119		simpr	⊢ ( ( 𝑥 ∈ ( On ∖ 1o ) ∧ 𝐴 = ( ω ·o 𝑥 ) ) → 𝐴 = ( ω ·o 𝑥 ) )
120		eldifi	⊢ ( 𝑥 ∈ ( On ∖ 1o ) → 𝑥 ∈ On )
121	15 120 74	sylancr	⊢ ( 𝑥 ∈ ( On ∖ 1o ) → ( ω ·o 𝑥 ) ∈ On )
122	121	adantr	⊢ ( ( 𝑥 ∈ ( On ∖ 1o ) ∧ 𝐴 = ( ω ·o 𝑥 ) ) → ( ω ·o 𝑥 ) ∈ On )
123	119 122	eqeltrd	⊢ ( ( 𝑥 ∈ ( On ∖ 1o ) ∧ 𝐴 = ( ω ·o 𝑥 ) ) → 𝐴 ∈ On )
124		limom	⊢ Lim ω
125	15 124	pm3.2i	⊢ ( ω ∈ On ∧ Lim ω )
126		omlimcl2	⊢ ( ( ( 𝑥 ∈ On ∧ ( ω ∈ On ∧ Lim ω ) ) ∧ ∅ ∈ 𝑥 ) → Lim ( ω ·o 𝑥 ) )
127	125 126	mpanl2	⊢ ( ( 𝑥 ∈ On ∧ ∅ ∈ 𝑥 ) → Lim ( ω ·o 𝑥 ) )
128	100 127	sylbi	⊢ ( 𝑥 ∈ ( On ∖ 1o ) → Lim ( ω ·o 𝑥 ) )
129	128	adantr	⊢ ( ( 𝑥 ∈ ( On ∖ 1o ) ∧ 𝐴 = ( ω ·o 𝑥 ) ) → Lim ( ω ·o 𝑥 ) )
130		limeq	⊢ ( 𝐴 = ( ω ·o 𝑥 ) → ( Lim 𝐴 ↔ Lim ( ω ·o 𝑥 ) ) )
131	130	adantl	⊢ ( ( 𝑥 ∈ ( On ∖ 1o ) ∧ 𝐴 = ( ω ·o 𝑥 ) ) → ( Lim 𝐴 ↔ Lim ( ω ·o 𝑥 ) ) )
132	129 131	mpbird	⊢ ( ( 𝑥 ∈ ( On ∖ 1o ) ∧ 𝐴 = ( ω ·o 𝑥 ) ) → Lim 𝐴 )
133	123 132	jca	⊢ ( ( 𝑥 ∈ ( On ∖ 1o ) ∧ 𝐴 = ( ω ·o 𝑥 ) ) → ( 𝐴 ∈ On ∧ Lim 𝐴 ) )
134	133	rexlimiva	⊢ ( ∃ 𝑥 ∈ ( On ∖ 1o ) 𝐴 = ( ω ·o 𝑥 ) → ( 𝐴 ∈ On ∧ Lim 𝐴 ) )
135	118 134	impbii	⊢ ( ( 𝐴 ∈ On ∧ Lim 𝐴 ) ↔ ∃ 𝑥 ∈ ( On ∖ 1o ) 𝐴 = ( ω ·o 𝑥 ) )
136	135	orbi2i	⊢ ( ( 𝐴 = On ∨ ( 𝐴 ∈ On ∧ Lim 𝐴 ) ) ↔ ( 𝐴 = On ∨ ∃ 𝑥 ∈ ( On ∖ 1o ) 𝐴 = ( ω ·o 𝑥 ) ) )
137	8 13 136	3bitr2i	⊢ ( Lim 𝐴 ↔ ( 𝐴 = On ∨ ∃ 𝑥 ∈ ( On ∖ 1o ) 𝐴 = ( ω ·o 𝑥 ) ) )