Theorem elfi2

Description: The empty intersection need not be considered in the set of finite intersections. (Contributed by Mario Carneiro, 21-Mar-2015)

	Ref	Expression
Assertion	elfi2	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 ∈ ( fi ‘ 𝐵 ) ↔ ∃ 𝑥 ∈ ( ( 𝒫 𝐵 ∩ Fin ) ∖ { ∅ } ) 𝐴 = ∩ 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		elex	⊢ ( 𝐴 ∈ ( fi ‘ 𝐵 ) → 𝐴 ∈ V )
2	1	a1i	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 ∈ ( fi ‘ 𝐵 ) → 𝐴 ∈ V ) )
3		simpr	⊢ ( ( 𝑥 ∈ ( ( 𝒫 𝐵 ∩ Fin ) ∖ { ∅ } ) ∧ 𝐴 = ∩ 𝑥 ) → 𝐴 = ∩ 𝑥 )
4		eldifsni	⊢ ( 𝑥 ∈ ( ( 𝒫 𝐵 ∩ Fin ) ∖ { ∅ } ) → 𝑥 ≠ ∅ )
5	4	adantr	⊢ ( ( 𝑥 ∈ ( ( 𝒫 𝐵 ∩ Fin ) ∖ { ∅ } ) ∧ 𝐴 = ∩ 𝑥 ) → 𝑥 ≠ ∅ )
6		intex	⊢ ( 𝑥 ≠ ∅ ↔ ∩ 𝑥 ∈ V )
7	5 6	sylib	⊢ ( ( 𝑥 ∈ ( ( 𝒫 𝐵 ∩ Fin ) ∖ { ∅ } ) ∧ 𝐴 = ∩ 𝑥 ) → ∩ 𝑥 ∈ V )
8	3 7	eqeltrd	⊢ ( ( 𝑥 ∈ ( ( 𝒫 𝐵 ∩ Fin ) ∖ { ∅ } ) ∧ 𝐴 = ∩ 𝑥 ) → 𝐴 ∈ V )
9	8	rexlimiva	⊢ ( ∃ 𝑥 ∈ ( ( 𝒫 𝐵 ∩ Fin ) ∖ { ∅ } ) 𝐴 = ∩ 𝑥 → 𝐴 ∈ V )
10	9	a1i	⊢ ( 𝐵 ∈ 𝑉 → ( ∃ 𝑥 ∈ ( ( 𝒫 𝐵 ∩ Fin ) ∖ { ∅ } ) 𝐴 = ∩ 𝑥 → 𝐴 ∈ V ) )
11		elfi	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 ∈ ( fi ‘ 𝐵 ) ↔ ∃ 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) 𝐴 = ∩ 𝑥 ) )
12		vprc	⊢ ¬ V ∈ V
13		elsni	⊢ ( 𝑥 ∈ { ∅ } → 𝑥 = ∅ )
14	13	inteqd	⊢ ( 𝑥 ∈ { ∅ } → ∩ 𝑥 = ∩ ∅ )
15		int0	⊢ ∩ ∅ = V
16	14 15	eqtrdi	⊢ ( 𝑥 ∈ { ∅ } → ∩ 𝑥 = V )
17	16	eleq1d	⊢ ( 𝑥 ∈ { ∅ } → ( ∩ 𝑥 ∈ V ↔ V ∈ V ) )
18	12 17	mtbiri	⊢ ( 𝑥 ∈ { ∅ } → ¬ ∩ 𝑥 ∈ V )
19		simpr	⊢ ( ( ( 𝐴 ∈ V ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 = ∩ 𝑥 ) → 𝐴 = ∩ 𝑥 )
20		simpll	⊢ ( ( ( 𝐴 ∈ V ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 = ∩ 𝑥 ) → 𝐴 ∈ V )
21	19 20	eqeltrrd	⊢ ( ( ( 𝐴 ∈ V ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 = ∩ 𝑥 ) → ∩ 𝑥 ∈ V )
22	18 21	nsyl3	⊢ ( ( ( 𝐴 ∈ V ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 = ∩ 𝑥 ) → ¬ 𝑥 ∈ { ∅ } )
23	22	biantrud	⊢ ( ( ( 𝐴 ∈ V ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 = ∩ 𝑥 ) → ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↔ ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ∧ ¬ 𝑥 ∈ { ∅ } ) ) )
24		eldif	⊢ ( 𝑥 ∈ ( ( 𝒫 𝐵 ∩ Fin ) ∖ { ∅ } ) ↔ ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ∧ ¬ 𝑥 ∈ { ∅ } ) )
25	23 24	bitr4di	⊢ ( ( ( 𝐴 ∈ V ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 = ∩ 𝑥 ) → ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↔ 𝑥 ∈ ( ( 𝒫 𝐵 ∩ Fin ) ∖ { ∅ } ) ) )
26	25	pm5.32da	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ 𝑉 ) → ( ( 𝐴 = ∩ 𝑥 ∧ 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ) ↔ ( 𝐴 = ∩ 𝑥 ∧ 𝑥 ∈ ( ( 𝒫 𝐵 ∩ Fin ) ∖ { ∅ } ) ) ) )
27		ancom	⊢ ( ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ∧ 𝐴 = ∩ 𝑥 ) ↔ ( 𝐴 = ∩ 𝑥 ∧ 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ) )
28		ancom	⊢ ( ( 𝑥 ∈ ( ( 𝒫 𝐵 ∩ Fin ) ∖ { ∅ } ) ∧ 𝐴 = ∩ 𝑥 ) ↔ ( 𝐴 = ∩ 𝑥 ∧ 𝑥 ∈ ( ( 𝒫 𝐵 ∩ Fin ) ∖ { ∅ } ) ) )
29	26 27 28	3bitr4g	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ 𝑉 ) → ( ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ∧ 𝐴 = ∩ 𝑥 ) ↔ ( 𝑥 ∈ ( ( 𝒫 𝐵 ∩ Fin ) ∖ { ∅ } ) ∧ 𝐴 = ∩ 𝑥 ) ) )
30	29	rexbidv2	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ 𝑉 ) → ( ∃ 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) 𝐴 = ∩ 𝑥 ↔ ∃ 𝑥 ∈ ( ( 𝒫 𝐵 ∩ Fin ) ∖ { ∅ } ) 𝐴 = ∩ 𝑥 ) )
31	11 30	bitrd	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 ∈ ( fi ‘ 𝐵 ) ↔ ∃ 𝑥 ∈ ( ( 𝒫 𝐵 ∩ Fin ) ∖ { ∅ } ) 𝐴 = ∩ 𝑥 ) )
32	31	expcom	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 ∈ V → ( 𝐴 ∈ ( fi ‘ 𝐵 ) ↔ ∃ 𝑥 ∈ ( ( 𝒫 𝐵 ∩ Fin ) ∖ { ∅ } ) 𝐴 = ∩ 𝑥 ) ) )
33	2 10 32	pm5.21ndd	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 ∈ ( fi ‘ 𝐵 ) ↔ ∃ 𝑥 ∈ ( ( 𝒫 𝐵 ∩ Fin ) ∖ { ∅ } ) 𝐴 = ∩ 𝑥 ) )