Theorem iunord

Description: The indexed union of a collection of ordinal numbers B ( x ) is ordinal. This proof is based on the proof of ssorduni , but does not use it directly, since ssorduni does not work when B is a proper class. (Contributed by Emmett Weisz, 3-Nov-2019)

	Ref	Expression
Assertion	iunord	⊢ ( ∀ 𝑥 ∈ 𝐴 Ord 𝐵 → Ord ∪ 𝑥 ∈ 𝐴 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		ordtr	⊢ ( Ord 𝐵 → Tr 𝐵 )
2	1	ralimi	⊢ ( ∀ 𝑥 ∈ 𝐴 Ord 𝐵 → ∀ 𝑥 ∈ 𝐴 Tr 𝐵 )
3		triun	⊢ ( ∀ 𝑥 ∈ 𝐴 Tr 𝐵 → Tr ∪ 𝑥 ∈ 𝐴 𝐵 )
4	2 3	syl	⊢ ( ∀ 𝑥 ∈ 𝐴 Ord 𝐵 → Tr ∪ 𝑥 ∈ 𝐴 𝐵 )
5		eliun	⊢ ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 )
6		nfra1	⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ 𝐴 Ord 𝐵
7		nfv	⊢ Ⅎ 𝑥 𝑦 ∈ On
8		rsp	⊢ ( ∀ 𝑥 ∈ 𝐴 Ord 𝐵 → ( 𝑥 ∈ 𝐴 → Ord 𝐵 ) )
9		ordelon	⊢ ( ( Ord 𝐵 ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ On )
10	9	ex	⊢ ( Ord 𝐵 → ( 𝑦 ∈ 𝐵 → 𝑦 ∈ On ) )
11	8 10	syl6	⊢ ( ∀ 𝑥 ∈ 𝐴 Ord 𝐵 → ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐵 → 𝑦 ∈ On ) ) )
12	6 7 11	rexlimd	⊢ ( ∀ 𝑥 ∈ 𝐴 Ord 𝐵 → ( ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ On ) )
13	5 12	biimtrid	⊢ ( ∀ 𝑥 ∈ 𝐴 Ord 𝐵 → ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → 𝑦 ∈ On ) )
14	13	ssrdv	⊢ ( ∀ 𝑥 ∈ 𝐴 Ord 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ On )
15		ordon	⊢ Ord On
16		trssord	⊢ ( ( Tr ∪ 𝑥 ∈ 𝐴 𝐵 ∧ ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ On ∧ Ord On ) → Ord ∪ 𝑥 ∈ 𝐴 𝐵 )
17	16	3exp	⊢ ( Tr ∪ 𝑥 ∈ 𝐴 𝐵 → ( ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ On → ( Ord On → Ord ∪ 𝑥 ∈ 𝐴 𝐵 ) ) )
18	15 17	mpii	⊢ ( Tr ∪ 𝑥 ∈ 𝐴 𝐵 → ( ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ On → Ord ∪ 𝑥 ∈ 𝐴 𝐵 ) )
19	4 14 18	sylc	⊢ ( ∀ 𝑥 ∈ 𝐴 Ord 𝐵 → Ord ∪ 𝑥 ∈ 𝐴 𝐵 )