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)

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