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

Metamath Proof Explorer

Theorem joinval2lem

Description: Lemma for joinval2 and joineu . (Contributed by NM, 12-Sep-2018) TODO: combine this through joineu into joinlem ?

Ref Expression
Hypotheses joinval2.b ⊢ B = Base K
joinval2.l ⊢ ≤ ˙ = ≤ K
joinval2.j ⊢ ∨ ˙ = join ⁡ K
joinval2.k ⊢ φ → K ∈ V
joinval2.x ⊢ φ → X ∈ B
joinval2.y ⊢ φ → Y ∈ B
Assertion joinval2lem ⊢ X ∈ B ∧ Y ∈ B → ∀ y ∈ X Y y ≤ ˙ x ∧ ∀ z ∈ B ∀ y ∈ X Y y ≤ ˙ z → x ≤ ˙ z ↔ X ≤ ˙ x ∧ Y ≤ ˙ x ∧ ∀ z ∈ B X ≤ ˙ z ∧ Y ≤ ˙ z → x ≤ ˙ z

Proof

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