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 e. Fin /\ A C_ B /\ ( Ord B /\ B =/= (/) ) ) -> U. A e. B )

Proof

Step Hyp Ref Expression
1 ord0eln0 
 |-  ( Ord B -> ( (/) e. B <-> B =/= (/) ) )
2 1 biimpar 
 |-  ( ( Ord B /\ B =/= (/) ) -> (/) e. B )
3 uni0 
 |-  U. (/) = (/)
4 3 eleq1i 
 |-  ( U. (/) e. B <-> (/) e. B )
5 4 biimpri 
 |-  ( (/) e. B -> U. (/) e. B )
6 unieq 
 |-  ( A = (/) -> U. A = U. (/) )
7 6 eleq1d 
 |-  ( A = (/) -> ( U. A e. B <-> U. (/) e. B ) )
8 5 7 syl5ibrcom 
 |-  ( (/) e. B -> ( A = (/) -> U. A e. B ) )
9 2 8 syl 
 |-  ( ( Ord B /\ B =/= (/) ) -> ( A = (/) -> U. A e. B ) )
10 9 3ad2ant3 
 |-  ( ( A e. Fin /\ A C_ B /\ ( Ord B /\ B =/= (/) ) ) -> ( A = (/) -> U. A e. B ) )
11 ordsson 
 |-  ( Ord B -> B C_ On )
12 sstr 
 |-  ( ( A C_ B /\ B C_ On ) -> A C_ On )
13 11 12 sylan2 
 |-  ( ( A C_ B /\ Ord B ) -> A C_ On )
14 13 adantrr 
 |-  ( ( A C_ B /\ ( Ord B /\ B =/= (/) ) ) -> A C_ On )
15 14 3adant1 
 |-  ( ( A e. Fin /\ A C_ B /\ ( Ord B /\ B =/= (/) ) ) -> A C_ On )
16 15 adantr 
 |-  ( ( ( A e. Fin /\ A C_ B /\ ( Ord B /\ B =/= (/) ) ) /\ A =/= (/) ) -> A C_ On )
17 simpl1 
 |-  ( ( ( A e. Fin /\ A C_ B /\ ( Ord B /\ B =/= (/) ) ) /\ A =/= (/) ) -> A e. Fin )
18 simpr 
 |-  ( ( ( A e. Fin /\ A C_ B /\ ( Ord B /\ B =/= (/) ) ) /\ A =/= (/) ) -> A =/= (/) )
19 ordunifi 
 |-  ( ( A C_ On /\ A e. Fin /\ A =/= (/) ) -> U. A e. A )
20 16 17 18 19 syl3anc 
 |-  ( ( ( A e. Fin /\ A C_ B /\ ( Ord B /\ B =/= (/) ) ) /\ A =/= (/) ) -> U. A e. A )
21 20 ex 
 |-  ( ( A e. Fin /\ A C_ B /\ ( Ord B /\ B =/= (/) ) ) -> ( A =/= (/) -> U. A e. A ) )
22 ssel 
 |-  ( A C_ B -> ( U. A e. A -> U. A e. B ) )
23 22 3ad2ant2 
 |-  ( ( A e. Fin /\ A C_ B /\ ( Ord B /\ B =/= (/) ) ) -> ( U. A e. A -> U. A e. B ) )
24 21 23 syld 
 |-  ( ( A e. Fin /\ A C_ B /\ ( Ord B /\ B =/= (/) ) ) -> ( A =/= (/) -> U. A e. B ) )
25 10 24 pm2.61dne 
 |-  ( ( A e. Fin /\ A C_ B /\ ( Ord B /\ B =/= (/) ) ) -> U. A e. B )