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

Metamath Proof Explorer

Theorem meetval2lem

Description: Lemma for meetval2 and meeteu . (Contributed by NM, 12-Sep-2018) TODO: combine this through meeteu into meetlem ?

Ref Expression
Hypotheses meetval2.b ⊢ B = Base K
meetval2.l ⊢ ≤ ˙ = ≤ K
meetval2.m ⊢ ∧ ˙ = meet ⁡ K
meetval2.k ⊢ φ → K ∈ V
meetval2.x ⊢ φ → X ∈ B
meetval2.y ⊢ φ → Y ∈ B
Assertion meetval2lem ⊢ X ∈ B ∧ Y ∈ B → ∀ y ∈ X Y x ≤ ˙ y ∧ ∀ z ∈ B ∀ y ∈ X Y z ≤ ˙ y → z ≤ ˙ x ↔ x ≤ ˙ X ∧ x ≤ ˙ Y ∧ ∀ z ∈ B z ≤ ˙ X ∧ z ≤ ˙ Y → z ≤ ˙ x

Proof

Step Hyp Ref Expression
1 meetval2.b ⊢ B = Base K
2 meetval2.l ⊢ ≤ ˙ = ≤ K
3 meetval2.m ⊢ ∧ ˙ = meet ⁡ K
4 meetval2.k ⊢ φ → K ∈ V
5 meetval2.x ⊢ φ → X ∈ B
6 meetval2.y ⊢ φ → Y ∈ B
7 breq2 ⊢ y = X → x ≤ ˙ y ↔ x ≤ ˙ X
8 breq2 ⊢ y = Y → x ≤ ˙ y ↔ x ≤ ˙ Y
9 7 8 ralprg ⊢ X ∈ B ∧ Y ∈ B → ∀ y ∈ X Y x ≤ ˙ y ↔ x ≤ ˙ X ∧ x ≤ ˙ Y
10 breq2 ⊢ y = X → z ≤ ˙ y ↔ z ≤ ˙ X
11 breq2 ⊢ y = Y → z ≤ ˙ y ↔ z ≤ ˙ Y
12 10 11 ralprg ⊢ X ∈ B ∧ Y ∈ B → ∀ y ∈ X Y z ≤ ˙ y ↔ z ≤ ˙ X ∧ z ≤ ˙ Y
13 12 imbi1d ⊢ X ∈ B ∧ Y ∈ B → ∀ y ∈ X Y z ≤ ˙ y → z ≤ ˙ x ↔ z ≤ ˙ X ∧ z ≤ ˙ Y → z ≤ ˙ x
14 13 ralbidv ⊢ X ∈ B ∧ Y ∈ B → ∀ z ∈ B ∀ y ∈ X Y z ≤ ˙ y → z ≤ ˙ x ↔ ∀ z ∈ B z ≤ ˙ X ∧ z ≤ ˙ Y → z ≤ ˙ x
15 9 14 anbi12d ⊢ X ∈ B ∧ Y ∈ B → ∀ y ∈ X Y x ≤ ˙ y ∧ ∀ z ∈ B ∀ y ∈ X Y z ≤ ˙ y → z ≤ ˙ x ↔ x ≤ ˙ X ∧ x ≤ ˙ Y ∧ ∀ z ∈ B z ≤ ˙ X ∧ z ≤ ˙ Y → z ≤ ˙ x