Theorem psrbaglefi

Description: There are finitely many bags dominated by a given bag. (Contributed by Mario Carneiro, 29-Dec-2014) (Revised by Mario Carneiro, 25-Jan-2015) Remove a sethood antecedent. (Revised by SN, 5-Aug-2024)

	Ref	Expression
Hypothesis	psrbag.d	⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
Assertion	psrbaglefi	⊢ ( 𝐹 ∈ 𝐷 → { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝐹 } ∈ Fin )

Proof

Step	Hyp	Ref	Expression
1		psrbag.d	⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
2		df-rab	⊢ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝐹 } = { 𝑦 ∣ ( 𝑦 ∈ 𝐷 ∧ 𝑦 ∘r ≤ 𝐹 ) }
3	1	psrbagf	⊢ ( 𝑦 ∈ 𝐷 → 𝑦 : 𝐼 ⟶ ℕ0 )
4	3	a1i	⊢ ( 𝐹 ∈ 𝐷 → ( 𝑦 ∈ 𝐷 → 𝑦 : 𝐼 ⟶ ℕ0 ) )
5	4	adantrd	⊢ ( 𝐹 ∈ 𝐷 → ( ( 𝑦 ∈ 𝐷 ∧ 𝑦 ∘r ≤ 𝐹 ) → 𝑦 : 𝐼 ⟶ ℕ0 ) )
6		ss2ixp	⊢ ( ∀ 𝑥 ∈ 𝐼 ( 0 ... ( 𝐹 ‘ 𝑥 ) ) ⊆ ℕ0 → X 𝑥 ∈ 𝐼 ( 0 ... ( 𝐹 ‘ 𝑥 ) ) ⊆ X 𝑥 ∈ 𝐼 ℕ0 )
7		fz0ssnn0	⊢ ( 0 ... ( 𝐹 ‘ 𝑥 ) ) ⊆ ℕ0
8	7	a1i	⊢ ( 𝑥 ∈ 𝐼 → ( 0 ... ( 𝐹 ‘ 𝑥 ) ) ⊆ ℕ0 )
9	6 8	mprg	⊢ X 𝑥 ∈ 𝐼 ( 0 ... ( 𝐹 ‘ 𝑥 ) ) ⊆ X 𝑥 ∈ 𝐼 ℕ0
10	9	sseli	⊢ ( 𝑦 ∈ X 𝑥 ∈ 𝐼 ( 0 ... ( 𝐹 ‘ 𝑥 ) ) → 𝑦 ∈ X 𝑥 ∈ 𝐼 ℕ0 )
11		vex	⊢ 𝑦 ∈ V
12	11	elixpconst	⊢ ( 𝑦 ∈ X 𝑥 ∈ 𝐼 ℕ0 ↔ 𝑦 : 𝐼 ⟶ ℕ0 )
13	10 12	sylib	⊢ ( 𝑦 ∈ X 𝑥 ∈ 𝐼 ( 0 ... ( 𝐹 ‘ 𝑥 ) ) → 𝑦 : 𝐼 ⟶ ℕ0 )
14	13	a1i	⊢ ( 𝐹 ∈ 𝐷 → ( 𝑦 ∈ X 𝑥 ∈ 𝐼 ( 0 ... ( 𝐹 ‘ 𝑥 ) ) → 𝑦 : 𝐼 ⟶ ℕ0 ) )
15		ffn	⊢ ( 𝑦 : 𝐼 ⟶ ℕ0 → 𝑦 Fn 𝐼 )
16	15	adantl	⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝑦 : 𝐼 ⟶ ℕ0 ) → 𝑦 Fn 𝐼 )
17	11	elixp	⊢ ( 𝑦 ∈ X 𝑥 ∈ 𝐼 ( 0 ... ( 𝐹 ‘ 𝑥 ) ) ↔ ( 𝑦 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑦 ‘ 𝑥 ) ∈ ( 0 ... ( 𝐹 ‘ 𝑥 ) ) ) )
18	17	baib	⊢ ( 𝑦 Fn 𝐼 → ( 𝑦 ∈ X 𝑥 ∈ 𝐼 ( 0 ... ( 𝐹 ‘ 𝑥 ) ) ↔ ∀ 𝑥 ∈ 𝐼 ( 𝑦 ‘ 𝑥 ) ∈ ( 0 ... ( 𝐹 ‘ 𝑥 ) ) ) )
19	16 18	syl	⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝑦 : 𝐼 ⟶ ℕ0 ) → ( 𝑦 ∈ X 𝑥 ∈ 𝐼 ( 0 ... ( 𝐹 ‘ 𝑥 ) ) ↔ ∀ 𝑥 ∈ 𝐼 ( 𝑦 ‘ 𝑥 ) ∈ ( 0 ... ( 𝐹 ‘ 𝑥 ) ) ) )
20		ffvelrn	⊢ ( ( 𝑦 : 𝐼 ⟶ ℕ0 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑦 ‘ 𝑥 ) ∈ ℕ0 )
21	20	adantll	⊢ ( ( ( 𝐹 ∈ 𝐷 ∧ 𝑦 : 𝐼 ⟶ ℕ0 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑦 ‘ 𝑥 ) ∈ ℕ0 )
22		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
23	21 22	eleqtrdi	⊢ ( ( ( 𝐹 ∈ 𝐷 ∧ 𝑦 : 𝐼 ⟶ ℕ0 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑦 ‘ 𝑥 ) ∈ ( ℤ≥ ‘ 0 ) )
24	1	psrbagf	⊢ ( 𝐹 ∈ 𝐷 → 𝐹 : 𝐼 ⟶ ℕ0 )
25	24	adantr	⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝑦 : 𝐼 ⟶ ℕ0 ) → 𝐹 : 𝐼 ⟶ ℕ0 )
26	25	ffvelrnda	⊢ ( ( ( 𝐹 ∈ 𝐷 ∧ 𝑦 : 𝐼 ⟶ ℕ0 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℕ0 )
27	26	nn0zd	⊢ ( ( ( 𝐹 ∈ 𝐷 ∧ 𝑦 : 𝐼 ⟶ ℕ0 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℤ )
28		elfz5	⊢ ( ( ( 𝑦 ‘ 𝑥 ) ∈ ( ℤ≥ ‘ 0 ) ∧ ( 𝐹 ‘ 𝑥 ) ∈ ℤ ) → ( ( 𝑦 ‘ 𝑥 ) ∈ ( 0 ... ( 𝐹 ‘ 𝑥 ) ) ↔ ( 𝑦 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
29	23 27 28	syl2anc	⊢ ( ( ( 𝐹 ∈ 𝐷 ∧ 𝑦 : 𝐼 ⟶ ℕ0 ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑦 ‘ 𝑥 ) ∈ ( 0 ... ( 𝐹 ‘ 𝑥 ) ) ↔ ( 𝑦 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
30	29	ralbidva	⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝑦 : 𝐼 ⟶ ℕ0 ) → ( ∀ 𝑥 ∈ 𝐼 ( 𝑦 ‘ 𝑥 ) ∈ ( 0 ... ( 𝐹 ‘ 𝑥 ) ) ↔ ∀ 𝑥 ∈ 𝐼 ( 𝑦 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
31	24	ffnd	⊢ ( 𝐹 ∈ 𝐷 → 𝐹 Fn 𝐼 )
32	31	adantr	⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝑦 : 𝐼 ⟶ ℕ0 ) → 𝐹 Fn 𝐼 )
33	11	a1i	⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝑦 : 𝐼 ⟶ ℕ0 ) → 𝑦 ∈ V )
34		simpl	⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝑦 : 𝐼 ⟶ ℕ0 ) → 𝐹 ∈ 𝐷 )
35		inidm	⊢ ( 𝐼 ∩ 𝐼 ) = 𝐼
36		eqidd	⊢ ( ( ( 𝐹 ∈ 𝐷 ∧ 𝑦 : 𝐼 ⟶ ℕ0 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑦 ‘ 𝑥 ) = ( 𝑦 ‘ 𝑥 ) )
37		eqidd	⊢ ( ( ( 𝐹 ∈ 𝐷 ∧ 𝑦 : 𝐼 ⟶ ℕ0 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
38	16 32 33 34 35 36 37	ofrfvalg	⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝑦 : 𝐼 ⟶ ℕ0 ) → ( 𝑦 ∘r ≤ 𝐹 ↔ ∀ 𝑥 ∈ 𝐼 ( 𝑦 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
39	30 38	bitr4d	⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝑦 : 𝐼 ⟶ ℕ0 ) → ( ∀ 𝑥 ∈ 𝐼 ( 𝑦 ‘ 𝑥 ) ∈ ( 0 ... ( 𝐹 ‘ 𝑥 ) ) ↔ 𝑦 ∘r ≤ 𝐹 ) )
40	1	psrbaglecl	⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝑦 : 𝐼 ⟶ ℕ0 ∧ 𝑦 ∘r ≤ 𝐹 ) → 𝑦 ∈ 𝐷 )
41	40	3expia	⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝑦 : 𝐼 ⟶ ℕ0 ) → ( 𝑦 ∘r ≤ 𝐹 → 𝑦 ∈ 𝐷 ) )
42	41	pm4.71rd	⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝑦 : 𝐼 ⟶ ℕ0 ) → ( 𝑦 ∘r ≤ 𝐹 ↔ ( 𝑦 ∈ 𝐷 ∧ 𝑦 ∘r ≤ 𝐹 ) ) )
43	19 39 42	3bitrrd	⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝑦 : 𝐼 ⟶ ℕ0 ) → ( ( 𝑦 ∈ 𝐷 ∧ 𝑦 ∘r ≤ 𝐹 ) ↔ 𝑦 ∈ X 𝑥 ∈ 𝐼 ( 0 ... ( 𝐹 ‘ 𝑥 ) ) ) )
44	43	ex	⊢ ( 𝐹 ∈ 𝐷 → ( 𝑦 : 𝐼 ⟶ ℕ0 → ( ( 𝑦 ∈ 𝐷 ∧ 𝑦 ∘r ≤ 𝐹 ) ↔ 𝑦 ∈ X 𝑥 ∈ 𝐼 ( 0 ... ( 𝐹 ‘ 𝑥 ) ) ) ) )
45	5 14 44	pm5.21ndd	⊢ ( 𝐹 ∈ 𝐷 → ( ( 𝑦 ∈ 𝐷 ∧ 𝑦 ∘r ≤ 𝐹 ) ↔ 𝑦 ∈ X 𝑥 ∈ 𝐼 ( 0 ... ( 𝐹 ‘ 𝑥 ) ) ) )
46	45	abbi1dv	⊢ ( 𝐹 ∈ 𝐷 → { 𝑦 ∣ ( 𝑦 ∈ 𝐷 ∧ 𝑦 ∘r ≤ 𝐹 ) } = X 𝑥 ∈ 𝐼 ( 0 ... ( 𝐹 ‘ 𝑥 ) ) )
47	2 46	eqtrid	⊢ ( 𝐹 ∈ 𝐷 → { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝐹 } = X 𝑥 ∈ 𝐼 ( 0 ... ( 𝐹 ‘ 𝑥 ) ) )
48		cnveq	⊢ ( 𝑓 = 𝐹 → ◡ 𝑓 = ◡ 𝐹 )
49	48	imaeq1d	⊢ ( 𝑓 = 𝐹 → ( ◡ 𝑓 “ ℕ ) = ( ◡ 𝐹 “ ℕ ) )
50	49	eleq1d	⊢ ( 𝑓 = 𝐹 → ( ( ◡ 𝑓 “ ℕ ) ∈ Fin ↔ ( ◡ 𝐹 “ ℕ ) ∈ Fin ) )
51	50 1	elrab2	⊢ ( 𝐹 ∈ 𝐷 ↔ ( 𝐹 ∈ ( ℕ0 ↑m 𝐼 ) ∧ ( ◡ 𝐹 “ ℕ ) ∈ Fin ) )
52	51	simprbi	⊢ ( 𝐹 ∈ 𝐷 → ( ◡ 𝐹 “ ℕ ) ∈ Fin )
53		fzfid	⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝑥 ∈ 𝐼 ) → ( 0 ... ( 𝐹 ‘ 𝑥 ) ) ∈ Fin )
54		frnnn0suppg	⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐹 : 𝐼 ⟶ ℕ0 ) → ( 𝐹 supp 0 ) = ( ◡ 𝐹 “ ℕ ) )
55	24 54	mpdan	⊢ ( 𝐹 ∈ 𝐷 → ( 𝐹 supp 0 ) = ( ◡ 𝐹 “ ℕ ) )
56		eqimss	⊢ ( ( 𝐹 supp 0 ) = ( ◡ 𝐹 “ ℕ ) → ( 𝐹 supp 0 ) ⊆ ( ◡ 𝐹 “ ℕ ) )
57	55 56	syl	⊢ ( 𝐹 ∈ 𝐷 → ( 𝐹 supp 0 ) ⊆ ( ◡ 𝐹 “ ℕ ) )
58		id	⊢ ( 𝐹 ∈ 𝐷 → 𝐹 ∈ 𝐷 )
59		c0ex	⊢ 0 ∈ V
60	59	a1i	⊢ ( 𝐹 ∈ 𝐷 → 0 ∈ V )
61	24 57 58 60	suppssrg	⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝑥 ∈ ( 𝐼 ∖ ( ◡ 𝐹 “ ℕ ) ) ) → ( 𝐹 ‘ 𝑥 ) = 0 )
62	61	oveq2d	⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝑥 ∈ ( 𝐼 ∖ ( ◡ 𝐹 “ ℕ ) ) ) → ( 0 ... ( 𝐹 ‘ 𝑥 ) ) = ( 0 ... 0 ) )
63		fz0sn	⊢ ( 0 ... 0 ) = { 0 }
64	62 63	eqtrdi	⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝑥 ∈ ( 𝐼 ∖ ( ◡ 𝐹 “ ℕ ) ) ) → ( 0 ... ( 𝐹 ‘ 𝑥 ) ) = { 0 } )
65		eqimss	⊢ ( ( 0 ... ( 𝐹 ‘ 𝑥 ) ) = { 0 } → ( 0 ... ( 𝐹 ‘ 𝑥 ) ) ⊆ { 0 } )
66	64 65	syl	⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝑥 ∈ ( 𝐼 ∖ ( ◡ 𝐹 “ ℕ ) ) ) → ( 0 ... ( 𝐹 ‘ 𝑥 ) ) ⊆ { 0 } )
67	52 53 66	ixpfi2	⊢ ( 𝐹 ∈ 𝐷 → X 𝑥 ∈ 𝐼 ( 0 ... ( 𝐹 ‘ 𝑥 ) ) ∈ Fin )
68	47 67	eqeltrd	⊢ ( 𝐹 ∈ 𝐷 → { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝐹 } ∈ Fin )