Metamath Proof Explorer

Theorem fiin

Description: The elements of ( fiC ) are closed under finite intersection. (Contributed by Mario Carneiro, 24-Nov-2013)

Ref Expression
Assertion fiin ( ( 𝐴 ∈ ( fi ‘ 𝐶 ) ∧ 𝐵 ∈ ( fi ‘ 𝐶 ) ) → ( 𝐴 ∩ 𝐵 ) ∈ ( fi ‘ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 elfvex ⊢ ( 𝐴 ∈ ( fi ‘ 𝐶 ) → 𝐶 ∈ V )
2 elfi ⊢ ( ( 𝐴 ∈ ( fi ‘ 𝐶 ) ∧ 𝐶 ∈ V ) → ( 𝐴 ∈ ( fi ‘ 𝐶 ) ↔ ∃ 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) 𝐴 = ∩ 𝑥 ) )
3 1 2 mpdan ⊢ ( 𝐴 ∈ ( fi ‘ 𝐶 ) → ( 𝐴 ∈ ( fi ‘ 𝐶 ) ↔ ∃ 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) 𝐴 = ∩ 𝑥 ) )
4 3 ibi ⊢ ( 𝐴 ∈ ( fi ‘ 𝐶 ) → ∃ 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) 𝐴 = ∩ 𝑥 )
5 4 adantr ⊢ ( ( 𝐴 ∈ ( fi ‘ 𝐶 ) ∧ 𝐵 ∈ ( fi ‘ 𝐶 ) ) → ∃ 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) 𝐴 = ∩ 𝑥 )
6 simpr ⊢ ( ( 𝐴 ∈ ( fi ‘ 𝐶 ) ∧ 𝐵 ∈ ( fi ‘ 𝐶 ) ) → 𝐵 ∈ ( fi ‘ 𝐶 ) )
7 elfi ⊢ ( ( 𝐵 ∈ ( fi ‘ 𝐶 ) ∧ 𝐶 ∈ V ) → ( 𝐵 ∈ ( fi ‘ 𝐶 ) ↔ ∃ 𝑦 ∈ ( 𝒫 𝐶 ∩ Fin ) 𝐵 = ∩ 𝑦 ) )
8 7 ancoms ⊢ ( ( 𝐶 ∈ V ∧ 𝐵 ∈ ( fi ‘ 𝐶 ) ) → ( 𝐵 ∈ ( fi ‘ 𝐶 ) ↔ ∃ 𝑦 ∈ ( 𝒫 𝐶 ∩ Fin ) 𝐵 = ∩ 𝑦 ) )
9 1 8 sylan ⊢ ( ( 𝐴 ∈ ( fi ‘ 𝐶 ) ∧ 𝐵 ∈ ( fi ‘ 𝐶 ) ) → ( 𝐵 ∈ ( fi ‘ 𝐶 ) ↔ ∃ 𝑦 ∈ ( 𝒫 𝐶 ∩ Fin ) 𝐵 = ∩ 𝑦 ) )
10 6 9 mpbid ⊢ ( ( 𝐴 ∈ ( fi ‘ 𝐶 ) ∧ 𝐵 ∈ ( fi ‘ 𝐶 ) ) → ∃ 𝑦 ∈ ( 𝒫 𝐶 ∩ Fin ) 𝐵 = ∩ 𝑦 )
11 elin ⊢ ( 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ↔ ( 𝑥 ∈ 𝒫 𝐶 ∧ 𝑥 ∈ Fin ) )
12 elin ⊢ ( 𝑦 ∈ ( 𝒫 𝐶 ∩ Fin ) ↔ ( 𝑦 ∈ 𝒫 𝐶 ∧ 𝑦 ∈ Fin ) )
13 pwuncl ⊢ ( ( 𝑥 ∈ 𝒫 𝐶 ∧ 𝑦 ∈ 𝒫 𝐶 ) → ( 𝑥 ∪ 𝑦 ) ∈ 𝒫 𝐶 )
14 unfi ⊢ ( ( 𝑥 ∈ Fin ∧ 𝑦 ∈ Fin ) → ( 𝑥 ∪ 𝑦 ) ∈ Fin )
15 13 14 anim12i ⊢ ( ( ( 𝑥 ∈ 𝒫 𝐶 ∧ 𝑦 ∈ 𝒫 𝐶 ) ∧ ( 𝑥 ∈ Fin ∧ 𝑦 ∈ Fin ) ) → ( ( 𝑥 ∪ 𝑦 ) ∈ 𝒫 𝐶 ∧ ( 𝑥 ∪ 𝑦 ) ∈ Fin ) )
16 15 an4s ⊢ ( ( ( 𝑥 ∈ 𝒫 𝐶 ∧ 𝑥 ∈ Fin ) ∧ ( 𝑦 ∈ 𝒫 𝐶 ∧ 𝑦 ∈ Fin ) ) → ( ( 𝑥 ∪ 𝑦 ) ∈ 𝒫 𝐶 ∧ ( 𝑥 ∪ 𝑦 ) ∈ Fin ) )
17 11 12 16 syl2anb ⊢ ( ( 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ∧ 𝑦 ∈ ( 𝒫 𝐶 ∩ Fin ) ) → ( ( 𝑥 ∪ 𝑦 ) ∈ 𝒫 𝐶 ∧ ( 𝑥 ∪ 𝑦 ) ∈ Fin ) )
18 elin ⊢ ( ( 𝑥 ∪ 𝑦 ) ∈ ( 𝒫 𝐶 ∩ Fin ) ↔ ( ( 𝑥 ∪ 𝑦 ) ∈ 𝒫 𝐶 ∧ ( 𝑥 ∪ 𝑦 ) ∈ Fin ) )
19 17 18 sylibr ⊢ ( ( 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ∧ 𝑦 ∈ ( 𝒫 𝐶 ∩ Fin ) ) → ( 𝑥 ∪ 𝑦 ) ∈ ( 𝒫 𝐶 ∩ Fin ) )
20 ineq12 ⊢ ( ( 𝐴 = ∩ 𝑥 ∧ 𝐵 = ∩ 𝑦 ) → ( 𝐴 ∩ 𝐵 ) = ( ∩ 𝑥 ∩ ∩ 𝑦 ) )
21 intun ⊢ ∩ ( 𝑥 ∪ 𝑦 ) = ( ∩ 𝑥 ∩ ∩ 𝑦 )
22 20 21 eqtr4di ⊢ ( ( 𝐴 = ∩ 𝑥 ∧ 𝐵 = ∩ 𝑦 ) → ( 𝐴 ∩ 𝐵 ) = ∩ ( 𝑥 ∪ 𝑦 ) )
23 inteq ⊢ ( 𝑧 = ( 𝑥 ∪ 𝑦 ) → ∩ 𝑧 = ∩ ( 𝑥 ∪ 𝑦 ) )
24 23 rspceeqv ⊢ ( ( ( 𝑥 ∪ 𝑦 ) ∈ ( 𝒫 𝐶 ∩ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∩ ( 𝑥 ∪ 𝑦 ) ) → ∃ 𝑧 ∈ ( 𝒫 𝐶 ∩ Fin ) ( 𝐴 ∩ 𝐵 ) = ∩ 𝑧 )
25 19 22 24 syl2an ⊢ ( ( ( 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ∧ 𝑦 ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ ( 𝐴 = ∩ 𝑥 ∧ 𝐵 = ∩ 𝑦 ) ) → ∃ 𝑧 ∈ ( 𝒫 𝐶 ∩ Fin ) ( 𝐴 ∩ 𝐵 ) = ∩ 𝑧 )
26 25 an4s ⊢ ( ( ( 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ∧ 𝐴 = ∩ 𝑥 ) ∧ ( 𝑦 ∈ ( 𝒫 𝐶 ∩ Fin ) ∧ 𝐵 = ∩ 𝑦 ) ) → ∃ 𝑧 ∈ ( 𝒫 𝐶 ∩ Fin ) ( 𝐴 ∩ 𝐵 ) = ∩ 𝑧 )
27 26 rexlimdvaa ⊢ ( ( 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ∧ 𝐴 = ∩ 𝑥 ) → ( ∃ 𝑦 ∈ ( 𝒫 𝐶 ∩ Fin ) 𝐵 = ∩ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝐶 ∩ Fin ) ( 𝐴 ∩ 𝐵 ) = ∩ 𝑧 ) )
28 27 rexlimiva ⊢ ( ∃ 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) 𝐴 = ∩ 𝑥 → ( ∃ 𝑦 ∈ ( 𝒫 𝐶 ∩ Fin ) 𝐵 = ∩ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝐶 ∩ Fin ) ( 𝐴 ∩ 𝐵 ) = ∩ 𝑧 ) )
29 5 10 28 sylc ⊢ ( ( 𝐴 ∈ ( fi ‘ 𝐶 ) ∧ 𝐵 ∈ ( fi ‘ 𝐶 ) ) → ∃ 𝑧 ∈ ( 𝒫 𝐶 ∩ Fin ) ( 𝐴 ∩ 𝐵 ) = ∩ 𝑧 )
30 inex1g ⊢ ( 𝐴 ∈ ( fi ‘ 𝐶 ) → ( 𝐴 ∩ 𝐵 ) ∈ V )
31 elfi ⊢ ( ( ( 𝐴 ∩ 𝐵 ) ∈ V ∧ 𝐶 ∈ V ) → ( ( 𝐴 ∩ 𝐵 ) ∈ ( fi ‘ 𝐶 ) ↔ ∃ 𝑧 ∈ ( 𝒫 𝐶 ∩ Fin ) ( 𝐴 ∩ 𝐵 ) = ∩ 𝑧 ) )
32 30 1 31 syl2anc ⊢ ( 𝐴 ∈ ( fi ‘ 𝐶 ) → ( ( 𝐴 ∩ 𝐵 ) ∈ ( fi ‘ 𝐶 ) ↔ ∃ 𝑧 ∈ ( 𝒫 𝐶 ∩ Fin ) ( 𝐴 ∩ 𝐵 ) = ∩ 𝑧 ) )
33 32 adantr ⊢ ( ( 𝐴 ∈ ( fi ‘ 𝐶 ) ∧ 𝐵 ∈ ( fi ‘ 𝐶 ) ) → ( ( 𝐴 ∩ 𝐵 ) ∈ ( fi ‘ 𝐶 ) ↔ ∃ 𝑧 ∈ ( 𝒫 𝐶 ∩ Fin ) ( 𝐴 ∩ 𝐵 ) = ∩ 𝑧 ) )
34 29 33 mpbird ⊢ ( ( 𝐴 ∈ ( fi ‘ 𝐶 ) ∧ 𝐵 ∈ ( fi ‘ 𝐶 ) ) → ( 𝐴 ∩ 𝐵 ) ∈ ( fi ‘ 𝐶 ) )