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 ( 𝜑 → ∀ 𝑥𝐴𝑦𝐴 ( 𝑥𝑦 ) ∈ 𝐴 )
fiinfi.b ( 𝜑 → ∀ 𝑥𝐵𝑦𝐵 ( 𝑥𝑦 ) ∈ 𝐵 )
fiinfi.c ( 𝜑𝐶 = ( 𝐴𝐵 ) )
Assertion fiinfi ( 𝜑 → ∀ 𝑥𝐶𝑦𝐶 ( 𝑥𝑦 ) ∈ 𝐶 )

Proof

Step Hyp Ref Expression
1 fiinfi.a ( 𝜑 → ∀ 𝑥𝐴𝑦𝐴 ( 𝑥𝑦 ) ∈ 𝐴 )
2 fiinfi.b ( 𝜑 → ∀ 𝑥𝐵𝑦𝐵 ( 𝑥𝑦 ) ∈ 𝐵 )
3 fiinfi.c ( 𝜑𝐶 = ( 𝐴𝐵 ) )
4 elinel1 ( 𝑥 ∈ ( 𝐴𝐵 ) → 𝑥𝐴 )
5 elinel1 ( 𝑦 ∈ ( 𝐴𝐵 ) → 𝑦𝐴 )
6 5 imim1i ( ( 𝑦𝐴 → ( 𝑥𝑦 ) ∈ 𝐴 ) → ( 𝑦 ∈ ( 𝐴𝐵 ) → ( 𝑥𝑦 ) ∈ 𝐴 ) )
7 6 ralimi2 ( ∀ 𝑦𝐴 ( 𝑥𝑦 ) ∈ 𝐴 → ∀ 𝑦 ∈ ( 𝐴𝐵 ) ( 𝑥𝑦 ) ∈ 𝐴 )
8 4 7 imim12i ( ( 𝑥𝐴 → ∀ 𝑦𝐴 ( 𝑥𝑦 ) ∈ 𝐴 ) → ( 𝑥 ∈ ( 𝐴𝐵 ) → ∀ 𝑦 ∈ ( 𝐴𝐵 ) ( 𝑥𝑦 ) ∈ 𝐴 ) )
9 8 ralimi2 ( ∀ 𝑥𝐴𝑦𝐴 ( 𝑥𝑦 ) ∈ 𝐴 → ∀ 𝑥 ∈ ( 𝐴𝐵 ) ∀ 𝑦 ∈ ( 𝐴𝐵 ) ( 𝑥𝑦 ) ∈ 𝐴 )
10 1 9 syl ( 𝜑 → ∀ 𝑥 ∈ ( 𝐴𝐵 ) ∀ 𝑦 ∈ ( 𝐴𝐵 ) ( 𝑥𝑦 ) ∈ 𝐴 )
11 elinel2 ( 𝑥 ∈ ( 𝐴𝐵 ) → 𝑥𝐵 )
12 elinel2 ( 𝑦 ∈ ( 𝐴𝐵 ) → 𝑦𝐵 )
13 12 imim1i ( ( 𝑦𝐵 → ( 𝑥𝑦 ) ∈ 𝐵 ) → ( 𝑦 ∈ ( 𝐴𝐵 ) → ( 𝑥𝑦 ) ∈ 𝐵 ) )
14 13 ralimi2 ( ∀ 𝑦𝐵 ( 𝑥𝑦 ) ∈ 𝐵 → ∀ 𝑦 ∈ ( 𝐴𝐵 ) ( 𝑥𝑦 ) ∈ 𝐵 )
15 11 14 imim12i ( ( 𝑥𝐵 → ∀ 𝑦𝐵 ( 𝑥𝑦 ) ∈ 𝐵 ) → ( 𝑥 ∈ ( 𝐴𝐵 ) → ∀ 𝑦 ∈ ( 𝐴𝐵 ) ( 𝑥𝑦 ) ∈ 𝐵 ) )
16 15 ralimi2 ( ∀ 𝑥𝐵𝑦𝐵 ( 𝑥𝑦 ) ∈ 𝐵 → ∀ 𝑥 ∈ ( 𝐴𝐵 ) ∀ 𝑦 ∈ ( 𝐴𝐵 ) ( 𝑥𝑦 ) ∈ 𝐵 )
17 2 16 syl ( 𝜑 → ∀ 𝑥 ∈ ( 𝐴𝐵 ) ∀ 𝑦 ∈ ( 𝐴𝐵 ) ( 𝑥𝑦 ) ∈ 𝐵 )
18 r19.26-2 ( ∀ 𝑥 ∈ ( 𝐴𝐵 ) ∀ 𝑦 ∈ ( 𝐴𝐵 ) ( ( 𝑥𝑦 ) ∈ 𝐴 ∧ ( 𝑥𝑦 ) ∈ 𝐵 ) ↔ ( ∀ 𝑥 ∈ ( 𝐴𝐵 ) ∀ 𝑦 ∈ ( 𝐴𝐵 ) ( 𝑥𝑦 ) ∈ 𝐴 ∧ ∀ 𝑥 ∈ ( 𝐴𝐵 ) ∀ 𝑦 ∈ ( 𝐴𝐵 ) ( 𝑥𝑦 ) ∈ 𝐵 ) )
19 10 17 18 sylanbrc ( 𝜑 → ∀ 𝑥 ∈ ( 𝐴𝐵 ) ∀ 𝑦 ∈ ( 𝐴𝐵 ) ( ( 𝑥𝑦 ) ∈ 𝐴 ∧ ( 𝑥𝑦 ) ∈ 𝐵 ) )
20 elin ( ( 𝑥𝑦 ) ∈ ( 𝐴𝐵 ) ↔ ( ( 𝑥𝑦 ) ∈ 𝐴 ∧ ( 𝑥𝑦 ) ∈ 𝐵 ) )
21 20 2ralbii ( ∀ 𝑥 ∈ ( 𝐴𝐵 ) ∀ 𝑦 ∈ ( 𝐴𝐵 ) ( 𝑥𝑦 ) ∈ ( 𝐴𝐵 ) ↔ ∀ 𝑥 ∈ ( 𝐴𝐵 ) ∀ 𝑦 ∈ ( 𝐴𝐵 ) ( ( 𝑥𝑦 ) ∈ 𝐴 ∧ ( 𝑥𝑦 ) ∈ 𝐵 ) )
22 19 21 sylibr ( 𝜑 → ∀ 𝑥 ∈ ( 𝐴𝐵 ) ∀ 𝑦 ∈ ( 𝐴𝐵 ) ( 𝑥𝑦 ) ∈ ( 𝐴𝐵 ) )
23 3 eleq2d ( 𝜑 → ( ( 𝑥𝑦 ) ∈ 𝐶 ↔ ( 𝑥𝑦 ) ∈ ( 𝐴𝐵 ) ) )
24 23 ralbidv ( 𝜑 → ( ∀ 𝑦 ∈ ( 𝐴𝐵 ) ( 𝑥𝑦 ) ∈ 𝐶 ↔ ∀ 𝑦 ∈ ( 𝐴𝐵 ) ( 𝑥𝑦 ) ∈ ( 𝐴𝐵 ) ) )
25 24 ralbidv ( 𝜑 → ( ∀ 𝑥 ∈ ( 𝐴𝐵 ) ∀ 𝑦 ∈ ( 𝐴𝐵 ) ( 𝑥𝑦 ) ∈ 𝐶 ↔ ∀ 𝑥 ∈ ( 𝐴𝐵 ) ∀ 𝑦 ∈ ( 𝐴𝐵 ) ( 𝑥𝑦 ) ∈ ( 𝐴𝐵 ) ) )
26 22 25 mpbird ( 𝜑 → ∀ 𝑥 ∈ ( 𝐴𝐵 ) ∀ 𝑦 ∈ ( 𝐴𝐵 ) ( 𝑥𝑦 ) ∈ 𝐶 )
27 3 raleqdv ( 𝜑 → ( ∀ 𝑦𝐶 ( 𝑥𝑦 ) ∈ 𝐶 ↔ ∀ 𝑦 ∈ ( 𝐴𝐵 ) ( 𝑥𝑦 ) ∈ 𝐶 ) )
28 27 ralbidv ( 𝜑 → ( ∀ 𝑥 ∈ ( 𝐴𝐵 ) ∀ 𝑦𝐶 ( 𝑥𝑦 ) ∈ 𝐶 ↔ ∀ 𝑥 ∈ ( 𝐴𝐵 ) ∀ 𝑦 ∈ ( 𝐴𝐵 ) ( 𝑥𝑦 ) ∈ 𝐶 ) )
29 26 28 mpbird ( 𝜑 → ∀ 𝑥 ∈ ( 𝐴𝐵 ) ∀ 𝑦𝐶 ( 𝑥𝑦 ) ∈ 𝐶 )
30 3 raleqdv ( 𝜑 → ( ∀ 𝑥𝐶𝑦𝐶 ( 𝑥𝑦 ) ∈ 𝐶 ↔ ∀ 𝑥 ∈ ( 𝐴𝐵 ) ∀ 𝑦𝐶 ( 𝑥𝑦 ) ∈ 𝐶 ) )
31 29 30 mpbird ( 𝜑 → ∀ 𝑥𝐶𝑦𝐶 ( 𝑥𝑦 ) ∈ 𝐶 )