Metamath Proof Explorer


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 syl5bi ( ∀ 𝑥𝐴 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 𝑥𝐴 𝐵 )