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

Metamath Proof Explorer

Theorem dihopelvalbN

Description: Ordered pair member of the partial isomorphism H for argument under W . (Contributed by NM, 21-Mar-2014) (New usage is discouraged.)

Ref Expression
Hypotheses dihval3.b ⊢ B = Base K
dihval3.l ⊢ ≤ ˙ = ≤ K
dihval3.h ⊢ H = LHyp ⁡ K
dihval3.t ⊢ T = LTrn ⁡ K ⁡ W
dihval3.r ⊢ R = trL ⁡ K ⁡ W
dihval3.o ⊢ O = g ∈ T ⟼ I ↾ B
dihval3.i ⊢ I = DIsoH ⁡ K ⁡ W
Assertion dihopelvalbN ⊢ K ∈ V ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W → F S ∈ I ⁡ X ↔ F ∈ T ∧ R ⁡ F ≤ ˙ X ∧ S = O

Proof

Step Hyp Ref Expression
1 dihval3.b ⊢ B = Base K
2 dihval3.l ⊢ ≤ ˙ = ≤ K
3 dihval3.h ⊢ H = LHyp ⁡ K
4 dihval3.t ⊢ T = LTrn ⁡ K ⁡ W
5 dihval3.r ⊢ R = trL ⁡ K ⁡ W
6 dihval3.o ⊢ O = g ∈ T ⟼ I ↾ B
7 dihval3.i ⊢ I = DIsoH ⁡ K ⁡ W
8 eqid ⊢ DIsoB ⁡ K ⁡ W = DIsoB ⁡ K ⁡ W
9 1 2 3 7 8 dihvalb ⊢ K ∈ V ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W → I ⁡ X = DIsoB ⁡ K ⁡ W ⁡ X
10 9 eleq2d ⊢ K ∈ V ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W → F S ∈ I ⁡ X ↔ F S ∈ DIsoB ⁡ K ⁡ W ⁡ X
11 1 2 3 4 5 6 8 dibopelval3 ⊢ K ∈ V ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W → F S ∈ DIsoB ⁡ K ⁡ W ⁡ X ↔ F ∈ T ∧ R ⁡ F ≤ ˙ X ∧ S = O
12 10 11 bitrd ⊢ K ∈ V ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W → F S ∈ I ⁡ X ↔ F ∈ T ∧ R ⁡ F ≤ ˙ X ∧ S = O