Metamath Proof Explorer

Theorem ss2iundf

Description: Subclass theorem for indexed union. (Contributed by RP, 17-Jul-2020)

Ref Expression
Hypotheses ss2iundf.xph 
|- F/ x ph
ss2iundf.yph 
|- F/ y ph
ss2iundf.y 
|- F/_ y Y
ss2iundf.a 
|- F/_ y A
ss2iundf.b 
|- F/_ y B
ss2iundf.xc 
|- F/_ x C
ss2iundf.yc 
|- F/_ y C
ss2iundf.d 
|- F/_ x D
ss2iundf.g 
|- F/_ y G
ss2iundf.el 
|- ( ( ph /\ x e. A ) -> Y e. C )
ss2iundf.sub 
|- ( ( ph /\ x e. A /\ y = Y ) -> D = G )
ss2iundf.ss 
|- ( ( ph /\ x e. A ) -> B C_ G )
Assertion ss2iundf 
|- ( ph -> U_ x e. A B C_ U_ y e. C D )

Proof

Step Hyp Ref Expression
1 ss2iundf.xph 
 |-  F/ x ph
2 ss2iundf.yph 
 |-  F/ y ph
3 ss2iundf.y 
 |-  F/_ y Y
4 ss2iundf.a 
 |-  F/_ y A
5 ss2iundf.b 
 |-  F/_ y B
6 ss2iundf.xc 
 |-  F/_ x C
7 ss2iundf.yc 
 |-  F/_ y C
8 ss2iundf.d 
 |-  F/_ x D
9 ss2iundf.g 
 |-  F/_ y G
10 ss2iundf.el 
 |-  ( ( ph /\ x e. A ) -> Y e. C )
11 ss2iundf.sub 
 |-  ( ( ph /\ x e. A /\ y = Y ) -> D = G )
12 ss2iundf.ss 
 |-  ( ( ph /\ x e. A ) -> B C_ G )
13 df-ral 
 |-  ( A. y e. C -. B C_ D <-> A. y ( y e. C -> -. B C_ D ) )
14 4 nfcri 
 |-  F/ y x e. A
15 2 14 nfan 
 |-  F/ y ( ph /\ x e. A )
16 simpr 
 |-  ( ( ( ph /\ x e. A ) /\ y = Y ) -> y = Y )
17 16 eleq1d 
 |-  ( ( ( ph /\ x e. A ) /\ y = Y ) -> ( y e. C <-> Y e. C ) )
18 17 biimprd 
 |-  ( ( ( ph /\ x e. A ) /\ y = Y ) -> ( Y e. C -> y e. C ) )
19 11 sseq2d 
 |-  ( ( ph /\ x e. A /\ y = Y ) -> ( B C_ D <-> B C_ G ) )
20 19 3expa 
 |-  ( ( ( ph /\ x e. A ) /\ y = Y ) -> ( B C_ D <-> B C_ G ) )
21 20 notbid 
 |-  ( ( ( ph /\ x e. A ) /\ y = Y ) -> ( -. B C_ D <-> -. B C_ G ) )
22 21 biimpd 
 |-  ( ( ( ph /\ x e. A ) /\ y = Y ) -> ( -. B C_ D -> -. B C_ G ) )
23 18 22 imim12d 
 |-  ( ( ( ph /\ x e. A ) /\ y = Y ) -> ( ( y e. C -> -. B C_ D ) -> ( Y e. C -> -. B C_ G ) ) )
24 23 ex 
 |-  ( ( ph /\ x e. A ) -> ( y = Y -> ( ( y e. C -> -. B C_ D ) -> ( Y e. C -> -. B C_ G ) ) ) )
25 15 24 alrimi 
 |-  ( ( ph /\ x e. A ) -> A. y ( y = Y -> ( ( y e. C -> -. B C_ D ) -> ( Y e. C -> -. B C_ G ) ) ) )
26 3 7 nfel 
 |-  F/ y Y e. C
27 5 9 nfss 
 |-  F/ y B C_ G
28 27 nfn 
 |-  F/ y -. B C_ G
29 26 28 nfim 
 |-  F/ y ( Y e. C -> -. B C_ G )
30 29 3 spcimgft 
 |-  ( A. y ( y = Y -> ( ( y e. C -> -. B C_ D ) -> ( Y e. C -> -. B C_ G ) ) ) -> ( Y e. C -> ( A. y ( y e. C -> -. B C_ D ) -> ( Y e. C -> -. B C_ G ) ) ) )
