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 ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ 𝐵 ∧ ( Ord 𝐵 ∧ 𝐵 ≠ ∅ ) ) → ∪ 𝐴 ∈ 𝐵 )

Proof

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