This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iinss2d

Description: Subset implication for an indexed intersection. (Contributed by Glauco Siliprandi, 24-Jan-2025)

Ref Expression
Hypotheses iinss2d.1 
|- F/ x ph
iinss2d.2 
|- F/_ x A
iinss2d.3 
|- F/_ x C
iinss2d.4 
|- ( ph -> A =/= (/) )
iinss2d.5 
|- ( ( ph /\ x e. A ) -> B C_ C )
Assertion iinss2d 
|- ( ph -> |^|_ x e. A B C_ C )

Proof

Step Hyp Ref Expression
1 iinss2d.1 
 |-  F/ x ph
2 iinss2d.2 
 |-  F/_ x A
3 iinss2d.3 
 |-  F/_ x C
4 iinss2d.4 
 |-  ( ph -> A =/= (/) )
5 iinss2d.5 
 |-  ( ( ph /\ x e. A ) -> B C_ C )
6 5 3adant3 
 |-  ( ( ph /\ x e. A /\ T. ) -> B C_ C )
7 2 n0f 
 |-  ( A =/= (/) <-> E. x x e. A )
8 4 7 sylib 
 |-  ( ph -> E. x x e. A )
9 rextru 
 |-  ( E. x x e. A <-> E. x e. A T. )
10 8 9 sylib 
 |-  ( ph -> E. x e. A T. )
11 1 6 10 reximdd 
 |-  ( ph -> E. x e. A B C_ C )
12 3 iinssf 
 |-  ( E. x e. A B C_ C -> |^|_ x e. A B C_ C )
13 11 12 syl 
 |-  ( ph -> |^|_ x e. A B C_ C )