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

Metamath Proof Explorer

Theorem inelfi

Description: The intersection of two sets is a finite intersection. (Contributed by Thierry Arnoux, 6-Jan-2017)

Ref Expression
Assertion inelfi ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 ∩ 𝐵 ) ∈ ( fi ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 prelpwi ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → { 𝐴 , 𝐵 } ∈ 𝒫 𝑋 )
2 1 3adant1 ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → { 𝐴 , 𝐵 } ∈ 𝒫 𝑋 )
3 prfi ⊢ { 𝐴 , 𝐵 } ∈ Fin
4 3 a1i ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → { 𝐴 , 𝐵 } ∈ Fin )
5 2 4 elind ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → { 𝐴 , 𝐵 } ∈ ( 𝒫 𝑋 ∩ Fin ) )
6 intprg ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ∩ { 𝐴 , 𝐵 } = ( 𝐴 ∩ 𝐵 ) )
7 6 3adant1 ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ∩ { 𝐴 , 𝐵 } = ( 𝐴 ∩ 𝐵 ) )
8 7 eqcomd ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 ∩ 𝐵 ) = ∩ { 𝐴 , 𝐵 } )
9 inteq ⊢ ( 𝑝 = { 𝐴 , 𝐵 } → ∩ 𝑝 = ∩ { 𝐴 , 𝐵 } )
10 9 rspceeqv ⊢ ( ( { 𝐴 , 𝐵 } ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∩ { 𝐴 , 𝐵 } ) → ∃ 𝑝 ∈ ( 𝒫 𝑋 ∩ Fin ) ( 𝐴 ∩ 𝐵 ) = ∩ 𝑝 )
11 5 8 10 syl2anc ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ∃ 𝑝 ∈ ( 𝒫 𝑋 ∩ Fin ) ( 𝐴 ∩ 𝐵 ) = ∩ 𝑝 )
12 inex1g ⊢ ( 𝐴 ∈ 𝑋 → ( 𝐴 ∩ 𝐵 ) ∈ V )
13 12 3ad2ant2 ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 ∩ 𝐵 ) ∈ V )
14 simp1 ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝑋 ∈ 𝑉 )
15 elfi ⊢ ( ( ( 𝐴 ∩ 𝐵 ) ∈ V ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝐴 ∩ 𝐵 ) ∈ ( fi ‘ 𝑋 ) ↔ ∃ 𝑝 ∈ ( 𝒫 𝑋 ∩ Fin ) ( 𝐴 ∩ 𝐵 ) = ∩ 𝑝 ) )
16 13 14 15 syl2anc ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 ∩ 𝐵 ) ∈ ( fi ‘ 𝑋 ) ↔ ∃ 𝑝 ∈ ( 𝒫 𝑋 ∩ Fin ) ( 𝐴 ∩ 𝐵 ) = ∩ 𝑝 ) )
17 11 16 mpbird ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 ∩ 𝐵 ) ∈ ( fi ‘ 𝑋 ) )