Metamath Proof Explorer

Theorem dffi2

Description: The set of finite intersections is the smallest set that contains A and is closed under pairwise intersection. (Contributed by Mario Carneiro, 24-Nov-2013)

Ref Expression
Assertion dffi2 
|- ( A e. V -> ( fi ` A ) = |^| { z | ( A C_ z /\ A. x e. z A. y e. z ( x i^i y ) e. z ) } )

Proof

Step Hyp Ref Expression
1 elex 
 |-  ( A e. V -> A e. _V )
2 vex 
 |-  t e. _V
3 elfi 
 |-  ( ( t e. _V /\ A e. _V ) -> ( t e. ( fi ` A ) <-> E. x e. ( ~P A i^i Fin ) t = |^| x ) )
4 2 3 mpan 
 |-  ( A e. _V -> ( t e. ( fi ` A ) <-> E. x e. ( ~P A i^i Fin ) t = |^| x ) )
5 4 biimpd 
 |-  ( A e. _V -> ( t e. ( fi ` A ) -> E. x e. ( ~P A i^i Fin ) t = |^| x ) )
6 df-rex 
 |-  ( E. x e. ( ~P A i^i Fin ) t = |^| x <-> E. x ( x e. ( ~P A i^i Fin ) /\ t = |^| x ) )
7 fiint 
 |-  ( A. x e. z A. y e. z ( x i^i y ) e. z <-> A. x ( ( x C_ z /\ x =/= (/) /\ x e. Fin ) -> |^| x e. z ) )
8 elinel1 
 |-  ( x e. ( ~P A i^i Fin ) -> x e. ~P A )
9 8 elpwid 
 |-  ( x e. ( ~P A i^i Fin ) -> x C_ A )
10 9 3ad2ant2 
 |-  ( ( A C_ z /\ x e. ( ~P A i^i Fin ) /\ t = |^| x ) -> x C_ A )
11 simp1 
 |-  ( ( A C_ z /\ x e. ( ~P A i^i Fin ) /\ t = |^| x ) -> A C_ z )
12 10 11 sstrd 
 |-  ( ( A C_ z /\ x e. ( ~P A i^i Fin ) /\ t = |^| x ) -> x C_ z )
13 eqvisset 
 |-  ( t = |^| x -> |^| x e. _V )
14 intex 
 |-  ( x =/= (/) <-> |^| x e. _V )
15 13 14 sylibr 
 |-  ( t = |^| x -> x =/= (/) )
16 15 3ad2ant3 
 |-  ( ( A C_ z /\ x e. ( ~P A i^i Fin ) /\ t = |^| x ) -> x =/= (/) )
17 elinel2 
 |-  ( x e. ( ~P A i^i Fin ) -> x e. Fin )
18 17 3ad2ant2 
 |-  ( ( A C_ z /\ x e. ( ~P A i^i Fin ) /\ t = |^| x ) -> x e. Fin )
19 12 16 18 3jca 
 |-  ( ( A C_ z /\ x e. ( ~P A i^i Fin ) /\ t = |^| x ) -> ( x C_ z /\ x =/= (/) /\ x e. Fin ) )
20 19 3expib 
 |-  ( A C_ z -> ( ( x e. ( ~P A i^i Fin ) /\ t = |^| x ) -> ( x C_ z /\ x =/= (/) /\ x e. Fin ) ) )
21 pm2.27 
 |-  ( ( x C_ z /\ x =/= (/) /\ x e. Fin ) -> ( ( ( x C_ z /\ x =/= (/) /\ x e. Fin ) -> |^| x e. z ) -> |^| x e. z ) )
22 20 21 syl6 
 |-  ( A C_ z -> ( ( x e. ( ~P A i^i Fin ) /\ t = |^| x ) -> ( ( ( x C_ z /\ x =/= (/) /\ x e. Fin ) -> |^| x e. z ) -> |^| x e. z ) ) )
23 eleq1 
 |-  ( t = |^| x -> ( t e. z <-> |^| x e. z ) )
24 23 biimprd 
 |-  ( t = |^| x -> ( |^| x e. z -> t e. z ) )
25 24 adantl 
 |-  ( ( x e. ( ~P A i^i Fin ) /\ t = |^| x ) -> ( |^| x e. z -> t e. z ) )
26 25 a1i 
 |-  ( A C_ z -> ( ( x e. ( ~P A i^i Fin ) /\ t = |^| x ) -> ( |^| x e. z -> t e. z ) ) )
27 22 26 syldd 
 |-  ( A C_ z -> ( ( x e. ( ~P A i^i Fin ) /\ t = |^| x ) -> ( ( ( x C_ z /\ x =/= (/) /\ x e. Fin ) -> |^| x e. z ) -> t e. z ) ) )
28 27 com23 
 |-  ( A C_ z -> ( ( ( x C_ z /\ x =/= (/) /\ x e. Fin ) -> |^| x e. z ) -> ( ( x e. ( ~P A i^i Fin ) /\ t = |^| x ) -> t e. z ) ) )
29 28 alimdv 
 |-  ( A C_ z -> ( A. x ( ( x C_ z /\ x =/= (/) /\ x e. Fin ) -> |^| x e. z ) -> A. x ( ( x e. ( ~P A i^i Fin ) /\ t = |^| x ) -> t e. z ) ) )
30 7 29 biimtrid 
 |-  ( A C_ z -> ( A. x e. z A. y e. z ( x i^i y ) e. z -> A. x ( ( x e. ( ~P A i^i Fin ) /\ t = |^| x ) -> t e. z ) ) )
