Metamath Proof Explorer

Theorem fissorduni

Description: The union (supremum) of a finite set of ordinals less than a nonzero ordinal class is an element of that ordinal class. (Contributed by BTernaryTau, 15-Jan-2026)

Ref Expression
Assertion fissorduni ⊢ A ∈ Fin ∧ A ⊆ B ∧ Ord ⁡ B ∧ B ≠ ∅ → ⋃ A ∈ B

Proof

Step Hyp Ref Expression
1 ord0eln0 ⊢ Ord ⁡ B → ∅ ∈ B ↔ B ≠ ∅
2 1 biimpar ⊢ Ord ⁡ B ∧ B ≠ ∅ → ∅ ∈ B
3 uni0 ⊢ ⋃ ∅ = ∅
4 3 eleq1i ⊢ ⋃ ∅ ∈ B ↔ ∅ ∈ B
5 4 biimpri ⊢ ∅ ∈ B → ⋃ ∅ ∈ B
6 unieq ⊢ A = ∅ → ⋃ A = ⋃ ∅
7 6 eleq1d ⊢ A = ∅ → ⋃ A ∈ B ↔ ⋃ ∅ ∈ B
8 5 7 syl5ibrcom ⊢ ∅ ∈ B → A = ∅ → ⋃ A ∈ B
9 2 8 syl ⊢ Ord ⁡ B ∧ B ≠ ∅ → A = ∅ → ⋃ A ∈ B
10 9 3ad2ant3 ⊢ A ∈ Fin ∧ A ⊆ B ∧ Ord ⁡ B ∧ B ≠ ∅ → A = ∅ → ⋃ A ∈ B
11 ordsson ⊢ Ord ⁡ B → B ⊆ On
12 sstr ⊢ A ⊆ B ∧ B ⊆ On → A ⊆ On
13 11 12 sylan2 ⊢ A ⊆ B ∧ Ord ⁡ B → A ⊆ On
14 13 adantrr ⊢ A ⊆ B ∧ Ord ⁡ B ∧ B ≠ ∅ → A ⊆ On
15 14 3adant1 ⊢ A ∈ Fin ∧ A ⊆ B ∧ Ord ⁡ B ∧ B ≠ ∅ → A ⊆ On
16 15 adantr ⊢ A ∈ Fin ∧ A ⊆ B ∧ Ord ⁡ B ∧ B ≠ ∅ ∧ A ≠ ∅ → A ⊆ On
17 simpl1 ⊢ A ∈ Fin ∧ A ⊆ B ∧ Ord ⁡ B ∧ B ≠ ∅ ∧ A ≠ ∅ → A ∈ Fin
18 simpr ⊢ A ∈ Fin ∧ A ⊆ B ∧ Ord ⁡ B ∧ B ≠ ∅ ∧ A ≠ ∅ → A ≠ ∅
19 ordunifi ⊢ A ⊆ On ∧ A ∈ Fin ∧ A ≠ ∅ → ⋃ A ∈ A
20 16 17 18 19 syl3anc ⊢ A ∈ Fin ∧ A ⊆ B ∧ Ord ⁡ B ∧ B ≠ ∅ ∧ A ≠ ∅ → ⋃ A ∈ A
21 20 ex ⊢ A ∈ Fin ∧ A ⊆ B ∧ Ord ⁡ B ∧ B ≠ ∅ → A ≠ ∅ → ⋃ A ∈ A
22 ssel ⊢ A ⊆ B → ⋃ A ∈ A → ⋃ A ∈ B
23 22 3ad2ant2 ⊢ A ∈ Fin ∧ A ⊆ B ∧ Ord ⁡ B ∧ B ≠ ∅ → ⋃ A ∈ A → ⋃ A ∈ B
24 21 23 syld ⊢ A ∈ Fin ∧ A ⊆ B ∧ Ord ⁡ B ∧ B ≠ ∅ → A ≠ ∅ → ⋃ A ∈ B
25 10 24 pm2.61dne ⊢ A ∈ Fin ∧ A ⊆ B ∧ Ord ⁡ B ∧ B ≠ ∅ → ⋃ A ∈ B