Metamath Proof Explorer


Theorem psrbaglesuppOLD

Description: Obsolete version of psrbaglesupp as of 5-Aug-2024. (Contributed by Mario Carneiro, 29-Dec-2014) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypothesis psrbag.d 𝐷 = { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin }
Assertion psrbaglesuppOLD ( ( 𝐼𝑉 ∧ ( 𝐹𝐷𝐺 : 𝐼 ⟶ ℕ0𝐺r𝐹 ) ) → ( 𝐺 “ ℕ ) ⊆ ( 𝐹 “ ℕ ) )

Proof

Step Hyp Ref Expression
1 psrbag.d 𝐷 = { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin }
2 frnnn0supp ( ( 𝐼𝑉𝐺 : 𝐼 ⟶ ℕ0 ) → ( 𝐺 supp 0 ) = ( 𝐺 “ ℕ ) )
3 2 3ad2antr2 ( ( 𝐼𝑉 ∧ ( 𝐹𝐷𝐺 : 𝐼 ⟶ ℕ0𝐺r𝐹 ) ) → ( 𝐺 supp 0 ) = ( 𝐺 “ ℕ ) )
4 simpr2 ( ( 𝐼𝑉 ∧ ( 𝐹𝐷𝐺 : 𝐼 ⟶ ℕ0𝐺r𝐹 ) ) → 𝐺 : 𝐼 ⟶ ℕ0 )
5 eldifi ( 𝑥 ∈ ( 𝐼 ∖ ( 𝐹 “ ℕ ) ) → 𝑥𝐼 )
6 simpr3 ( ( 𝐼𝑉 ∧ ( 𝐹𝐷𝐺 : 𝐼 ⟶ ℕ0𝐺r𝐹 ) ) → 𝐺r𝐹 )
7 4 ffnd ( ( 𝐼𝑉 ∧ ( 𝐹𝐷𝐺 : 𝐼 ⟶ ℕ0𝐺r𝐹 ) ) → 𝐺 Fn 𝐼 )
8 1 psrbagfOLD ( ( 𝐼𝑉𝐹𝐷 ) → 𝐹 : 𝐼 ⟶ ℕ0 )
9 8 3ad2antr1 ( ( 𝐼𝑉 ∧ ( 𝐹𝐷𝐺 : 𝐼 ⟶ ℕ0𝐺r𝐹 ) ) → 𝐹 : 𝐼 ⟶ ℕ0 )
10 9 ffnd ( ( 𝐼𝑉 ∧ ( 𝐹𝐷𝐺 : 𝐼 ⟶ ℕ0𝐺r𝐹 ) ) → 𝐹 Fn 𝐼 )
11 simpl ( ( 𝐼𝑉 ∧ ( 𝐹𝐷𝐺 : 𝐼 ⟶ ℕ0𝐺r𝐹 ) ) → 𝐼𝑉 )
12 inidm ( 𝐼𝐼 ) = 𝐼
13 eqidd ( ( ( 𝐼𝑉 ∧ ( 𝐹𝐷𝐺 : 𝐼 ⟶ ℕ0𝐺r𝐹 ) ) ∧ 𝑥𝐼 ) → ( 𝐺𝑥 ) = ( 𝐺𝑥 ) )
14 eqidd ( ( ( 𝐼𝑉 ∧ ( 𝐹𝐷𝐺 : 𝐼 ⟶ ℕ0𝐺r𝐹 ) ) ∧ 𝑥𝐼 ) → ( 𝐹𝑥 ) = ( 𝐹𝑥 ) )
15 7 10 11 11 12 13 14 ofrfval ( ( 𝐼𝑉 ∧ ( 𝐹𝐷𝐺 : 𝐼 ⟶ ℕ0𝐺r𝐹 ) ) → ( 𝐺r𝐹 ↔ ∀ 𝑥𝐼 ( 𝐺𝑥 ) ≤ ( 𝐹𝑥 ) ) )
16 6 15 mpbid ( ( 𝐼𝑉 ∧ ( 𝐹𝐷𝐺 : 𝐼 ⟶ ℕ0𝐺r𝐹 ) ) → ∀ 𝑥𝐼 ( 𝐺𝑥 ) ≤ ( 𝐹𝑥 ) )
17 16 r19.21bi ( ( ( 𝐼𝑉 ∧ ( 𝐹𝐷𝐺 : 𝐼 ⟶ ℕ0𝐺r𝐹 ) ) ∧ 𝑥𝐼 ) → ( 𝐺𝑥 ) ≤ ( 𝐹𝑥 ) )
18 5 17 sylan2 ( ( ( 𝐼𝑉 ∧ ( 𝐹𝐷𝐺 : 𝐼 ⟶ ℕ0𝐺r𝐹 ) ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝐹 “ ℕ ) ) ) → ( 𝐺𝑥 ) ≤ ( 𝐹𝑥 ) )
19 11 9 jca ( ( 𝐼𝑉 ∧ ( 𝐹𝐷𝐺 : 𝐼 ⟶ ℕ0𝐺r𝐹 ) ) → ( 𝐼𝑉𝐹 : 𝐼 ⟶ ℕ0 ) )
20 frnnn0supp ( ( 𝐼𝑉𝐹 : 𝐼 ⟶ ℕ0 ) → ( 𝐹 supp 0 ) = ( 𝐹 “ ℕ ) )
21 eqimss ( ( 𝐹 supp 0 ) = ( 𝐹 “ ℕ ) → ( 𝐹 supp 0 ) ⊆ ( 𝐹 “ ℕ ) )
22 19 20 21 3syl ( ( 𝐼𝑉 ∧ ( 𝐹𝐷𝐺 : 𝐼 ⟶ ℕ0𝐺r𝐹 ) ) → ( 𝐹 supp 0 ) ⊆ ( 𝐹 “ ℕ ) )
23 c0ex 0 ∈ V
24 23 a1i ( ( 𝐼𝑉 ∧ ( 𝐹𝐷𝐺 : 𝐼 ⟶ ℕ0𝐺r𝐹 ) ) → 0 ∈ V )
25 9 22 11 24 suppssr ( ( ( 𝐼𝑉 ∧ ( 𝐹𝐷𝐺 : 𝐼 ⟶ ℕ0𝐺r𝐹 ) ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝐹 “ ℕ ) ) ) → ( 𝐹𝑥 ) = 0 )
26 18 25 breqtrd ( ( ( 𝐼𝑉 ∧ ( 𝐹𝐷𝐺 : 𝐼 ⟶ ℕ0𝐺r𝐹 ) ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝐹 “ ℕ ) ) ) → ( 𝐺𝑥 ) ≤ 0 )
27 ffvelrn ( ( 𝐺 : 𝐼 ⟶ ℕ0𝑥𝐼 ) → ( 𝐺𝑥 ) ∈ ℕ0 )
28 4 5 27 syl2an ( ( ( 𝐼𝑉 ∧ ( 𝐹𝐷𝐺 : 𝐼 ⟶ ℕ0𝐺r𝐹 ) ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝐹 “ ℕ ) ) ) → ( 𝐺𝑥 ) ∈ ℕ0 )
29 28 nn0ge0d ( ( ( 𝐼𝑉 ∧ ( 𝐹𝐷𝐺 : 𝐼 ⟶ ℕ0𝐺r𝐹 ) ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝐹 “ ℕ ) ) ) → 0 ≤ ( 𝐺𝑥 ) )
30 28 nn0red ( ( ( 𝐼𝑉 ∧ ( 𝐹𝐷𝐺 : 𝐼 ⟶ ℕ0𝐺r𝐹 ) ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝐹 “ ℕ ) ) ) → ( 𝐺𝑥 ) ∈ ℝ )
31 0re 0 ∈ ℝ
32 letri3 ( ( ( 𝐺𝑥 ) ∈ ℝ ∧ 0 ∈ ℝ ) → ( ( 𝐺𝑥 ) = 0 ↔ ( ( 𝐺𝑥 ) ≤ 0 ∧ 0 ≤ ( 𝐺𝑥 ) ) ) )
33 30 31 32 sylancl ( ( ( 𝐼𝑉 ∧ ( 𝐹𝐷𝐺 : 𝐼 ⟶ ℕ0𝐺r𝐹 ) ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝐹 “ ℕ ) ) ) → ( ( 𝐺𝑥 ) = 0 ↔ ( ( 𝐺𝑥 ) ≤ 0 ∧ 0 ≤ ( 𝐺𝑥 ) ) ) )
34 26 29 33 mpbir2and ( ( ( 𝐼𝑉 ∧ ( 𝐹𝐷𝐺 : 𝐼 ⟶ ℕ0𝐺r𝐹 ) ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝐹 “ ℕ ) ) ) → ( 𝐺𝑥 ) = 0 )
35 4 34 suppss ( ( 𝐼𝑉 ∧ ( 𝐹𝐷𝐺 : 𝐼 ⟶ ℕ0𝐺r𝐹 ) ) → ( 𝐺 supp 0 ) ⊆ ( 𝐹 “ ℕ ) )
36 3 35 eqsstrrd ( ( 𝐼𝑉 ∧ ( 𝐹𝐷𝐺 : 𝐼 ⟶ ℕ0𝐺r𝐹 ) ) → ( 𝐺 “ ℕ ) ⊆ ( 𝐹 “ ℕ ) )