Theorem ssorduni

Description: The union of a class of ordinal numbers is ordinal. Proposition 7.19 of TakeutiZaring p. 40. (Contributed by NM, 30-May-1994) (Proof shortened by Andrew Salmon, 12-Aug-2011)

	Ref	Expression
Assertion	ssorduni	⊢ ( 𝐴 ⊆ On → Ord ∪ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		eluni2	⊢ ( 𝑥 ∈ ∪ 𝐴 ↔ ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 )
2		ssel	⊢ ( 𝐴 ⊆ On → ( 𝑦 ∈ 𝐴 → 𝑦 ∈ On ) )
3		onelss	⊢ ( 𝑦 ∈ On → ( 𝑥 ∈ 𝑦 → 𝑥 ⊆ 𝑦 ) )
4	2 3	syl6	⊢ ( 𝐴 ⊆ On → ( 𝑦 ∈ 𝐴 → ( 𝑥 ∈ 𝑦 → 𝑥 ⊆ 𝑦 ) ) )
5		anc2r	⊢ ( ( 𝑦 ∈ 𝐴 → ( 𝑥 ∈ 𝑦 → 𝑥 ⊆ 𝑦 ) ) → ( 𝑦 ∈ 𝐴 → ( 𝑥 ∈ 𝑦 → ( 𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝐴 ) ) ) )
6	4 5	syl	⊢ ( 𝐴 ⊆ On → ( 𝑦 ∈ 𝐴 → ( 𝑥 ∈ 𝑦 → ( 𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝐴 ) ) ) )
7		ssuni	⊢ ( ( 𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑥 ⊆ ∪ 𝐴 )
8	6 7	syl8	⊢ ( 𝐴 ⊆ On → ( 𝑦 ∈ 𝐴 → ( 𝑥 ∈ 𝑦 → 𝑥 ⊆ ∪ 𝐴 ) ) )
9	8	rexlimdv	⊢ ( 𝐴 ⊆ On → ( ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 → 𝑥 ⊆ ∪ 𝐴 ) )
10	1 9	syl5bi	⊢ ( 𝐴 ⊆ On → ( 𝑥 ∈ ∪ 𝐴 → 𝑥 ⊆ ∪ 𝐴 ) )
11	10	ralrimiv	⊢ ( 𝐴 ⊆ On → ∀ 𝑥 ∈ ∪ 𝐴 𝑥 ⊆ ∪ 𝐴 )
12		dftr3	⊢ ( Tr ∪ 𝐴 ↔ ∀ 𝑥 ∈ ∪ 𝐴 𝑥 ⊆ ∪ 𝐴 )
13	11 12	sylibr	⊢ ( 𝐴 ⊆ On → Tr ∪ 𝐴 )
14		onelon	⊢ ( ( 𝑦 ∈ On ∧ 𝑥 ∈ 𝑦 ) → 𝑥 ∈ On )
15	14	ex	⊢ ( 𝑦 ∈ On → ( 𝑥 ∈ 𝑦 → 𝑥 ∈ On ) )
16	2 15	syl6	⊢ ( 𝐴 ⊆ On → ( 𝑦 ∈ 𝐴 → ( 𝑥 ∈ 𝑦 → 𝑥 ∈ On ) ) )
17	16	rexlimdv	⊢ ( 𝐴 ⊆ On → ( ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 → 𝑥 ∈ On ) )
18	1 17	syl5bi	⊢ ( 𝐴 ⊆ On → ( 𝑥 ∈ ∪ 𝐴 → 𝑥 ∈ On ) )
19	18	ssrdv	⊢ ( 𝐴 ⊆ On → ∪ 𝐴 ⊆ On )
20		ordon	⊢ Ord On
21		trssord	⊢ ( ( Tr ∪ 𝐴 ∧ ∪ 𝐴 ⊆ On ∧ Ord On ) → Ord ∪ 𝐴 )
22	21	3exp	⊢ ( Tr ∪ 𝐴 → ( ∪ 𝐴 ⊆ On → ( Ord On → Ord ∪ 𝐴 ) ) )
23	20 22	mpii	⊢ ( Tr ∪ 𝐴 → ( ∪ 𝐴 ⊆ On → Ord ∪ 𝐴 ) )
24	13 19 23	sylc	⊢ ( 𝐴 ⊆ On → Ord ∪ 𝐴 )