Metamath Proof Explorer

Theorem onsupuni

Description: The supremum of a set of ordinals is the union of that set. Lemma 2.10 of Schloeder p. 5. (Contributed by RP, 19-Jan-2025)

Ref Expression
Assertion onsupuni 
|- ( ( A C_ On /\ A e. V ) -> sup ( A , On , _E ) = U. A )

Proof

Step Hyp Ref Expression
1 ssonuni 
 |-  ( A e. V -> ( A C_ On -> U. A e. On ) )
2 1 impcom 
 |-  ( ( A C_ On /\ A e. V ) -> U. A e. On )
3 elssuni 
 |-  ( y e. A -> y C_ U. A )
4 3 rgen 
 |-  A. y e. A y C_ U. A
5 simpl 
 |-  ( ( A C_ On /\ A e. V ) -> A C_ On )
6 5 sselda 
 |-  ( ( ( A C_ On /\ A e. V ) /\ y e. A ) -> y e. On )
7 2 adantr 
 |-  ( ( ( A C_ On /\ A e. V ) /\ y e. A ) -> U. A e. On )
8 ontri1 
 |-  ( ( y e. On /\ U. A e. On ) -> ( y C_ U. A <-> -. U. A e. y ) )
9 6 7 8 syl2anc 
 |-  ( ( ( A C_ On /\ A e. V ) /\ y e. A ) -> ( y C_ U. A <-> -. U. A e. y ) )
10 epel 
 |-  ( U. A _E y <-> U. A e. y )
11 10 notbii 
 |-  ( -. U. A _E y <-> -. U. A e. y )
12 9 11 bitr4di 
 |-  ( ( ( A C_ On /\ A e. V ) /\ y e. A ) -> ( y C_ U. A <-> -. U. A _E y ) )
13 12 ralbidva 
 |-  ( ( A C_ On /\ A e. V ) -> ( A. y e. A y C_ U. A <-> A. y e. A -. U. A _E y ) )
14 4 13 mpbii 
 |-  ( ( A C_ On /\ A e. V ) -> A. y e. A -. U. A _E y )
15 2 adantr 
 |-  ( ( ( A C_ On /\ A e. V ) /\ y e. On ) -> U. A e. On )
16 epelg 
 |-  ( U. A e. On -> ( y _E U. A <-> y e. U. A ) )
17 15 16 syl 
 |-  ( ( ( A C_ On /\ A e. V ) /\ y e. On ) -> ( y _E U. A <-> y e. U. A ) )
18 17 biimpd 
 |-  ( ( ( A C_ On /\ A e. V ) /\ y e. On ) -> ( y _E U. A -> y e. U. A ) )
19 eluni2 
 |-  ( y e. U. A <-> E. x e. A y e. x )
20 epel 
 |-  ( y _E x <-> y e. x )
21 20 rexbii 
 |-  ( E. x e. A y _E x <-> E. x e. A y e. x )
22 19 21 bitr4i 
 |-  ( y e. U. A <-> E. x e. A y _E x )
23 18 22 imbitrdi 
 |-  ( ( ( A C_ On /\ A e. V ) /\ y e. On ) -> ( y _E U. A -> E. x e. A y _E x ) )
24 23 ralrimiva 
 |-  ( ( A C_ On /\ A e. V ) -> A. y e. On ( y _E U. A -> E. x e. A y _E x ) )
25 epweon 
 |-  _E We On
26 weso 
 |-  ( _E We On -> _E Or On )
27 25 26 mp1i 
 |-  ( ( A C_ On /\ A e. V ) -> _E Or On )
28 27 eqsup 
 |-  ( ( A C_ On /\ A e. V ) -> ( ( U. A e. On /\ A. y e. A -. U. A _E y /\ A. y e. On ( y _E U. A -> E. x e. A y _E x ) ) -> sup ( A , On , _E ) = U. A ) )
29 2 14 24 28 mp3and 
 |-  ( ( A C_ On /\ A e. V ) -> sup ( A , On , _E ) = U. A )