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 ‘ 𝑋 ) )