31 25 10 30 sylc 
 |-  ( ( ph /\ x e. A ) -> ( A. y ( y e. C -> -. B C_ D ) -> ( Y e. C -> -. B C_ G ) ) )
32 10 31 mpid 
 |-  ( ( ph /\ x e. A ) -> ( A. y ( y e. C -> -. B C_ D ) -> -. B C_ G ) )
33 13 32 syl5bi 
 |-  ( ( ph /\ x e. A ) -> ( A. y e. C -. B C_ D -> -. B C_ G ) )
34 33 con2d 
 |-  ( ( ph /\ x e. A ) -> ( B C_ G -> -. A. y e. C -. B C_ D ) )
35 dfrex2 
 |-  ( E. y e. C B C_ D <-> -. A. y e. C -. B C_ D )
36 34 35 syl6ibr 
 |-  ( ( ph /\ x e. A ) -> ( B C_ G -> E. y e. C B C_ D ) )
37 12 36 mpd 
 |-  ( ( ph /\ x e. A ) -> E. y e. C B C_ D )
38 37 ex 
 |-  ( ph -> ( x e. A -> E. y e. C B C_ D ) )
39 1 38 ralrimi 
 |-  ( ph -> A. x e. A E. y e. C B C_ D )
40 ssel 
 |-  ( B C_ D -> ( z e. B -> z e. D ) )
41 40 reximi 
 |-  ( E. y e. C B C_ D -> E. y e. C ( z e. B -> z e. D ) )
42 5 nfcri 
 |-  F/ y z e. B
43 42 r19.37 
 |-  ( E. y e. C ( z e. B -> z e. D ) -> ( z e. B -> E. y e. C z e. D ) )
44 41 43 syl 
 |-  ( E. y e. C B C_ D -> ( z e. B -> E. y e. C z e. D ) )
45 eliun 
 |-  ( z e. U_ y e. C D <-> E. y e. C z e. D )
46 44 45 syl6ibr 
 |-  ( E. y e. C B C_ D -> ( z e. B -> z e. U_ y e. C D ) )
47 46 ssrdv 
 |-  ( E. y e. C B C_ D -> B C_ U_ y e. C D )
48 47 ralimi 
 |-  ( A. x e. A E. y e. C B C_ D -> A. x e. A B C_ U_ y e. C D )
49 df-iun 
 |-  U_ x e. A B = { z | E. x e. A z e. B }
50 49 sseq1i 
 |-  ( U_ x e. A B C_ U_ y e. C D <-> { z | E. x e. A z e. B } C_ U_ y e. C D )
51 abss 
 |-  ( { z | E. x e. A z e. B } C_ U_ y e. C D <-> A. z ( E. x e. A z e. B -> z e. U_ y e. C D ) )
52 dfss2 
 |-  ( B C_ U_ y e. C D <-> A. z ( z e. B -> z e. U_ y e. C D ) )
53 52 ralbii 
 |-  ( A. x e. A B C_ U_ y e. C D <-> A. x e. A A. z ( z e. B -> z e. U_ y e. C D ) )
54 ralcom4 
 |-  ( A. x e. A A. z ( z e. B -> z e. U_ y e. C D ) <-> A. z A. x e. A ( z e. B -> z e. U_ y e. C D ) )
55 6 8 nfiun 
 |-  F/_ x U_ y e. C D
56 55 nfcri 
 |-  F/ x z e. U_ y e. C D
57 56 r19.23 
 |-  ( A. x e. A ( z e. B -> z e. U_ y e. C D ) <-> ( E. x e. A z e. B -> z e. U_ y e. C D ) )
58 57 albii 
 |-  ( A. z A. x e. A ( z e. B -> z e. U_ y e. C D ) <-> A. z ( E. x e. A z e. B -> z e. U_ y e. C D ) )
59 53 54 58 3bitrri 
 |-  ( A. z ( E. x e. A z e. B -> z e. U_ y e. C D ) <-> A. x e. A B C_ U_ y e. C D )
60 50 51 59 3bitri 
 |-  ( U_ x e. A B C_ U_ y e. C D <-> A. x e. A B C_ U_ y e. C D )
61 48 60 sylibr 
 |-  ( A. x e. A E. y e. C B C_ D -> U_ x e. A B C_ U_ y e. C D )
62 39 61 syl 
 |-  ( ph -> U_ x e. A B C_ U_ y e. C D )