31 30 imp 
 |-  ( ( A C_ z /\ A. x e. z A. y e. z ( x i^i y ) e. z ) -> A. x ( ( x e. ( ~P A i^i Fin ) /\ t = |^| x ) -> t e. z ) )
32 19.23v 
 |-  ( A. x ( ( x e. ( ~P A i^i Fin ) /\ t = |^| x ) -> t e. z ) <-> ( E. x ( x e. ( ~P A i^i Fin ) /\ t = |^| x ) -> t e. z ) )
33 31 32 sylib 
 |-  ( ( A C_ z /\ A. x e. z A. y e. z ( x i^i y ) e. z ) -> ( E. x ( x e. ( ~P A i^i Fin ) /\ t = |^| x ) -> t e. z ) )
34 6 33 biimtrid 
 |-  ( ( A C_ z /\ A. x e. z A. y e. z ( x i^i y ) e. z ) -> ( E. x e. ( ~P A i^i Fin ) t = |^| x -> t e. z ) )
35 5 34 sylan9 
 |-  ( ( A e. _V /\ ( A C_ z /\ A. x e. z A. y e. z ( x i^i y ) e. z ) ) -> ( t e. ( fi ` A ) -> t e. z ) )
36 35 ssrdv 
 |-  ( ( A e. _V /\ ( A C_ z /\ A. x e. z A. y e. z ( x i^i y ) e. z ) ) -> ( fi ` A ) C_ z )
37 36 ex 
 |-  ( A e. _V -> ( ( A C_ z /\ A. x e. z A. y e. z ( x i^i y ) e. z ) -> ( fi ` A ) C_ z ) )
38 37 alrimiv 
 |-  ( A e. _V -> A. z ( ( A C_ z /\ A. x e. z A. y e. z ( x i^i y ) e. z ) -> ( fi ` A ) C_ z ) )
39 ssintab 
 |-  ( ( fi ` A ) C_ |^| { z | ( A C_ z /\ A. x e. z A. y e. z ( x i^i y ) e. z ) } <-> A. z ( ( A C_ z /\ A. x e. z A. y e. z ( x i^i y ) e. z ) -> ( fi ` A ) C_ z ) )
40 38 39 sylibr 
 |-  ( A e. _V -> ( fi ` A ) C_ |^| { z | ( A C_ z /\ A. x e. z A. y e. z ( x i^i y ) e. z ) } )
41 ssfii 
 |-  ( A e. _V -> A C_ ( fi ` A ) )
42 fiin 
 |-  ( ( x e. ( fi ` A ) /\ y e. ( fi ` A ) ) -> ( x i^i y ) e. ( fi ` A ) )
43 42 rgen2 
 |-  A. x e. ( fi ` A ) A. y e. ( fi ` A ) ( x i^i y ) e. ( fi ` A )
44 fvex 
 |-  ( fi ` A ) e. _V
45 sseq2 
 |-  ( z = ( fi ` A ) -> ( A C_ z <-> A C_ ( fi ` A ) ) )
46 eleq2 
 |-  ( z = ( fi ` A ) -> ( ( x i^i y ) e. z <-> ( x i^i y ) e. ( fi ` A ) ) )
47 46 raleqbi1dv 
 |-  ( z = ( fi ` A ) -> ( A. y e. z ( x i^i y ) e. z <-> A. y e. ( fi ` A ) ( x i^i y ) e. ( fi ` A ) ) )
48 47 raleqbi1dv 
 |-  ( z = ( fi ` A ) -> ( A. x e. z A. y e. z ( x i^i y ) e. z <-> A. x e. ( fi ` A ) A. y e. ( fi ` A ) ( x i^i y ) e. ( fi ` A ) ) )
49 45 48 anbi12d 
 |-  ( z = ( fi ` A ) -> ( ( A C_ z /\ A. x e. z A. y e. z ( x i^i y ) e. z ) <-> ( A C_ ( fi ` A ) /\ A. x e. ( fi ` A ) A. y e. ( fi ` A ) ( x i^i y ) e. ( fi ` A ) ) ) )
50 44 49 elab 
 |-  ( ( fi ` A ) e. { z | ( A C_ z /\ A. x e. z A. y e. z ( x i^i y ) e. z ) } <-> ( A C_ ( fi ` A ) /\ A. x e. ( fi ` A ) A. y e. ( fi ` A ) ( x i^i y ) e. ( fi ` A ) ) )
51 41 43 50 sylanblrc 
 |-  ( A e. _V -> ( fi ` A ) e. { z | ( A C_ z /\ A. x e. z A. y e. z ( x i^i y ) e. z ) } )
52 intss1 
 |-  ( ( fi ` A ) e. { z | ( A C_ z /\ A. x e. z A. y e. z ( x i^i y ) e. z ) } -> |^| { z | ( A C_ z /\ A. x e. z A. y e. z ( x i^i y ) e. z ) } C_ ( fi ` A ) )
53 51 52 syl 
 |-  ( A e. _V -> |^| { z | ( A C_ z /\ A. x e. z A. y e. z ( x i^i y ) e. z ) } C_ ( fi ` A ) )
54 40 53 eqssd 
 |-  ( A e. _V -> ( fi ` A ) = |^| { z | ( A C_ z /\ A. x e. z A. y e. z ( x i^i y ) e. z ) } )
55 1 54 syl 
 |-  ( A e. V -> ( fi ` A ) = |^| { z | ( A C_ z /\ A. x e. z A. y e. z ( x i^i y ) e. z ) } )