Description: Subset relationship for an indexed union. (Contributed by Thierry Arnoux, 31-Dec-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ssiun2sf.1 | |
|
ssiun2sf.2 | |
||
ssiun2sf.3 | |
||
ssiun2sf.4 | |
||
Assertion | ssiun2sf | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssiun2sf.1 | |
|
2 | ssiun2sf.2 | |
|
3 | ssiun2sf.3 | |
|
4 | ssiun2sf.4 | |
|
5 | 2 1 | nfel | |
6 | nfiu1 | |
|
7 | 3 6 | nfss | |
8 | 5 7 | nfim | |
9 | eleq1 | |
|
10 | 4 | sseq1d | |
11 | 9 10 | imbi12d | |
12 | ssiun2 | |
|
13 | 2 8 11 12 | vtoclgf | |
14 | 13 | pm2.43i | |