Metamath Proof Explorer

Theorem carsgmon

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

Ref Expression
Hypotheses carsgval.1 ⊢ φ → O ∈ V
carsgval.2 ⊢ φ → M : 𝒫 O ⟶ 0 +∞
carsgmon.1 ⊢ φ → A ⊆ B
carsgmon.2 ⊢ φ → B ∈ 𝒫 O
carsgmon.3 ⊢ φ ∧ x ⊆ y ∧ y ∈ 𝒫 O → M ⁡ x ≤ M ⁡ y
Assertion carsgmon ⊢ φ → M ⁡ A ≤ M ⁡ B

Proof

Step Hyp Ref Expression
1 carsgval.1 ⊢ φ → O ∈ V
2 carsgval.2 ⊢ φ → M : 𝒫 O ⟶ 0 +∞
3 carsgmon.1 ⊢ φ → A ⊆ B
4 carsgmon.2 ⊢ φ → B ∈ 𝒫 O
5 carsgmon.3 ⊢ φ ∧ x ⊆ y ∧ y ∈ 𝒫 O → M ⁡ x ≤ M ⁡ y
6 4 3 ssexd ⊢ φ → A ∈ V
7 id ⊢ φ → φ
8 sseq1 ⊢ x = A → x ⊆ y ↔ A ⊆ y
9 8 3anbi2d ⊢ x = A → φ ∧ x ⊆ y ∧ y ∈ 𝒫 O ↔ φ ∧ A ⊆ y ∧ y ∈ 𝒫 O
10 fveq2 ⊢ x = A → M ⁡ x = M ⁡ A
11 10 breq1d ⊢ x = A → M ⁡ x ≤ M ⁡ y ↔ M ⁡ A ≤ M ⁡ y
12 9 11 imbi12d ⊢ x = A → φ ∧ x ⊆ y ∧ y ∈ 𝒫 O → M ⁡ x ≤ M ⁡ y ↔ φ ∧ A ⊆ y ∧ y ∈ 𝒫 O → M ⁡ A ≤ M ⁡ y
13 sseq2 ⊢ y = B → A ⊆ y ↔ A ⊆ B
14 eleq1 ⊢ y = B → y ∈ 𝒫 O ↔ B ∈ 𝒫 O
15 13 14 3anbi23d ⊢ y = B → φ ∧ A ⊆ y ∧ y ∈ 𝒫 O ↔ φ ∧ A ⊆ B ∧ B ∈ 𝒫 O
16 fveq2 ⊢ y = B → M ⁡ y = M ⁡ B
17 16 breq2d ⊢ y = B → M ⁡ A ≤ M ⁡ y ↔ M ⁡ A ≤ M ⁡ B
18 15 17 imbi12d ⊢ y = B → φ ∧ A ⊆ y ∧ y ∈ 𝒫 O → M ⁡ A ≤ M ⁡ y ↔ φ ∧ A ⊆ B ∧ B ∈ 𝒫 O → M ⁡ A ≤ M ⁡ B
19 12 18 5 vtocl2g ⊢ A ∈ V ∧ B ∈ 𝒫 O → φ ∧ A ⊆ B ∧ B ∈ 𝒫 O → M ⁡ A ≤ M ⁡ B
20 19 imp ⊢ A ∈ V ∧ B ∈ 𝒫 O ∧ φ ∧ A ⊆ B ∧ B ∈ 𝒫 O → M ⁡ A ≤ M ⁡ B
21 6 4 7 3 4 20 syl23anc ⊢ φ → M ⁡ A ≤ M ⁡ B