Metamath Proof Explorer

Theorem ralssiun

Description: The index set of an indexed union is a subset of the union when each B contains its index. (Contributed by ML, 16-Dec-2020)

Ref Expression
Assertion ralssiun 
|- ( A. x e. A x e. B -> A C_ U_ x e. A B )

Proof

Step Hyp Ref Expression
1 nfra1 
 |-  F/ x A. x e. A x e. B
2 nfcv 
 |-  F/_ x A
3 nfiu1 
 |-  F/_ x U_ x e. A B
4 simpr 
 |-  ( ( ( x = y /\ A. x e. A x e. B ) /\ x e. A ) -> x e. A )
5 rsp 
 |-  ( A. x e. A x e. B -> ( x e. A -> x e. B ) )
6 5 adantl 
 |-  ( ( x = y /\ A. x e. A x e. B ) -> ( x e. A -> x e. B ) )
7 eleq1 
 |-  ( x = y -> ( x e. B <-> y e. B ) )
8 7 imbi2d 
 |-  ( x = y -> ( ( x e. A -> x e. B ) <-> ( x e. A -> y e. B ) ) )
9 8 adantr 
 |-  ( ( x = y /\ A. x e. A x e. B ) -> ( ( x e. A -> x e. B ) <-> ( x e. A -> y e. B ) ) )
10 6 9 mpbid 
 |-  ( ( x = y /\ A. x e. A x e. B ) -> ( x e. A -> y e. B ) )
11 10 imp 
 |-  ( ( ( x = y /\ A. x e. A x e. B ) /\ x e. A ) -> y e. B )
12 rspe 
 |-  ( ( x e. A /\ y e. B ) -> E. x e. A y e. B )
13 4 11 12 syl2anc 
 |-  ( ( ( x = y /\ A. x e. A x e. B ) /\ x e. A ) -> E. x e. A y e. B )
14 abid 
 |-  ( y e. { y | E. x e. A y e. B } <-> E. x e. A y e. B )
15 13 14 sylibr 
 |-  ( ( ( x = y /\ A. x e. A x e. B ) /\ x e. A ) -> y e. { y | E. x e. A y e. B } )
16 eleq1 
 |-  ( x = y -> ( x e. { y | E. x e. A y e. B } <-> y e. { y | E. x e. A y e. B } ) )
17 16 ad2antrr 
 |-  ( ( ( x = y /\ A. x e. A x e. B ) /\ x e. A ) -> ( x e. { y | E. x e. A y e. B } <-> y e. { y | E. x e. A y e. B } ) )
18 15 17 mpbird 
 |-  ( ( ( x = y /\ A. x e. A x e. B ) /\ x e. A ) -> x e. { y | E. x e. A y e. B } )
19 df-iun 
 |-  U_ x e. A B = { y | E. x e. A y e. B }
20 18 19 eleqtrrdi 
 |-  ( ( ( x = y /\ A. x e. A x e. B ) /\ x e. A ) -> x e. U_ x e. A B )
21 20 expl 
 |-  ( x = y -> ( ( A. x e. A x e. B /\ x e. A ) -> x e. U_ x e. A B ) )
22 21 equcoms 
 |-  ( y = x -> ( ( A. x e. A x e. B /\ x e. A ) -> x e. U_ x e. A B ) )
23 22 vtocleg 
 |-  ( x e. A -> ( ( A. x e. A x e. B /\ x e. A ) -> x e. U_ x e. A B ) )
24 23 anabsi7 
 |-  ( ( A. x e. A x e. B /\ x e. A ) -> x e. U_ x e. A B )
25 24 ex 
 |-  ( A. x e. A x e. B -> ( x e. A -> x e. U_ x e. A B ) )
26 1 2 3 25 ssrd 
 |-  ( A. x e. A x e. B -> A C_ U_ x e. A B )