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 biimtrid 
 |-  ( ( 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 imbitrrdi 
 |-  ( ( 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 1 37 ralrimia 
 |-  ( ph -> A. x e. A E. y e. C B C_ D )
39 ssel 
 |-  ( B C_ D -> ( z e. B -> z e. D ) )
40 39 reximi 
 |-  ( E. y e. C B C_ D -> E. y e. C ( z e. B -> z e. D ) )
41 5 nfcri 
 |-  F/ y z e. B
42 41 r19.37 
 |-  ( E. y e. C ( z e. B -> z e. D ) -> ( z e. B -> E. y e. C z e. D ) )
43 40 42 syl 
 |-  ( E. y e. C B C_ D -> ( z e. B -> E. y e. C z e. D ) )
44 eliun 
 |-  ( z e. U_ y e. C D <-> E. y e. C z e. D )
45 43 44 imbitrrdi 
 |-  ( E. y e. C B C_ D -> ( z e. B -> z e. U_ y e. C D ) )
46 45 ssrdv 
 |-  ( E. y e. C B C_ D -> B C_ U_ y e. C D )
47 46 ralimi 
 |-  ( A. x e. A E. y e. C B C_ D -> A. x e. A B C_ U_ y e. C D )
48 6 8 nfiun 
 |-  F/_ x U_ y e. C D
49 48 iunssf 
 |-  ( U_ x e. A B C_ U_ y e. C D <-> A. x e. A B C_ U_ y e. C D )
50 47 49 sylibr 
 |-  ( A. x e. A E. y e. C B C_ D -> U_ x e. A B C_ U_ y e. C D )
51 38 50 syl 
 |-  ( ph -> U_ x e. A B C_ U_ y e. C D )