Metamath Proof Explorer

Theorem onintunirab

Description: The intersection of a non-empty class of ordinals is the union of every ordinal less-than-or-equal to every element of that class. (Contributed by RP, 29-Jan-2025)

Ref Expression
Assertion onintunirab 
|- ( ( A C_ On /\ A =/= (/) ) -> |^| A = U. { x e. On | A. y e. A x C_ y } )

Proof

Step Hyp Ref Expression
1 simp3 
 |-  ( ( ( A C_ On /\ A =/= (/) ) /\ x e. On /\ A. y e. A x C_ y ) -> A. y e. A x C_ y )
2 ssint 
 |-  ( x C_ |^| A <-> A. y e. A x C_ y )
3 1 2 sylibr 
 |-  ( ( ( A C_ On /\ A =/= (/) ) /\ x e. On /\ A. y e. A x C_ y ) -> x C_ |^| A )
4 simp2 
 |-  ( ( ( A C_ On /\ A =/= (/) ) /\ x e. On /\ A. y e. A x C_ y ) -> x e. On )
5 oninton 
 |-  ( ( A C_ On /\ A =/= (/) ) -> |^| A e. On )
6 5 3ad2ant1 
 |-  ( ( ( A C_ On /\ A =/= (/) ) /\ x e. On /\ A. y e. A x C_ y ) -> |^| A e. On )
7 onsssuc 
 |-  ( ( x e. On /\ |^| A e. On ) -> ( x C_ |^| A <-> x e. suc |^| A ) )
8 4 6 7 syl2anc 
 |-  ( ( ( A C_ On /\ A =/= (/) ) /\ x e. On /\ A. y e. A x C_ y ) -> ( x C_ |^| A <-> x e. suc |^| A ) )
9 3 8 mpbid 
 |-  ( ( ( A C_ On /\ A =/= (/) ) /\ x e. On /\ A. y e. A x C_ y ) -> x e. suc |^| A )
10 9 rabssdv 
 |-  ( ( A C_ On /\ A =/= (/) ) -> { x e. On | A. y e. A x C_ y } C_ suc |^| A )
11 ssrab2 
 |-  { x e. On | A. y e. A x C_ y } C_ On
12 11 a1i 
 |-  ( ( A C_ On /\ A =/= (/) ) -> { x e. On | A. y e. A x C_ y } C_ On )
13 eloni 
 |-  ( |^| A e. On -> Ord |^| A )
14 5 13 syl 
 |-  ( ( A C_ On /\ A =/= (/) ) -> Ord |^| A )
15 ordunisssuc 
 |-  ( ( { x e. On | A. y e. A x C_ y } C_ On /\ Ord |^| A ) -> ( U. { x e. On | A. y e. A x C_ y } C_ |^| A <-> { x e. On | A. y e. A x C_ y } C_ suc |^| A ) )
16 12 14 15 syl2anc 
 |-  ( ( A C_ On /\ A =/= (/) ) -> ( U. { x e. On | A. y e. A x C_ y } C_ |^| A <-> { x e. On | A. y e. A x C_ y } C_ suc |^| A ) )
17 10 16 mpbird 
 |-  ( ( A C_ On /\ A =/= (/) ) -> U. { x e. On | A. y e. A x C_ y } C_ |^| A )
18 sseq1 
 |-  ( x = |^| A -> ( x C_ y <-> |^| A C_ y ) )
19 18 ralbidv 
 |-  ( x = |^| A -> ( A. y e. A x C_ y <-> A. y e. A |^| A C_ y ) )
20 intss1 
 |-  ( y e. A -> |^| A C_ y )
21 20 rgen 
 |-  A. y e. A |^| A C_ y
22 21 a1i 
 |-  ( ( A C_ On /\ A =/= (/) ) -> A. y e. A |^| A C_ y )
23 19 5 22 elrabd 
 |-  ( ( A C_ On /\ A =/= (/) ) -> |^| A e. { x e. On | A. y e. A x C_ y } )
24 unissel 
 |-  ( ( U. { x e. On | A. y e. A x C_ y } C_ |^| A /\ |^| A e. { x e. On | A. y e. A x C_ y } ) -> U. { x e. On | A. y e. A x C_ y } = |^| A )
25 17 23 24 syl2anc 
 |-  ( ( A C_ On /\ A =/= (/) ) -> U. { x e. On | A. y e. A x C_ y } = |^| A )
26 25 eqcomd 
 |-  ( ( A C_ On /\ A =/= (/) ) -> |^| A = U. { x e. On | A. y e. A x C_ y } )