This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ffvelcdm ⊢ ( ( 𝑦 : 𝐼 ⟶ ℕ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 ffvelcdmda ⊢ ( ( ( 𝐹 ∈ 𝐷 ∧ 𝑦 : 𝐼 ⟶ ℕ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 eqabcdv ⊢ ( 𝐹 ∈ 𝐷 → { 𝑦 ∣ ( 𝑦 ∈ 𝐷 ∧ 𝑦 ∘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 fcdmnn0suppg ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐹 : 𝐼 ⟶ ℕ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 )