Theorem fifo

Description: Describe a surjection from nonempty finite sets to finite intersections. (Contributed by Mario Carneiro, 18-May-2015)

	Ref	Expression
Hypothesis	fifo.1	⊢ 𝐹 = ( 𝑦 ∈ ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) ↦ ∩ 𝑦 )
Assertion	fifo	⊢ ( 𝐴 ∈ 𝑉 → 𝐹 : ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) –onto→ ( fi ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		fifo.1	⊢ 𝐹 = ( 𝑦 ∈ ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) ↦ ∩ 𝑦 )
2		eldifsni	⊢ ( 𝑦 ∈ ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) → 𝑦 ≠ ∅ )
3		intex	⊢ ( 𝑦 ≠ ∅ ↔ ∩ 𝑦 ∈ V )
4	2 3	sylib	⊢ ( 𝑦 ∈ ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) → ∩ 𝑦 ∈ V )
5	4	rgen	⊢ ∀ 𝑦 ∈ ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) ∩ 𝑦 ∈ V
6	1	fnmpt	⊢ ( ∀ 𝑦 ∈ ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) ∩ 𝑦 ∈ V → 𝐹 Fn ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) )
7	5 6	mp1i	⊢ ( 𝐴 ∈ 𝑉 → 𝐹 Fn ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) )
8		dffn4	⊢ ( 𝐹 Fn ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) ↔ 𝐹 : ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) –onto→ ran 𝐹 )
9	7 8	sylib	⊢ ( 𝐴 ∈ 𝑉 → 𝐹 : ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) –onto→ ran 𝐹 )
10		elfi2	⊢ ( 𝐴 ∈ 𝑉 → ( 𝑥 ∈ ( fi ‘ 𝐴 ) ↔ ∃ 𝑦 ∈ ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) 𝑥 = ∩ 𝑦 ) )
11	1	elrnmpt	⊢ ( 𝑥 ∈ V → ( 𝑥 ∈ ran 𝐹 ↔ ∃ 𝑦 ∈ ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) 𝑥 = ∩ 𝑦 ) )
12	11	elv	⊢ ( 𝑥 ∈ ran 𝐹 ↔ ∃ 𝑦 ∈ ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) 𝑥 = ∩ 𝑦 )
13	10 12	bitr4di	⊢ ( 𝐴 ∈ 𝑉 → ( 𝑥 ∈ ( fi ‘ 𝐴 ) ↔ 𝑥 ∈ ran 𝐹 ) )
14	13	eqrdv	⊢ ( 𝐴 ∈ 𝑉 → ( fi ‘ 𝐴 ) = ran 𝐹 )
15		foeq3	⊢ ( ( fi ‘ 𝐴 ) = ran 𝐹 → ( 𝐹 : ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) –onto→ ( fi ‘ 𝐴 ) ↔ 𝐹 : ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) –onto→ ran 𝐹 ) )
16	14 15	syl	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐹 : ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) –onto→ ( fi ‘ 𝐴 ) ↔ 𝐹 : ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) –onto→ ran 𝐹 ) )
17	9 16	mpbird	⊢ ( 𝐴 ∈ 𝑉 → 𝐹 : ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) –onto→ ( fi ‘ 𝐴 ) )