Metamath Proof Explorer

Theorem psrbagleadd1

Description: The analogue of " X <_ F implies X + G <_ F + G " (compare leadd1d ) for bags. (Contributed by SN, 2-May-2025)

Ref Expression
Hypotheses psrbag.d ⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
psrbagconf1o.s ⊢ 𝑆 = { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝐹 }
psrbagleadd1.t ⊢ 𝑇 = { 𝑧 ∈ 𝐷 ∣ 𝑧 ∘r ≤ ( 𝐹 ∘f + 𝐺 ) }
Assertion psrbagleadd1 ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ) → ( 𝑋 ∘f + 𝐺 ) ∈ 𝑇 )

Proof

Step Hyp Ref Expression
1 psrbag.d ⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
2 psrbagconf1o.s ⊢ 𝑆 = { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝐹 }
3 psrbagleadd1.t ⊢ 𝑇 = { 𝑧 ∈ 𝐷 ∣ 𝑧 ∘r ≤ ( 𝐹 ∘f + 𝐺 ) }
4 elrabi ⊢ ( 𝑋 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝐹 } → 𝑋 ∈ 𝐷 )
5 4 2 eleq2s ⊢ ( 𝑋 ∈ 𝑆 → 𝑋 ∈ 𝐷 )
6 5 3ad2ant3 ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ) → 𝑋 ∈ 𝐷 )
7 simp2 ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ) → 𝐺 ∈ 𝐷 )
8 1 psrbagaddcl ⊢ ( ( 𝑋 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ) → ( 𝑋 ∘f + 𝐺 ) ∈ 𝐷 )
9 6 7 8 syl2anc ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ) → ( 𝑋 ∘f + 𝐺 ) ∈ 𝐷 )
10 1 psrbagf ⊢ ( 𝑋 ∈ 𝐷 → 𝑋 : 𝐼 ⟶ ℕ0 )
11 6 10 syl ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ) → 𝑋 : 𝐼 ⟶ ℕ0 )
12 11 ffvelcdmda ⊢ ( ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑋 ‘ 𝑥 ) ∈ ℕ0 )
13 12 nn0red ⊢ ( ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑋 ‘ 𝑥 ) ∈ ℝ )
14 1 psrbagf ⊢ ( 𝐹 ∈ 𝐷 → 𝐹 : 𝐼 ⟶ ℕ0 )
15 14 3ad2ant1 ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ) → 𝐹 : 𝐼 ⟶ ℕ0 )
16 15 ffvelcdmda ⊢ ( ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℕ0 )
17 16 nn0red ⊢ ( ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
18 1 psrbagf ⊢ ( 𝐺 ∈ 𝐷 → 𝐺 : 𝐼 ⟶ ℕ0 )
19 18 3ad2ant2 ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ) → 𝐺 : 𝐼 ⟶ ℕ0 )
20 19 ffvelcdmda ⊢ ( ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝐺 ‘ 𝑥 ) ∈ ℕ0 )
21 20 nn0red ⊢ ( ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝐺 ‘ 𝑥 ) ∈ ℝ )
22 breq1 ⊢ ( 𝑦 = 𝑋 → ( 𝑦 ∘r ≤ 𝐹 ↔ 𝑋 ∘r ≤ 𝐹 ) )
23 22 2 elrab2 ⊢ ( 𝑋 ∈ 𝑆 ↔ ( 𝑋 ∈ 𝐷 ∧ 𝑋 ∘r ≤ 𝐹 ) )
24 23 simprbi ⊢ ( 𝑋 ∈ 𝑆 → 𝑋 ∘r ≤ 𝐹 )
25 24 3ad2ant3 ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ) → 𝑋 ∘r ≤ 𝐹 )
26 10 ffnd ⊢ ( 𝑋 ∈ 𝐷 → 𝑋 Fn 𝐼 )
27 5 26 syl ⊢ ( 𝑋 ∈ 𝑆 → 𝑋 Fn 𝐼 )
28 27 3ad2ant3 ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ) → 𝑋 Fn 𝐼 )
29 14 ffnd ⊢ ( 𝐹 ∈ 𝐷 → 𝐹 Fn 𝐼 )
30 29 3ad2ant1 ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ) → 𝐹 Fn 𝐼 )
31 id ⊢ ( 𝐹 ∈ 𝐷 → 𝐹 ∈ 𝐷 )
32 31 29 fndmexd ⊢ ( 𝐹 ∈ 𝐷 → 𝐼 ∈ V )
33 32 3ad2ant1 ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ) → 𝐼 ∈ V )
34 inidm ⊢ ( 𝐼 ∩ 𝐼 ) = 𝐼
35 eqidd ⊢ ( ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑋 ‘ 𝑥 ) = ( 𝑋 ‘ 𝑥 ) )
36 eqidd ⊢ ( ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
37 28 30 33 33 34 35 36 ofrfval ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ) → ( 𝑋 ∘r ≤ 𝐹 ↔ ∀ 𝑥 ∈ 𝐼 ( 𝑋 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
38 25 37 mpbid ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ) → ∀ 𝑥 ∈ 𝐼 ( 𝑋 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) )
39 38 r19.21bi ⊢ ( ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑋 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) )
40 13 17 21 39 leadd1dd ⊢ ( ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑋 ‘ 𝑥 ) + ( 𝐺 ‘ 𝑥 ) ) ≤ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐺 ‘ 𝑥 ) ) )
41 40 ralrimiva ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ) → ∀ 𝑥 ∈ 𝐼 ( ( 𝑋 ‘ 𝑥 ) + ( 𝐺 ‘ 𝑥 ) ) ≤ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐺 ‘ 𝑥 ) ) )
42 1 psrbagf ⊢ ( ( 𝑋 ∘f + 𝐺 ) ∈ 𝐷 → ( 𝑋 ∘f + 𝐺 ) : 𝐼 ⟶ ℕ0 )
43 42 ffnd ⊢ ( ( 𝑋 ∘f + 𝐺 ) ∈ 𝐷 → ( 𝑋 ∘f + 𝐺 ) Fn 𝐼 )
44 9 43 syl ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ) → ( 𝑋 ∘f + 𝐺 ) Fn 𝐼 )
45 1 psrbagaddcl ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ) → ( 𝐹 ∘f + 𝐺 ) ∈ 𝐷 )
46 45 3adant3 ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ) → ( 𝐹 ∘f + 𝐺 ) ∈ 𝐷 )
47 1 psrbagf ⊢ ( ( 𝐹 ∘f + 𝐺 ) ∈ 𝐷 → ( 𝐹 ∘f + 𝐺 ) : 𝐼 ⟶ ℕ0 )
48 47 ffnd ⊢ ( ( 𝐹 ∘f + 𝐺 ) ∈ 𝐷 → ( 𝐹 ∘f + 𝐺 ) Fn 𝐼 )
49 46 48 syl ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ) → ( 𝐹 ∘f + 𝐺 ) Fn 𝐼 )
50 18 ffnd ⊢ ( 𝐺 ∈ 𝐷 → 𝐺 Fn 𝐼 )
51 50 3ad2ant2 ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ) → 𝐺 Fn 𝐼 )
52 eqidd ⊢ ( ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
53 28 51 33 33 34 35 52 ofval ⊢ ( ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑋 ∘f + 𝐺 ) ‘ 𝑥 ) = ( ( 𝑋 ‘ 𝑥 ) + ( 𝐺 ‘ 𝑥 ) ) )
54 30 51 33 33 34 36 52 ofval ⊢ ( ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑥 ) + ( 𝐺 ‘ 𝑥 ) ) )
55 44 49 33 33 34 53 54 ofrfval ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ) → ( ( 𝑋 ∘f + 𝐺 ) ∘r ≤ ( 𝐹 ∘f + 𝐺 ) ↔ ∀ 𝑥 ∈ 𝐼 ( ( 𝑋 ‘ 𝑥 ) + ( 𝐺 ‘ 𝑥 ) ) ≤ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐺 ‘ 𝑥 ) ) ) )
56 41 55 mpbird ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ) → ( 𝑋 ∘f + 𝐺 ) ∘r ≤ ( 𝐹 ∘f + 𝐺 ) )
57 breq1 ⊢ ( 𝑧 = ( 𝑋 ∘f + 𝐺 ) → ( 𝑧 ∘r ≤ ( 𝐹 ∘f + 𝐺 ) ↔ ( 𝑋 ∘f + 𝐺 ) ∘r ≤ ( 𝐹 ∘f + 𝐺 ) ) )
58 57 3 elrab2 ⊢ ( ( 𝑋 ∘f + 𝐺 ) ∈ 𝑇 ↔ ( ( 𝑋 ∘f + 𝐺 ) ∈ 𝐷 ∧ ( 𝑋 ∘f + 𝐺 ) ∘r ≤ ( 𝐹 ∘f + 𝐺 ) ) )
59 9 56 58 sylanbrc ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ) → ( 𝑋 ∘f + 𝐺 ) ∈ 𝑇 )