Theorem ufinffr

Description: An infinite subset is contained in a free ultrafilter. (Contributed by Jeff Hankins, 6-Dec-2009) (Revised by Mario Carneiro, 4-Dec-2013)

	Ref	Expression
Assertion	ufinffr	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴 ) → ∃ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐴 ∈ 𝑓 ∧ ∩ 𝑓 = ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		ominf	⊢ ¬ ω ∈ Fin
2		domfi	⊢ ( ( 𝐴 ∈ Fin ∧ ω ≼ 𝐴 ) → ω ∈ Fin )
3	2	expcom	⊢ ( ω ≼ 𝐴 → ( 𝐴 ∈ Fin → ω ∈ Fin ) )
4	1 3	mtoi	⊢ ( ω ≼ 𝐴 → ¬ 𝐴 ∈ Fin )
5		cfinfil	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ¬ 𝐴 ∈ Fin ) → { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∖ 𝑥 ) ∈ Fin } ∈ ( Fil ‘ 𝑋 ) )
6	4 5	syl3an3	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴 ) → { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∖ 𝑥 ) ∈ Fin } ∈ ( Fil ‘ 𝑋 ) )
7		filssufil	⊢ ( { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∖ 𝑥 ) ∈ Fin } ∈ ( Fil ‘ 𝑋 ) → ∃ 𝑓 ∈ ( UFil ‘ 𝑋 ) { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∖ 𝑥 ) ∈ Fin } ⊆ 𝑓 )
8	6 7	syl	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴 ) → ∃ 𝑓 ∈ ( UFil ‘ 𝑋 ) { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∖ 𝑥 ) ∈ Fin } ⊆ 𝑓 )
9		difeq2	⊢ ( 𝑥 = 𝐴 → ( 𝐴 ∖ 𝑥 ) = ( 𝐴 ∖ 𝐴 ) )
10		difid	⊢ ( 𝐴 ∖ 𝐴 ) = ∅
11	9 10	eqtrdi	⊢ ( 𝑥 = 𝐴 → ( 𝐴 ∖ 𝑥 ) = ∅ )
12	11	eleq1d	⊢ ( 𝑥 = 𝐴 → ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ↔ ∅ ∈ Fin ) )
13		elpw2g	⊢ ( 𝑋 ∈ 𝐵 → ( 𝐴 ∈ 𝒫 𝑋 ↔ 𝐴 ⊆ 𝑋 ) )
14	13	biimpar	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ) → 𝐴 ∈ 𝒫 𝑋 )
15	14	3adant3	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴 ) → 𝐴 ∈ 𝒫 𝑋 )
16		0fin	⊢ ∅ ∈ Fin
17	16	a1i	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴 ) → ∅ ∈ Fin )
18	12 15 17	elrabd	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴 ) → 𝐴 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∖ 𝑥 ) ∈ Fin } )
19		ssel	⊢ ( { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∖ 𝑥 ) ∈ Fin } ⊆ 𝑓 → ( 𝐴 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∖ 𝑥 ) ∈ Fin } → 𝐴 ∈ 𝑓 ) )
20	18 19	syl5com	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴 ) → ( { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∖ 𝑥 ) ∈ Fin } ⊆ 𝑓 → 𝐴 ∈ 𝑓 ) )
21		intss	⊢ ( { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∖ 𝑥 ) ∈ Fin } ⊆ 𝑓 → ∩ 𝑓 ⊆ ∩ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∖ 𝑥 ) ∈ Fin } )
22		neldifsn	⊢ ¬ 𝑦 ∈ ( 𝐴 ∖ { 𝑦 } )
23		elinti	⊢ ( 𝑦 ∈ ∩ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∖ 𝑥 ) ∈ Fin } → ( ( 𝐴 ∖ { 𝑦 } ) ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∖ 𝑥 ) ∈ Fin } → 𝑦 ∈ ( 𝐴 ∖ { 𝑦 } ) ) )
24	22 23	mtoi	⊢ ( 𝑦 ∈ ∩ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∖ 𝑥 ) ∈ Fin } → ¬ ( 𝐴 ∖ { 𝑦 } ) ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∖ 𝑥 ) ∈ Fin } )
25		difeq2	⊢ ( 𝑥 = ( 𝐴 ∖ { 𝑦 } ) → ( 𝐴 ∖ 𝑥 ) = ( 𝐴 ∖ ( 𝐴 ∖ { 𝑦 } ) ) )
26	25	eleq1d	⊢ ( 𝑥 = ( 𝐴 ∖ { 𝑦 } ) → ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ↔ ( 𝐴 ∖ ( 𝐴 ∖ { 𝑦 } ) ) ∈ Fin ) )
27		simp2	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴 ) → 𝐴 ⊆ 𝑋 )
28	27	ssdifssd	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴 ) → ( 𝐴 ∖ { 𝑦 } ) ⊆ 𝑋 )
29		elpw2g	⊢ ( 𝑋 ∈ 𝐵 → ( ( 𝐴 ∖ { 𝑦 } ) ∈ 𝒫 𝑋 ↔ ( 𝐴 ∖ { 𝑦 } ) ⊆ 𝑋 ) )
30	29	3ad2ant1	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴 ) → ( ( 𝐴 ∖ { 𝑦 } ) ∈ 𝒫 𝑋 ↔ ( 𝐴 ∖ { 𝑦 } ) ⊆ 𝑋 ) )
31	28 30	mpbird	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴 ) → ( 𝐴 ∖ { 𝑦 } ) ∈ 𝒫 𝑋 )
32		snfi	⊢ { 𝑦 } ∈ Fin
33		eldif	⊢ ( 𝑥 ∈ ( 𝐴 ∖ ( 𝐴 ∖ { 𝑦 } ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ( 𝐴 ∖ { 𝑦 } ) ) )
34		eldif	⊢ ( 𝑥 ∈ ( 𝐴 ∖ { 𝑦 } ) ↔ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ { 𝑦 } ) )
35	34	notbii	⊢ ( ¬ 𝑥 ∈ ( 𝐴 ∖ { 𝑦 } ) ↔ ¬ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ { 𝑦 } ) )
36		iman	⊢ ( ( 𝑥 ∈ 𝐴 → 𝑥 ∈ { 𝑦 } ) ↔ ¬ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ { 𝑦 } ) )
37	35 36	bitr4i	⊢ ( ¬ 𝑥 ∈ ( 𝐴 ∖ { 𝑦 } ) ↔ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ { 𝑦 } ) )
38	37	anbi2i	⊢ ( ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ( 𝐴 ∖ { 𝑦 } ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ { 𝑦 } ) ) )
39	33 38	bitri	⊢ ( 𝑥 ∈ ( 𝐴 ∖ ( 𝐴 ∖ { 𝑦 } ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ { 𝑦 } ) ) )
40		pm3.35	⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ { 𝑦 } ) ) → 𝑥 ∈ { 𝑦 } )
41	39 40	sylbi	⊢ ( 𝑥 ∈ ( 𝐴 ∖ ( 𝐴 ∖ { 𝑦 } ) ) → 𝑥 ∈ { 𝑦 } )
42	41	ssriv	⊢ ( 𝐴 ∖ ( 𝐴 ∖ { 𝑦 } ) ) ⊆ { 𝑦 }
43		ssfi	⊢ ( ( { 𝑦 } ∈ Fin ∧ ( 𝐴 ∖ ( 𝐴 ∖ { 𝑦 } ) ) ⊆ { 𝑦 } ) → ( 𝐴 ∖ ( 𝐴 ∖ { 𝑦 } ) ) ∈ Fin )
44	32 42 43	mp2an	⊢ ( 𝐴 ∖ ( 𝐴 ∖ { 𝑦 } ) ) ∈ Fin
45	44	a1i	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴 ) → ( 𝐴 ∖ ( 𝐴 ∖ { 𝑦 } ) ) ∈ Fin )
46	26 31 45	elrabd	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴 ) → ( 𝐴 ∖ { 𝑦 } ) ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∖ 𝑥 ) ∈ Fin } )
47	24 46	nsyl3	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴 ) → ¬ 𝑦 ∈ ∩ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∖ 𝑥 ) ∈ Fin } )
48	47	eq0rdv	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴 ) → ∩ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∖ 𝑥 ) ∈ Fin } = ∅ )
49	48	sseq2d	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴 ) → ( ∩ 𝑓 ⊆ ∩ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∖ 𝑥 ) ∈ Fin } ↔ ∩ 𝑓 ⊆ ∅ ) )
50	21 49	syl5ib	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴 ) → ( { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∖ 𝑥 ) ∈ Fin } ⊆ 𝑓 → ∩ 𝑓 ⊆ ∅ ) )
51		ss0	⊢ ( ∩ 𝑓 ⊆ ∅ → ∩ 𝑓 = ∅ )
52	50 51	syl6	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴 ) → ( { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∖ 𝑥 ) ∈ Fin } ⊆ 𝑓 → ∩ 𝑓 = ∅ ) )
53	20 52	jcad	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴 ) → ( { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∖ 𝑥 ) ∈ Fin } ⊆ 𝑓 → ( 𝐴 ∈ 𝑓 ∧ ∩ 𝑓 = ∅ ) ) )
54	53	reximdv	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴 ) → ( ∃ 𝑓 ∈ ( UFil ‘ 𝑋 ) { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∖ 𝑥 ) ∈ Fin } ⊆ 𝑓 → ∃ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐴 ∈ 𝑓 ∧ ∩ 𝑓 = ∅ ) ) )
55	8 54	mpd	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴 ) → ∃ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐴 ∈ 𝑓 ∧ ∩ 𝑓 = ∅ ) )