This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
Assertion psrbaglesupp ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) → ( ◡ 𝐺 “ ℕ ) ⊆ ( ◡ 𝐹 “ ℕ ) )

Proof

Step Hyp Ref Expression
1 psrbag.d ⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ 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 fcdmnn0suppg ⊢ ( ( 𝐺 ∈ 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 fcdmnn0suppg ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐹 : 𝐼 ⟶ ℕ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 ffvelcdm ⊢ ( ( 𝐺 : 𝐼 ⟶ ℕ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 ≤ 𝐹 ) → ( ◡ 𝐺 “ ℕ ) ⊆ ( ◡ 𝐹 “ ℕ ) )