Metamath Proof Explorer

Theorem iunxpssiun1

Description: Provide an upper bound for the indexed union of cartesian products. (Contributed by Thierry Arnoux, 13-Oct-2025)

Ref Expression
Hypothesis iunxpssiun1.1 
|- ( ( ph /\ x e. A ) -> C C_ E )
Assertion iunxpssiun1 
|- ( ph -> U_ x e. A ( B X. C ) C_ ( U_ x e. A B X. E ) )

Proof

Step Hyp Ref Expression
1 iunxpssiun1.1 
 |-  ( ( ph /\ x e. A ) -> C C_ E )
2 ssiun2 
 |-  ( x e. A -> B C_ U_ x e. A B )
3 2 adantl 
 |-  ( ( ph /\ x e. A ) -> B C_ U_ x e. A B )
4 nfcv 
 |-  F/_ y B
5 nfcsb1v 
 |-  F/_ x [_ y / x ]_ B
6 csbeq1a 
 |-  ( x = y -> B = [_ y / x ]_ B )
7 4 5 6 cbviun 
 |-  U_ x e. A B = U_ y e. A [_ y / x ]_ B
8 3 7 sseqtrdi 
 |-  ( ( ph /\ x e. A ) -> B C_ U_ y e. A [_ y / x ]_ B )
9 xpss12 
 |-  ( ( B C_ U_ y e. A [_ y / x ]_ B /\ C C_ E ) -> ( B X. C ) C_ ( U_ y e. A [_ y / x ]_ B X. E ) )
10 8 1 9 syl2anc 
 |-  ( ( ph /\ x e. A ) -> ( B X. C ) C_ ( U_ y e. A [_ y / x ]_ B X. E ) )
11 10 ralrimiva 
 |-  ( ph -> A. x e. A ( B X. C ) C_ ( U_ y e. A [_ y / x ]_ B X. E ) )
12 nfcv 
 |-  F/_ x A
13 12 5 nfiun 
 |-  F/_ x U_ y e. A [_ y / x ]_ B
14 nfcv 
 |-  F/_ x E
15 13 14 nfxp 
 |-  F/_ x ( U_ y e. A [_ y / x ]_ B X. E )
16 15 iunssf 
 |-  ( U_ x e. A ( B X. C ) C_ ( U_ y e. A [_ y / x ]_ B X. E ) <-> A. x e. A ( B X. C ) C_ ( U_ y e. A [_ y / x ]_ B X. E ) )
17 11 16 sylibr 
 |-  ( ph -> U_ x e. A ( B X. C ) C_ ( U_ y e. A [_ y / x ]_ B X. E ) )
18 7 xpeq1i 
 |-  ( U_ x e. A B X. E ) = ( U_ y e. A [_ y / x ]_ B X. E )
19 17 18 sseqtrrdi 
 |-  ( ph -> U_ x e. A ( B X. C ) C_ ( U_ x e. A B X. E ) )