Metamath Proof Explorer

Theorem psrbagcon

Description: The analogue of the statement " 0 <_ G <_ F implies 0 <_ F - G <_ F " for finite bags. (Contributed by Mario Carneiro, 29-Dec-2014) Remove a sethood antecedent. (Revised by SN, 5-Aug-2024)

Ref Expression
Hypothesis psrbag.d ⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
Assertion psrbagcon ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) → ( ( 𝐹 ∘f − 𝐺 ) ∈ 𝐷 ∧ ( 𝐹 ∘f − 𝐺 ) ∘r ≤ 𝐹 ) )

Proof

Step Hyp Ref Expression
1 psrbag.d ⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
2 1 psrbagf ⊢ ( 𝐹 ∈ 𝐷 → 𝐹 : 𝐼 ⟶ ℕ0 )
3 2 ffnd ⊢ ( 𝐹 ∈ 𝐷 → 𝐹 Fn 𝐼 )
4 3 3ad2ant1 ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) → 𝐹 Fn 𝐼 )
5 simp2 ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) → 𝐺 : 𝐼 ⟶ ℕ0 )
6 5 ffnd ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) → 𝐺 Fn 𝐼 )
7 id ⊢ ( 𝐹 ∈ 𝐷 → 𝐹 ∈ 𝐷 )
8 7 3 fndmexd ⊢ ( 𝐹 ∈ 𝐷 → 𝐼 ∈ V )
9 8 3ad2ant1 ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) → 𝐼 ∈ V )
10 inidm ⊢ ( 𝐼 ∩ 𝐼 ) = 𝐼
11 4 6 9 9 10 offn ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) → ( 𝐹 ∘f − 𝐺 ) Fn 𝐼 )
12 eqidd ⊢ ( ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
13 eqidd ⊢ ( ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
14 4 6 9 9 10 12 13 ofval ⊢ ( ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝐹 ∘f − 𝐺 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) )
15 simp3 ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) → 𝐺 ∘r ≤ 𝐹 )
16 6 4 9 9 10 13 12 ofrfval ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) → ( 𝐺 ∘r ≤ 𝐹 ↔ ∀ 𝑥 ∈ 𝐼 ( 𝐺 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
17 15 16 mpbid ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) → ∀ 𝑥 ∈ 𝐼 ( 𝐺 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) )
18 17 r19.21bi ⊢ ( ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝐺 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) )
19 5 ffvelcdmda ⊢ ( ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝐺 ‘ 𝑥 ) ∈ ℕ0 )
20 2 3ad2ant1 ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) → 𝐹 : 𝐼 ⟶ ℕ0 )
21 20 ffvelcdmda ⊢ ( ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℕ0 )
22 nn0sub ⊢ ( ( ( 𝐺 ‘ 𝑥 ) ∈ ℕ0 ∧ ( 𝐹 ‘ 𝑥 ) ∈ ℕ0 ) → ( ( 𝐺 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) ↔ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ∈ ℕ0 ) )
23 19 21 22 syl2anc ⊢ ( ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝐺 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) ↔ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ∈ ℕ0 ) )
24 18 23 mpbid ⊢ ( ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ∈ ℕ0 )
25 14 24 eqeltrd ⊢ ( ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝐹 ∘f − 𝐺 ) ‘ 𝑥 ) ∈ ℕ0 )
26 25 ralrimiva ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) → ∀ 𝑥 ∈ 𝐼 ( ( 𝐹 ∘f − 𝐺 ) ‘ 𝑥 ) ∈ ℕ0 )
27 ffnfv ⊢ ( ( 𝐹 ∘f − 𝐺 ) : 𝐼 ⟶ ℕ0 ↔ ( ( 𝐹 ∘f − 𝐺 ) Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝐹 ∘f − 𝐺 ) ‘ 𝑥 ) ∈ ℕ0 ) )
28 11 26 27 sylanbrc ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) → ( 𝐹 ∘f − 𝐺 ) : 𝐼 ⟶ ℕ0 )
29 simp1 ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) → 𝐹 ∈ 𝐷 )
30 1 psrbag ⊢ ( 𝐼 ∈ V → ( 𝐹 ∈ 𝐷 ↔ ( 𝐹 : 𝐼 ⟶ ℕ0 ∧ ( ◡ 𝐹 “ ℕ ) ∈ Fin ) ) )
31 9 30 syl ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) → ( 𝐹 ∈ 𝐷 ↔ ( 𝐹 : 𝐼 ⟶ ℕ0 ∧ ( ◡ 𝐹 “ ℕ ) ∈ Fin ) ) )
32 29 31 mpbid ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) → ( 𝐹 : 𝐼 ⟶ ℕ0 ∧ ( ◡ 𝐹 “ ℕ ) ∈ Fin ) )
33 32 simprd ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) → ( ◡ 𝐹 “ ℕ ) ∈ Fin )
34 19 nn0ge0d ⊢ ( ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) ∧ 𝑥 ∈ 𝐼 ) → 0 ≤ ( 𝐺 ‘ 𝑥 ) )
35 21 nn0red ⊢ ( ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
36 19 nn0red ⊢ ( ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝐺 ‘ 𝑥 ) ∈ ℝ )
37 35 36 subge02d ⊢ ( ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) ∧ 𝑥 ∈ 𝐼 ) → ( 0 ≤ ( 𝐺 ‘ 𝑥 ) ↔ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
38 34 37 mpbid ⊢ ( ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ≤ ( 𝐹 ‘ 𝑥 ) )
39 38 ralrimiva ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) → ∀ 𝑥 ∈ 𝐼 ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ≤ ( 𝐹 ‘ 𝑥 ) )
40 11 4 9 9 10 14 12 ofrfval ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) → ( ( 𝐹 ∘f − 𝐺 ) ∘r ≤ 𝐹 ↔ ∀ 𝑥 ∈ 𝐼 ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
41 39 40 mpbird ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) → ( 𝐹 ∘f − 𝐺 ) ∘r ≤ 𝐹 )
42 1 psrbaglesupp ⊢ ( ( 𝐹 ∈ 𝐷 ∧ ( 𝐹 ∘f − 𝐺 ) : 𝐼 ⟶ ℕ0 ∧ ( 𝐹 ∘f − 𝐺 ) ∘r ≤ 𝐹 ) → ( ◡ ( 𝐹 ∘f − 𝐺 ) “ ℕ ) ⊆ ( ◡ 𝐹 “ ℕ ) )
43 29 28 41 42 syl3anc ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) → ( ◡ ( 𝐹 ∘f − 𝐺 ) “ ℕ ) ⊆ ( ◡ 𝐹 “ ℕ ) )
44 33 43 ssfid ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) → ( ◡ ( 𝐹 ∘f − 𝐺 ) “ ℕ ) ∈ Fin )
45 1 psrbag ⊢ ( 𝐼 ∈ V → ( ( 𝐹 ∘f − 𝐺 ) ∈ 𝐷 ↔ ( ( 𝐹 ∘f − 𝐺 ) : 𝐼 ⟶ ℕ0 ∧ ( ◡ ( 𝐹 ∘f − 𝐺 ) “ ℕ ) ∈ Fin ) ) )
46 9 45 syl ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) → ( ( 𝐹 ∘f − 𝐺 ) ∈ 𝐷 ↔ ( ( 𝐹 ∘f − 𝐺 ) : 𝐼 ⟶ ℕ0 ∧ ( ◡ ( 𝐹 ∘f − 𝐺 ) “ ℕ ) ∈ Fin ) ) )
47 28 44 46 mpbir2and ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) → ( 𝐹 ∘f − 𝐺 ) ∈ 𝐷 )
48 47 41 jca ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) → ( ( 𝐹 ∘f − 𝐺 ) ∈ 𝐷 ∧ ( 𝐹 ∘f − 𝐺 ) ∘r ≤ 𝐹 ) )