Theorem elfir

Description: Sufficient condition for an element of ( fiB ) . (Contributed by Mario Carneiro, 24-Nov-2013)

	Ref	Expression
Assertion	elfir	⊢ ( ( 𝐵 ∈ 𝑉 ∧ ( 𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) ) → ∩ 𝐴 ∈ ( fi ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		simp1	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) → 𝐴 ⊆ 𝐵 )
2		elpw2g	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵 ) )
3	1 2	imbitrrid	⊢ ( 𝐵 ∈ 𝑉 → ( ( 𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) → 𝐴 ∈ 𝒫 𝐵 ) )
4	3	imp	⊢ ( ( 𝐵 ∈ 𝑉 ∧ ( 𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) ) → 𝐴 ∈ 𝒫 𝐵 )
5		simpr3	⊢ ( ( 𝐵 ∈ 𝑉 ∧ ( 𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) ) → 𝐴 ∈ Fin )
6	4 5	elind	⊢ ( ( 𝐵 ∈ 𝑉 ∧ ( 𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) ) → 𝐴 ∈ ( 𝒫 𝐵 ∩ Fin ) )
7		eqid	⊢ ∩ 𝐴 = ∩ 𝐴
8		inteq	⊢ ( 𝑥 = 𝐴 → ∩ 𝑥 = ∩ 𝐴 )
9	8	rspceeqv	⊢ ( ( 𝐴 ∈ ( 𝒫 𝐵 ∩ Fin ) ∧ ∩ 𝐴 = ∩ 𝐴 ) → ∃ 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ∩ 𝐴 = ∩ 𝑥 )
10	6 7 9	sylancl	⊢ ( ( 𝐵 ∈ 𝑉 ∧ ( 𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) ) → ∃ 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ∩ 𝐴 = ∩ 𝑥 )
11		simp2	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) → 𝐴 ≠ ∅ )
12		intex	⊢ ( 𝐴 ≠ ∅ ↔ ∩ 𝐴 ∈ V )
13	11 12	sylib	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) → ∩ 𝐴 ∈ V )
14		id	⊢ ( 𝐵 ∈ 𝑉 → 𝐵 ∈ 𝑉 )
15		elfi	⊢ ( ( ∩ 𝐴 ∈ V ∧ 𝐵 ∈ 𝑉 ) → ( ∩ 𝐴 ∈ ( fi ‘ 𝐵 ) ↔ ∃ 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ∩ 𝐴 = ∩ 𝑥 ) )
16	13 14 15	syl2anr	⊢ ( ( 𝐵 ∈ 𝑉 ∧ ( 𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) ) → ( ∩ 𝐴 ∈ ( fi ‘ 𝐵 ) ↔ ∃ 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ∩ 𝐴 = ∩ 𝑥 ) )
17	10 16	mpbird	⊢ ( ( 𝐵 ∈ 𝑉 ∧ ( 𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) ) → ∩ 𝐴 ∈ ( fi ‘ 𝐵 ) )