Theorem onexomgt

Description: For any ordinal, there is always a larger product of omega. (Contributed by RP, 1-Feb-2025)

	Ref	Expression
Assertion	onexomgt	⊢ ( 𝐴 ∈ On → ∃ 𝑥 ∈ On 𝐴 ∈ ( ω ·o 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		omelon	⊢ ω ∈ On
2		peano1	⊢ ∅ ∈ ω
3	2	ne0ii	⊢ ω ≠ ∅
4		omeu	⊢ ( ( ω ∈ On ∧ 𝐴 ∈ On ∧ ω ≠ ∅ ) → ∃! 𝑐 ∃ 𝑎 ∈ On ∃ 𝑏 ∈ ω ( 𝑐 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( ( ω ·o 𝑎 ) +o 𝑏 ) = 𝐴 ) )
5	1 3 4	mp3an13	⊢ ( 𝐴 ∈ On → ∃! 𝑐 ∃ 𝑎 ∈ On ∃ 𝑏 ∈ ω ( 𝑐 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( ( ω ·o 𝑎 ) +o 𝑏 ) = 𝐴 ) )
6		euex	⊢ ( ∃! 𝑐 ∃ 𝑎 ∈ On ∃ 𝑏 ∈ ω ( 𝑐 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( ( ω ·o 𝑎 ) +o 𝑏 ) = 𝐴 ) → ∃ 𝑐 ∃ 𝑎 ∈ On ∃ 𝑏 ∈ ω ( 𝑐 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( ( ω ·o 𝑎 ) +o 𝑏 ) = 𝐴 ) )
7		onsuc	⊢ ( 𝑎 ∈ On → suc 𝑎 ∈ On )
8	7	adantr	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ ω ) → suc 𝑎 ∈ On )
9		simpr	⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ ω ) ∧ ( ( ω ·o 𝑎 ) +o 𝑏 ) = 𝐴 ) → ( ( ω ·o 𝑎 ) +o 𝑏 ) = 𝐴 )
10		simpr	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ ω ) → 𝑏 ∈ ω )
11		simpl	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ ω ) → 𝑎 ∈ On )
12		omcl	⊢ ( ( ω ∈ On ∧ 𝑎 ∈ On ) → ( ω ·o 𝑎 ) ∈ On )
13	1 11 12	sylancr	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ ω ) → ( ω ·o 𝑎 ) ∈ On )
14		oaordi	⊢ ( ( ω ∈ On ∧ ( ω ·o 𝑎 ) ∈ On ) → ( 𝑏 ∈ ω → ( ( ω ·o 𝑎 ) +o 𝑏 ) ∈ ( ( ω ·o 𝑎 ) +o ω ) ) )
15	1 13 14	sylancr	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ ω ) → ( 𝑏 ∈ ω → ( ( ω ·o 𝑎 ) +o 𝑏 ) ∈ ( ( ω ·o 𝑎 ) +o ω ) ) )
16	10 15	mpd	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ ω ) → ( ( ω ·o 𝑎 ) +o 𝑏 ) ∈ ( ( ω ·o 𝑎 ) +o ω ) )
17		omsuc	⊢ ( ( ω ∈ On ∧ 𝑎 ∈ On ) → ( ω ·o suc 𝑎 ) = ( ( ω ·o 𝑎 ) +o ω ) )
18	1 11 17	sylancr	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ ω ) → ( ω ·o suc 𝑎 ) = ( ( ω ·o 𝑎 ) +o ω ) )
19	16 18	eleqtrrd	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ ω ) → ( ( ω ·o 𝑎 ) +o 𝑏 ) ∈ ( ω ·o suc 𝑎 ) )
20	19	adantr	⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ ω ) ∧ ( ( ω ·o 𝑎 ) +o 𝑏 ) = 𝐴 ) → ( ( ω ·o 𝑎 ) +o 𝑏 ) ∈ ( ω ·o suc 𝑎 ) )
21	9 20	eqeltrrd	⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ ω ) ∧ ( ( ω ·o 𝑎 ) +o 𝑏 ) = 𝐴 ) → 𝐴 ∈ ( ω ·o suc 𝑎 ) )
22		oveq2	⊢ ( 𝑥 = suc 𝑎 → ( ω ·o 𝑥 ) = ( ω ·o suc 𝑎 ) )
23	22	eleq2d	⊢ ( 𝑥 = suc 𝑎 → ( 𝐴 ∈ ( ω ·o 𝑥 ) ↔ 𝐴 ∈ ( ω ·o suc 𝑎 ) ) )
24	23	rspcev	⊢ ( ( suc 𝑎 ∈ On ∧ 𝐴 ∈ ( ω ·o suc 𝑎 ) ) → ∃ 𝑥 ∈ On 𝐴 ∈ ( ω ·o 𝑥 ) )
25	8 21 24	syl2an2r	⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ ω ) ∧ ( ( ω ·o 𝑎 ) +o 𝑏 ) = 𝐴 ) → ∃ 𝑥 ∈ On 𝐴 ∈ ( ω ·o 𝑥 ) )
26	25	ex	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ ω ) → ( ( ( ω ·o 𝑎 ) +o 𝑏 ) = 𝐴 → ∃ 𝑥 ∈ On 𝐴 ∈ ( ω ·o 𝑥 ) ) )
27	26	adantld	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ ω ) → ( ( 𝑐 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( ( ω ·o 𝑎 ) +o 𝑏 ) = 𝐴 ) → ∃ 𝑥 ∈ On 𝐴 ∈ ( ω ·o 𝑥 ) ) )
28	27	a1i	⊢ ( 𝐴 ∈ On → ( ( 𝑎 ∈ On ∧ 𝑏 ∈ ω ) → ( ( 𝑐 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( ( ω ·o 𝑎 ) +o 𝑏 ) = 𝐴 ) → ∃ 𝑥 ∈ On 𝐴 ∈ ( ω ·o 𝑥 ) ) ) )
29	28	rexlimdvv	⊢ ( 𝐴 ∈ On → ( ∃ 𝑎 ∈ On ∃ 𝑏 ∈ ω ( 𝑐 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( ( ω ·o 𝑎 ) +o 𝑏 ) = 𝐴 ) → ∃ 𝑥 ∈ On 𝐴 ∈ ( ω ·o 𝑥 ) ) )
30	29	exlimdv	⊢ ( 𝐴 ∈ On → ( ∃ 𝑐 ∃ 𝑎 ∈ On ∃ 𝑏 ∈ ω ( 𝑐 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( ( ω ·o 𝑎 ) +o 𝑏 ) = 𝐴 ) → ∃ 𝑥 ∈ On 𝐴 ∈ ( ω ·o 𝑥 ) ) )
31	6 30	syl5	⊢ ( 𝐴 ∈ On → ( ∃! 𝑐 ∃ 𝑎 ∈ On ∃ 𝑏 ∈ ω ( 𝑐 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( ( ω ·o 𝑎 ) +o 𝑏 ) = 𝐴 ) → ∃ 𝑥 ∈ On 𝐴 ∈ ( ω ·o 𝑥 ) ) )
32	5 31	mpd	⊢ ( 𝐴 ∈ On → ∃ 𝑥 ∈ On 𝐴 ∈ ( ω ·o 𝑥 ) )