Metamath Proof Explorer


Theorem psrbaglesupp

Description: The support of a dominated bag is smaller than the dominating bag. (Contributed by Mario Carneiro, 29-Dec-2014) Remove a sethood antecedent. (Revised by SN, 5-Aug-2024)

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

Proof

Step Hyp Ref Expression
1 psrbag.d 𝐷 = { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin }
2 df-ofr r ≤ = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∀ 𝑐 ∈ ( dom 𝑎 ∩ dom 𝑏 ) ( 𝑎𝑐 ) ≤ ( 𝑏𝑐 ) }
3 2 relopabiv Rel ∘r
4 3 brrelex1i ( 𝐺r𝐹𝐺 ∈ V )
5 4 3ad2ant3 ( ( 𝐹𝐷𝐺 : 𝐼 ⟶ ℕ0𝐺r𝐹 ) → 𝐺 ∈ V )
6 simp2 ( ( 𝐹𝐷𝐺 : 𝐼 ⟶ ℕ0𝐺r𝐹 ) → 𝐺 : 𝐼 ⟶ ℕ0 )
7 frnnn0suppg ( ( 𝐺 ∈ V ∧ 𝐺 : 𝐼 ⟶ ℕ0 ) → ( 𝐺 supp 0 ) = ( 𝐺 “ ℕ ) )
8 5 6 7 syl2anc ( ( 𝐹𝐷𝐺 : 𝐼 ⟶ ℕ0𝐺r𝐹 ) → ( 𝐺 supp 0 ) = ( 𝐺 “ ℕ ) )
9 eldifi ( 𝑥 ∈ ( 𝐼 ∖ ( 𝐹 “ ℕ ) ) → 𝑥𝐼 )
10 simp3 ( ( 𝐹𝐷𝐺 : 𝐼 ⟶ ℕ0𝐺r𝐹 ) → 𝐺r𝐹 )
11 6 ffnd ( ( 𝐹𝐷𝐺 : 𝐼 ⟶ ℕ0𝐺r𝐹 ) → 𝐺 Fn 𝐼 )
12 1 psrbagf ( 𝐹𝐷𝐹 : 𝐼 ⟶ ℕ0 )
13 12 3ad2ant1 ( ( 𝐹𝐷𝐺 : 𝐼 ⟶ ℕ0𝐺r𝐹 ) → 𝐹 : 𝐼 ⟶ ℕ0 )
14 13 ffnd ( ( 𝐹𝐷𝐺 : 𝐼 ⟶ ℕ0𝐺r𝐹 ) → 𝐹 Fn 𝐼 )
15 simp1 ( ( 𝐹𝐷𝐺 : 𝐼 ⟶ ℕ0𝐺r𝐹 ) → 𝐹𝐷 )
16 inidm ( 𝐼𝐼 ) = 𝐼
17 eqidd ( ( ( 𝐹𝐷𝐺 : 𝐼 ⟶ ℕ0𝐺r𝐹 ) ∧ 𝑥𝐼 ) → ( 𝐺𝑥 ) = ( 𝐺𝑥 ) )
18 eqidd ( ( ( 𝐹𝐷𝐺 : 𝐼 ⟶ ℕ0𝐺r𝐹 ) ∧ 𝑥𝐼 ) → ( 𝐹𝑥 ) = ( 𝐹𝑥 ) )
19 11 14 5 15 16 17 18 ofrfvalg ( ( 𝐹𝐷𝐺 : 𝐼 ⟶ ℕ0𝐺r𝐹 ) → ( 𝐺r𝐹 ↔ ∀ 𝑥𝐼 ( 𝐺𝑥 ) ≤ ( 𝐹𝑥 ) ) )
20 10 19 mpbid ( ( 𝐹𝐷𝐺 : 𝐼 ⟶ ℕ0𝐺r𝐹 ) → ∀ 𝑥𝐼 ( 𝐺𝑥 ) ≤ ( 𝐹𝑥 ) )
21 20 r19.21bi ( ( ( 𝐹𝐷𝐺 : 𝐼 ⟶ ℕ0𝐺r𝐹 ) ∧ 𝑥𝐼 ) → ( 𝐺𝑥 ) ≤ ( 𝐹𝑥 ) )
22 9 21 sylan2 ( ( ( 𝐹𝐷𝐺 : 𝐼 ⟶ ℕ0𝐺r𝐹 ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝐹 “ ℕ ) ) ) → ( 𝐺𝑥 ) ≤ ( 𝐹𝑥 ) )
23 frnnn0suppg ( ( 𝐹𝐷𝐹 : 𝐼 ⟶ ℕ0 ) → ( 𝐹 supp 0 ) = ( 𝐹 “ ℕ ) )
24 15 13 23 syl2anc ( ( 𝐹𝐷𝐺 : 𝐼 ⟶ ℕ0𝐺r𝐹 ) → ( 𝐹 supp 0 ) = ( 𝐹 “ ℕ ) )
25 eqimss ( ( 𝐹 supp 0 ) = ( 𝐹 “ ℕ ) → ( 𝐹 supp 0 ) ⊆ ( 𝐹 “ ℕ ) )
26 24 25 syl ( ( 𝐹𝐷𝐺 : 𝐼 ⟶ ℕ0𝐺r𝐹 ) → ( 𝐹 supp 0 ) ⊆ ( 𝐹 “ ℕ ) )
27 c0ex 0 ∈ V
28 27 a1i ( ( 𝐹𝐷𝐺 : 𝐼 ⟶ ℕ0𝐺r𝐹 ) → 0 ∈ V )
29 13 26 15 28 suppssrg ( ( ( 𝐹𝐷𝐺 : 𝐼 ⟶ ℕ0𝐺r𝐹 ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝐹 “ ℕ ) ) ) → ( 𝐹𝑥 ) = 0 )
30 22 29 breqtrd ( ( ( 𝐹𝐷𝐺 : 𝐼 ⟶ ℕ0𝐺r𝐹 ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝐹 “ ℕ ) ) ) → ( 𝐺𝑥 ) ≤ 0 )
31 ffvelrn ( ( 𝐺 : 𝐼 ⟶ ℕ0𝑥𝐼 ) → ( 𝐺𝑥 ) ∈ ℕ0 )
32 6 9 31 syl2an ( ( ( 𝐹𝐷𝐺 : 𝐼 ⟶ ℕ0𝐺r𝐹 ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝐹 “ ℕ ) ) ) → ( 𝐺𝑥 ) ∈ ℕ0 )
33 32 nn0ge0d ( ( ( 𝐹𝐷𝐺 : 𝐼 ⟶ ℕ0𝐺r𝐹 ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝐹 “ ℕ ) ) ) → 0 ≤ ( 𝐺𝑥 ) )
34 32 nn0red ( ( ( 𝐹𝐷𝐺 : 𝐼 ⟶ ℕ0𝐺r𝐹 ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝐹 “ ℕ ) ) ) → ( 𝐺𝑥 ) ∈ ℝ )
35 0re 0 ∈ ℝ
36 letri3 ( ( ( 𝐺𝑥 ) ∈ ℝ ∧ 0 ∈ ℝ ) → ( ( 𝐺𝑥 ) = 0 ↔ ( ( 𝐺𝑥 ) ≤ 0 ∧ 0 ≤ ( 𝐺𝑥 ) ) ) )
37 34 35 36 sylancl ( ( ( 𝐹𝐷𝐺 : 𝐼 ⟶ ℕ0𝐺r𝐹 ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝐹 “ ℕ ) ) ) → ( ( 𝐺𝑥 ) = 0 ↔ ( ( 𝐺𝑥 ) ≤ 0 ∧ 0 ≤ ( 𝐺𝑥 ) ) ) )
38 30 33 37 mpbir2and ( ( ( 𝐹𝐷𝐺 : 𝐼 ⟶ ℕ0𝐺r𝐹 ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝐹 “ ℕ ) ) ) → ( 𝐺𝑥 ) = 0 )
39 6 38 suppss ( ( 𝐹𝐷𝐺 : 𝐼 ⟶ ℕ0𝐺r𝐹 ) → ( 𝐺 supp 0 ) ⊆ ( 𝐹 “ ℕ ) )
40 8 39 eqsstrrd ( ( 𝐹𝐷𝐺 : 𝐼 ⟶ ℕ0𝐺r𝐹 ) → ( 𝐺 “ ℕ ) ⊆ ( 𝐹 “ ℕ ) )