Metamath Proof Explorer

Theorem numiunnum

Description: An indexed union of sets is numerable if its index set is numerable and there exists a collection of well-orderings on its members. (Contributed by Matthew House, 23-Aug-2025)

Ref Expression
Assertion numiunnum 
|- ( ( A e. dom card /\ A. x e. A ( B e. V /\ S We B ) ) -> U_ x e. A B e. dom card )

Proof

Step Hyp Ref Expression
1 dfac8b 
 |-  ( A e. dom card -> E. s s We A )
2 1 adantr 
 |-  ( ( A e. dom card /\ A. x e. A ( B e. V /\ S We B ) ) -> E. s s We A )
3 simpll 
 |-  ( ( ( A e. dom card /\ A. x e. A ( B e. V /\ S We B ) ) /\ s We A ) -> A e. dom card )
4 simplr 
 |-  ( ( ( A e. dom card /\ A. x e. A ( B e. V /\ S We B ) ) /\ s We A ) -> A. x e. A ( B e. V /\ S We B ) )
5 r19.26 
 |-  ( A. x e. A ( B e. V /\ S We B ) <-> ( A. x e. A B e. V /\ A. x e. A S We B ) )
6 4 5 sylib 
 |-  ( ( ( A e. dom card /\ A. x e. A ( B e. V /\ S We B ) ) /\ s We A ) -> ( A. x e. A B e. V /\ A. x e. A S We B ) )
7 6 simpld 
 |-  ( ( ( A e. dom card /\ A. x e. A ( B e. V /\ S We B ) ) /\ s We A ) -> A. x e. A B e. V )
8 iunexg 
 |-  ( ( A e. dom card /\ A. x e. A B e. V ) -> U_ x e. A B e. _V )
9 3 7 8 syl2anc 
 |-  ( ( ( A e. dom card /\ A. x e. A ( B e. V /\ S We B ) ) /\ s We A ) -> U_ x e. A B e. _V )
10 9 9 xpexd 
 |-  ( ( ( A e. dom card /\ A. x e. A ( B e. V /\ S We B ) ) /\ s We A ) -> ( U_ x e. A B X. U_ x e. A B ) e. _V )
11 opabssxp 
 |-  { <. y , z >. | ( ( y e. U_ x e. A B /\ z e. U_ x e. A B ) /\ ( ( ( w e. U_ x e. A B |-> ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v s u ) ) ` y ) s ( ( w e. U_ x e. A B |-> ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v s u ) ) ` z ) \/ ( ( ( w e. U_ x e. A B |-> ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v s u ) ) ` y ) = ( ( w e. U_ x e. A B |-> ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v s u ) ) ` z ) /\ y [_ ( ( w e. U_ x e. A B |-> ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v s u ) ) ` y ) / x ]_ S z ) ) ) } C_ ( U_ x e. A B X. U_ x e. A B )
12 11 a1i 
 |-  ( ( ( A e. dom card /\ A. x e. A ( B e. V /\ S We B ) ) /\ s We A ) -> { <. y , z >. | ( ( y e. U_ x e. A B /\ z e. U_ x e. A B ) /\ ( ( ( w e. U_ x e. A B |-> ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v s u ) ) ` y ) s ( ( w e. U_ x e. A B |-> ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v s u ) ) ` z ) \/ ( ( ( w e. U_ x e. A B |-> ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v s u ) ) ` y ) = ( ( w e. U_ x e. A B |-> ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v s u ) ) ` z ) /\ y [_ ( ( w e. U_ x e. A B |-> ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v s u ) ) ` y ) / x ]_ S z ) ) ) } C_ ( U_ x e. A B X. U_ x e. A B ) )
