Metamath Proof Explorer

Theorem fiinfi

Description: If two classes have the finite intersection property, then so does their intersection. (Contributed by RP, 1-Jan-2020)

Ref Expression
Hypotheses fiinfi.a 
|- ( ph -> A. x e. A A. y e. A ( x i^i y ) e. A )
fiinfi.b 
|- ( ph -> A. x e. B A. y e. B ( x i^i y ) e. B )
fiinfi.c 
|- ( ph -> C = ( A i^i B ) )
Assertion fiinfi 
|- ( ph -> A. x e. C A. y e. C ( x i^i y ) e. C )

Proof

Step Hyp Ref Expression
1 fiinfi.a 
 |-  ( ph -> A. x e. A A. y e. A ( x i^i y ) e. A )
2 fiinfi.b 
 |-  ( ph -> A. x e. B A. y e. B ( x i^i y ) e. B )
3 fiinfi.c 
 |-  ( ph -> C = ( A i^i B ) )
4 elinel1 
 |-  ( x e. ( A i^i B ) -> x e. A )
5 elinel1 
 |-  ( y e. ( A i^i B ) -> y e. A )
6 5 imim1i 
 |-  ( ( y e. A -> ( x i^i y ) e. A ) -> ( y e. ( A i^i B ) -> ( x i^i y ) e. A ) )
7 6 ralimi2 
 |-  ( A. y e. A ( x i^i y ) e. A -> A. y e. ( A i^i B ) ( x i^i y ) e. A )
8 4 7 imim12i 
 |-  ( ( x e. A -> A. y e. A ( x i^i y ) e. A ) -> ( x e. ( A i^i B ) -> A. y e. ( A i^i B ) ( x i^i y ) e. A ) )
9 8 ralimi2 
 |-  ( A. x e. A A. y e. A ( x i^i y ) e. A -> A. x e. ( A i^i B ) A. y e. ( A i^i B ) ( x i^i y ) e. A )
10 1 9 syl 
 |-  ( ph -> A. x e. ( A i^i B ) A. y e. ( A i^i B ) ( x i^i y ) e. A )
11 elinel2 
 |-  ( x e. ( A i^i B ) -> x e. B )
12 elinel2 
 |-  ( y e. ( A i^i B ) -> y e. B )
13 12 imim1i 
 |-  ( ( y e. B -> ( x i^i y ) e. B ) -> ( y e. ( A i^i B ) -> ( x i^i y ) e. B ) )
14 13 ralimi2 
 |-  ( A. y e. B ( x i^i y ) e. B -> A. y e. ( A i^i B ) ( x i^i y ) e. B )
15 11 14 imim12i 
 |-  ( ( x e. B -> A. y e. B ( x i^i y ) e. B ) -> ( x e. ( A i^i B ) -> A. y e. ( A i^i B ) ( x i^i y ) e. B ) )
16 15 ralimi2 
 |-  ( A. x e. B A. y e. B ( x i^i y ) e. B -> A. x e. ( A i^i B ) A. y e. ( A i^i B ) ( x i^i y ) e. B )
17 2 16 syl 
 |-  ( ph -> A. x e. ( A i^i B ) A. y e. ( A i^i B ) ( x i^i y ) e. B )
18 r19.26-2 
 |-  ( A. x e. ( A i^i B ) A. y e. ( A i^i B ) ( ( x i^i y ) e. A /\ ( x i^i y ) e. B ) <-> ( A. x e. ( A i^i B ) A. y e. ( A i^i B ) ( x i^i y ) e. A /\ A. x e. ( A i^i B ) A. y e. ( A i^i B ) ( x i^i y ) e. B ) )
19 10 17 18 sylanbrc 
 |-  ( ph -> A. x e. ( A i^i B ) A. y e. ( A i^i B ) ( ( x i^i y ) e. A /\ ( x i^i y ) e. B ) )
20 elin 
 |-  ( ( x i^i y ) e. ( A i^i B ) <-> ( ( x i^i y ) e. A /\ ( x i^i y ) e. B ) )
21 20 2ralbii 
 |-  ( A. x e. ( A i^i B ) A. y e. ( A i^i B ) ( x i^i y ) e. ( A i^i B ) <-> A. x e. ( A i^i B ) A. y e. ( A i^i B ) ( ( x i^i y ) e. A /\ ( x i^i y ) e. B ) )
22 19 21 sylibr 
 |-  ( ph -> A. x e. ( A i^i B ) A. y e. ( A i^i B ) ( x i^i y ) e. ( A i^i B ) )
23 3 eleq2d 
 |-  ( ph -> ( ( x i^i y ) e. C <-> ( x i^i y ) e. ( A i^i B ) ) )
24 23 ralbidv 
 |-  ( ph -> ( A. y e. ( A i^i B ) ( x i^i y ) e. C <-> A. y e. ( A i^i B ) ( x i^i y ) e. ( A i^i B ) ) )
25 24 ralbidv 
 |-  ( ph -> ( A. x e. ( A i^i B ) A. y e. ( A i^i B ) ( x i^i y ) e. C <-> A. x e. ( A i^i B ) A. y e. ( A i^i B ) ( x i^i y ) e. ( A i^i B ) ) )
26 22 25 mpbird 
 |-  ( ph -> A. x e. ( A i^i B ) A. y e. ( A i^i B ) ( x i^i y ) e. C )
27 3 raleqdv 
 |-  ( ph -> ( A. y e. C ( x i^i y ) e. C <-> A. y e. ( A i^i B ) ( x i^i y ) e. C ) )
28 27 ralbidv 
 |-  ( ph -> ( A. x e. ( A i^i B ) A. y e. C ( x i^i y ) e. C <-> A. x e. ( A i^i B ) A. y e. ( A i^i B ) ( x i^i y ) e. C ) )
29 26 28 mpbird 
 |-  ( ph -> A. x e. ( A i^i B ) A. y e. C ( x i^i y ) e. C )
30 3 raleqdv 
 |-  ( ph -> ( A. x e. C A. y e. C ( x i^i y ) e. C <-> A. x e. ( A i^i B ) A. y e. C ( x i^i y ) e. C ) )
31 29 30 mpbird 
 |-  ( ph -> A. x e. C A. y e. C ( x i^i y ) e. C )