Metamath Proof Explorer


Theorem psrbaglefiOLD

Description: Obsolete version of psrbaglefi as of 6-Aug-2024. (Contributed by Mario Carneiro, 29-Dec-2014) (Revised by Mario Carneiro, 25-Jan-2015) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis psrbag.d 𝐷 = { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin }
Assertion psrbaglefiOLD ( ( 𝐼𝑉𝐹𝐷 ) → { 𝑦𝐷𝑦r𝐹 } ∈ Fin )

Proof

Step Hyp Ref Expression
1 psrbag.d 𝐷 = { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ 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 ... ( 𝐹𝑥 ) ) ⊆ ℕ0X 𝑥𝐼 ( 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 psrbagfOLD ( ( 𝐼𝑉𝐹𝐷 ) → 𝐹 : 𝐼 ⟶ ℕ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 psrbagleclOLD ( ( 𝐼𝑉 ∧ ( 𝐹𝐷𝑦 : 𝐼 ⟶ ℕ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 ( 𝐹𝐷 ↔ ( 𝐹 ∈ ( ℕ0m 𝐼 ) ∧ ( 𝐹 “ ℕ ) ∈ Fin ) )
54 49 53 sylib ( ( 𝐼𝑉𝐹𝐷 ) → ( 𝐹 ∈ ( ℕ0m 𝐼 ) ∧ ( 𝐹 “ ℕ ) ∈ 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 eqtrdi ( ( ( 𝐼𝑉𝐹𝐷 ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝐹 “ ℕ ) ) ) → ( 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 )