13 10 12 ssexd 
 |-  ( ( ( A e. dom card /\ A. x e. A ( B e. V /\ S We B ) ) /\ s We A ) -> { <. y , z >. | ( ( y e. U_ x e. A B /\ z e. U_ x e. A B ) /\ ( ( ( w e. U_ x e. A B |-> ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v s u ) ) ` y ) s ( ( w e. U_ x e. A B |-> ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v s u ) ) ` z ) \/ ( ( ( w e. U_ x e. A B |-> ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v s u ) ) ` y ) = ( ( w e. U_ x e. A B |-> ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v s u ) ) ` z ) /\ y [_ ( ( w e. U_ x e. A B |-> ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v s u ) ) ` y ) / x ]_ S z ) ) ) } e. _V )
14 simpr 
 |-  ( ( ( A e. dom card /\ A. x e. A ( B e. V /\ S We B ) ) /\ s We A ) -> s We A )
15 exse 
 |-  ( A e. dom card -> s Se A )
16 15 ad2antrr 
 |-  ( ( ( A e. dom card /\ A. x e. A ( B e. V /\ S We B ) ) /\ s We A ) -> s Se A )
17 6 simprd 
 |-  ( ( ( A e. dom card /\ A. x e. A ( B e. V /\ S We B ) ) /\ s We A ) -> A. x e. A S We B )
18 eqid 
 |-  ( w e. U_ x e. A B |-> ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v s u ) ) = ( w e. U_ x e. A B |-> ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v s u ) )
19 eqid 
 |-  { <. y , z >. | ( ( y e. U_ x e. A B /\ z e. U_ x e. A B ) /\ ( ( ( w e. U_ x e. A B |-> ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v s u ) ) ` y ) s ( ( w e. U_ x e. A B |-> ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v s u ) ) ` z ) \/ ( ( ( w e. U_ x e. A B |-> ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v s u ) ) ` y ) = ( ( w e. U_ x e. A B |-> ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v s u ) ) ` z ) /\ y [_ ( ( w e. U_ x e. A B |-> ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v s u ) ) ` y ) / x ]_ S z ) ) ) } = { <. y , z >. | ( ( y e. U_ x e. A B /\ z e. U_ x e. A B ) /\ ( ( ( w e. U_ x e. A B |-> ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v s u ) ) ` y ) s ( ( w e. U_ x e. A B |-> ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v s u ) ) ` z ) \/ ( ( ( w e. U_ x e. A B |-> ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v s u ) ) ` y ) = ( ( w e. U_ x e. A B |-> ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v s u ) ) ` z ) /\ y [_ ( ( w e. U_ x e. A B |-> ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v s u ) ) ` y ) / x ]_ S z ) ) ) }
20 18 19 weiunwe 
 |-  ( ( s We A /\ s Se A /\ A. x e. A S We B ) -> { <. y , z >. | ( ( y e. U_ x e. A B /\ z e. U_ x e. A B ) /\ ( ( ( w e. U_ x e. A B |-> ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v s u ) ) ` y ) s ( ( w e. U_ x e. A B |-> ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v s u ) ) ` z ) \/ ( ( ( w e. U_ x e. A B |-> ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v s u ) ) ` y ) = ( ( w e. U_ x e. A B |-> ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v s u ) ) ` z ) /\ y [_ ( ( w e. U_ x e. A B |-> ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v s u ) ) ` y ) / x ]_ S z ) ) ) } We U_ x e. A B )
21 14 16 17 20 syl3anc 
 |-  ( ( ( A e. dom card /\ A. x e. A ( B e. V /\ S We B ) ) /\ s We A ) -> { <. y , z >. | ( ( y e. U_ x e. A B /\ z e. U_ x e. A B ) /\ ( ( ( w e. U_ x e. A B |-> ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v s u ) ) ` y ) s ( ( w e. U_ x e. A B |-> ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v s u ) ) ` z ) \/ ( ( ( w e. U_ x e. A B |-> ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v s u ) ) ` y ) = ( ( w e. U_ x e. A B |-> ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v s u ) ) ` z ) /\ y [_ ( ( w e. U_ x e. A B |-> ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v s u ) ) ` y ) / x ]_ S z ) ) ) } We U_ x e. A B )
22 weeq1 
 |-  ( t = { <. y , z >. | ( ( y e. U_ x e. A B /\ z e. U_ x e. A B ) /\ ( ( ( w e. U_ x e. A B |-> ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v s u ) ) ` y ) s ( ( w e. U_ x e. A B |-> ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v s u ) ) ` z ) \/ ( ( ( w e. U_ x e. A B |-> ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v s u ) ) ` y ) = ( ( w e. U_ x e. A B |-> ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v s u ) ) ` z ) /\ y [_ ( ( w e. U_ x e. A B |-> ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v s u ) ) ` y ) / x ]_ S z ) ) ) } -> ( t We U_ x e. A B <-> { <. y , z >. | ( ( y e. U_ x e. A B /\ z e. U_ x e. A B ) /\ ( ( ( w e. U_ x e. A B |-> ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v s u ) ) ` y ) s ( ( w e. U_ x e. A B |-> ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v s u ) ) ` z ) \/ ( ( ( w e. U_ x e. A B |-> ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v s u ) ) ` y ) = ( ( w e. U_ x e. A B |-> ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v s u ) ) ` z ) /\ y [_ ( ( w e. U_ x e. A B |-> ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v s u ) ) ` y ) / x ]_ S z ) ) ) } We U_ x e. A B ) )
23 13 21 22 spcedv 
 |-  ( ( ( A e. dom card /\ A. x e. A ( B e. V /\ S We B ) ) /\ s We A ) -> E. t t We U_ x e. A B )
24 2 23 exlimddv 
 |-  ( ( A e. dom card /\ A. x e. A ( B e. V /\ S We B ) ) -> E. t t We U_ x e. A B )
25 ween 
 |-  ( U_ x e. A B e. dom card <-> E. t t We U_ x e. A B )
26 24 25 sylibr 
 |-  ( ( A e. dom card /\ A. x e. A ( B e. V /\ S We B ) ) -> U_ x e. A B e. dom card )