Metamath Proof Explorer

Theorem carsgmon

Description: Utility lemma: Apply monotony. (Contributed by Thierry Arnoux, 29-May-2020)

Ref Expression
Hypotheses carsgval.1 ⊢ ( 𝜑 → 𝑂 ∈ 𝑉 )
carsgval.2 ⊢ ( 𝜑 → 𝑀 : 𝒫 𝑂 ⟶ ( 0 [,] +∞ ) )
carsgmon.1 ⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
carsgmon.2 ⊢ ( 𝜑 → 𝐵 ∈ 𝒫 𝑂 )
carsgmon.3 ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ 𝑥 ) ≤ ( 𝑀 ‘ 𝑦 ) )
Assertion carsgmon ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ≤ ( 𝑀 ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 carsgval.1 ⊢ ( 𝜑 → 𝑂 ∈ 𝑉 )
2 carsgval.2 ⊢ ( 𝜑 → 𝑀 : 𝒫 𝑂 ⟶ ( 0 [,] +∞ ) )
3 carsgmon.1 ⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
4 carsgmon.2 ⊢ ( 𝜑 → 𝐵 ∈ 𝒫 𝑂 )
5 carsgmon.3 ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ 𝑥 ) ≤ ( 𝑀 ‘ 𝑦 ) )
6 4 3 ssexd ⊢ ( 𝜑 → 𝐴 ∈ V )
7 id ⊢ ( 𝜑 → 𝜑 )
8 sseq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ⊆ 𝑦 ↔ 𝐴 ⊆ 𝑦 ) )
9 8 3anbi2d ⊢ ( 𝑥 = 𝐴 → ( ( 𝜑 ∧ 𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝒫 𝑂 ) ↔ ( 𝜑 ∧ 𝐴 ⊆ 𝑦 ∧ 𝑦 ∈ 𝒫 𝑂 ) ) )
10 fveq2 ⊢ ( 𝑥 = 𝐴 → ( 𝑀 ‘ 𝑥 ) = ( 𝑀 ‘ 𝐴 ) )
11 10 breq1d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑀 ‘ 𝑥 ) ≤ ( 𝑀 ‘ 𝑦 ) ↔ ( 𝑀 ‘ 𝐴 ) ≤ ( 𝑀 ‘ 𝑦 ) ) )
12 9 11 imbi12d ⊢ ( 𝑥 = 𝐴 → ( ( ( 𝜑 ∧ 𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ 𝑥 ) ≤ ( 𝑀 ‘ 𝑦 ) ) ↔ ( ( 𝜑 ∧ 𝐴 ⊆ 𝑦 ∧ 𝑦 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ 𝐴 ) ≤ ( 𝑀 ‘ 𝑦 ) ) ) )
13 sseq2 ⊢ ( 𝑦 = 𝐵 → ( 𝐴 ⊆ 𝑦 ↔ 𝐴 ⊆ 𝐵 ) )
14 eleq1 ⊢ ( 𝑦 = 𝐵 → ( 𝑦 ∈ 𝒫 𝑂 ↔ 𝐵 ∈ 𝒫 𝑂 ) )
15 13 14 3anbi23d ⊢ ( 𝑦 = 𝐵 → ( ( 𝜑 ∧ 𝐴 ⊆ 𝑦 ∧ 𝑦 ∈ 𝒫 𝑂 ) ↔ ( 𝜑 ∧ 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝒫 𝑂 ) ) )
16 fveq2 ⊢ ( 𝑦 = 𝐵 → ( 𝑀 ‘ 𝑦 ) = ( 𝑀 ‘ 𝐵 ) )
17 16 breq2d ⊢ ( 𝑦 = 𝐵 → ( ( 𝑀 ‘ 𝐴 ) ≤ ( 𝑀 ‘ 𝑦 ) ↔ ( 𝑀 ‘ 𝐴 ) ≤ ( 𝑀 ‘ 𝐵 ) ) )
18 15 17 imbi12d ⊢ ( 𝑦 = 𝐵 → ( ( ( 𝜑 ∧ 𝐴 ⊆ 𝑦 ∧ 𝑦 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ 𝐴 ) ≤ ( 𝑀 ‘ 𝑦 ) ) ↔ ( ( 𝜑 ∧ 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ 𝐴 ) ≤ ( 𝑀 ‘ 𝐵 ) ) ) )
19 12 18 5 vtocl2g ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ 𝒫 𝑂 ) → ( ( 𝜑 ∧ 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ 𝐴 ) ≤ ( 𝑀 ‘ 𝐵 ) ) )
20 19 imp ⊢ ( ( ( 𝐴 ∈ V ∧ 𝐵 ∈ 𝒫 𝑂 ) ∧ ( 𝜑 ∧ 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝒫 𝑂 ) ) → ( 𝑀 ‘ 𝐴 ) ≤ ( 𝑀 ‘ 𝐵 ) )
21 6 4 7 3 4 20 syl23anc ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ≤ ( 𝑀 ‘ 𝐵 ) )