Theorem limuni3

Description: The union of a nonempty class of limit ordinals is a limit ordinal. (Contributed by NM, 1-Feb-2005)

	Ref	Expression
Assertion	limuni3	⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 Lim 𝑥 ) → Lim ∪ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		limeq	⊢ ( 𝑥 = 𝑧 → ( Lim 𝑥 ↔ Lim 𝑧 ) )
2	1	rspcv	⊢ ( 𝑧 ∈ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 Lim 𝑥 → Lim 𝑧 ) )
3		vex	⊢ 𝑧 ∈ V
4		limelon	⊢ ( ( 𝑧 ∈ V ∧ Lim 𝑧 ) → 𝑧 ∈ On )
5	3 4	mpan	⊢ ( Lim 𝑧 → 𝑧 ∈ On )
6	2 5	syl6com	⊢ ( ∀ 𝑥 ∈ 𝐴 Lim 𝑥 → ( 𝑧 ∈ 𝐴 → 𝑧 ∈ On ) )
7	6	ssrdv	⊢ ( ∀ 𝑥 ∈ 𝐴 Lim 𝑥 → 𝐴 ⊆ On )
8		ssorduni	⊢ ( 𝐴 ⊆ On → Ord ∪ 𝐴 )
9	7 8	syl	⊢ ( ∀ 𝑥 ∈ 𝐴 Lim 𝑥 → Ord ∪ 𝐴 )
10	9	adantl	⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 Lim 𝑥 ) → Ord ∪ 𝐴 )
11		n0	⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑧 𝑧 ∈ 𝐴 )
12		0ellim	⊢ ( Lim 𝑧 → ∅ ∈ 𝑧 )
13		elunii	⊢ ( ( ∅ ∈ 𝑧 ∧ 𝑧 ∈ 𝐴 ) → ∅ ∈ ∪ 𝐴 )
14	13	expcom	⊢ ( 𝑧 ∈ 𝐴 → ( ∅ ∈ 𝑧 → ∅ ∈ ∪ 𝐴 ) )
15	12 14	syl5	⊢ ( 𝑧 ∈ 𝐴 → ( Lim 𝑧 → ∅ ∈ ∪ 𝐴 ) )
16	2 15	syld	⊢ ( 𝑧 ∈ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 Lim 𝑥 → ∅ ∈ ∪ 𝐴 ) )
17	16	exlimiv	⊢ ( ∃ 𝑧 𝑧 ∈ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 Lim 𝑥 → ∅ ∈ ∪ 𝐴 ) )
18	11 17	sylbi	⊢ ( 𝐴 ≠ ∅ → ( ∀ 𝑥 ∈ 𝐴 Lim 𝑥 → ∅ ∈ ∪ 𝐴 ) )
19	18	imp	⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 Lim 𝑥 ) → ∅ ∈ ∪ 𝐴 )
20		eluni2	⊢ ( 𝑦 ∈ ∪ 𝐴 ↔ ∃ 𝑧 ∈ 𝐴 𝑦 ∈ 𝑧 )
21	1	rspccv	⊢ ( ∀ 𝑥 ∈ 𝐴 Lim 𝑥 → ( 𝑧 ∈ 𝐴 → Lim 𝑧 ) )
22		limsuc	⊢ ( Lim 𝑧 → ( 𝑦 ∈ 𝑧 ↔ suc 𝑦 ∈ 𝑧 ) )
23	22	anbi1d	⊢ ( Lim 𝑧 → ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝐴 ) ↔ ( suc 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝐴 ) ) )
24		elunii	⊢ ( ( suc 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝐴 ) → suc 𝑦 ∈ ∪ 𝐴 )
25	23 24	biimtrdi	⊢ ( Lim 𝑧 → ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝐴 ) → suc 𝑦 ∈ ∪ 𝐴 ) )
26	25	expd	⊢ ( Lim 𝑧 → ( 𝑦 ∈ 𝑧 → ( 𝑧 ∈ 𝐴 → suc 𝑦 ∈ ∪ 𝐴 ) ) )
27	26	com3r	⊢ ( 𝑧 ∈ 𝐴 → ( Lim 𝑧 → ( 𝑦 ∈ 𝑧 → suc 𝑦 ∈ ∪ 𝐴 ) ) )
28	21 27	sylcom	⊢ ( ∀ 𝑥 ∈ 𝐴 Lim 𝑥 → ( 𝑧 ∈ 𝐴 → ( 𝑦 ∈ 𝑧 → suc 𝑦 ∈ ∪ 𝐴 ) ) )
29	28	rexlimdv	⊢ ( ∀ 𝑥 ∈ 𝐴 Lim 𝑥 → ( ∃ 𝑧 ∈ 𝐴 𝑦 ∈ 𝑧 → suc 𝑦 ∈ ∪ 𝐴 ) )
30	20 29	biimtrid	⊢ ( ∀ 𝑥 ∈ 𝐴 Lim 𝑥 → ( 𝑦 ∈ ∪ 𝐴 → suc 𝑦 ∈ ∪ 𝐴 ) )
31	30	ralrimiv	⊢ ( ∀ 𝑥 ∈ 𝐴 Lim 𝑥 → ∀ 𝑦 ∈ ∪ 𝐴 suc 𝑦 ∈ ∪ 𝐴 )
32	31	adantl	⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 Lim 𝑥 ) → ∀ 𝑦 ∈ ∪ 𝐴 suc 𝑦 ∈ ∪ 𝐴 )
33		dflim4	⊢ ( Lim ∪ 𝐴 ↔ ( Ord ∪ 𝐴 ∧ ∅ ∈ ∪ 𝐴 ∧ ∀ 𝑦 ∈ ∪ 𝐴 suc 𝑦 ∈ ∪ 𝐴 ) )
34	10 19 32 33	syl3anbrc	⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 Lim 𝑥 ) → Lim ∪ 𝐴 )