Metamath Proof Explorer

Theorem dibopelval2

Description: Member of the partial isomorphism B. (Contributed by NM, 3-Mar-2014) (Revised by Mario Carneiro, 6-May-2015)

Ref Expression
Hypotheses dibval2.b ⊢ B = Base K
dibval2.l ⊢ ≤ ˙ = ≤ K
dibval2.h ⊢ H = LHyp ⁡ K
dibval2.t ⊢ T = LTrn ⁡ K ⁡ W
dibval2.o ⊢ 0 ˙ = f ∈ T ⟼ I ↾ B
dibval2.j ⊢ J = DIsoA ⁡ K ⁡ W
dibval2.i ⊢ I = DIsoB ⁡ K ⁡ W
Assertion dibopelval2 ⊢ K ∈ V ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W → F S ∈ I ⁡ X ↔ F ∈ J ⁡ X ∧ S = 0 ˙

Proof

Step Hyp Ref Expression
1 dibval2.b ⊢ B = Base K
2 dibval2.l ⊢ ≤ ˙ = ≤ K
3 dibval2.h ⊢ H = LHyp ⁡ K
4 dibval2.t ⊢ T = LTrn ⁡ K ⁡ W
5 dibval2.o ⊢ 0 ˙ = f ∈ T ⟼ I ↾ B
6 dibval2.j ⊢ J = DIsoA ⁡ K ⁡ W
7 dibval2.i ⊢ I = DIsoB ⁡ K ⁡ W
8 1 2 3 4 5 6 7 dibval2 ⊢ K ∈ V ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W → I ⁡ X = J ⁡ X × 0 ˙
9 8 eleq2d ⊢ K ∈ V ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W → F S ∈ I ⁡ X ↔ F S ∈ J ⁡ X × 0 ˙
10 opelxp ⊢ F S ∈ J ⁡ X × 0 ˙ ↔ F ∈ J ⁡ X ∧ S ∈ 0 ˙
11 4 fvexi ⊢ T ∈ V
12 11 mptex ⊢ f ∈ T ⟼ I ↾ B ∈ V
13 5 12 eqeltri ⊢ 0 ˙ ∈ V
14 13 elsn2 ⊢ S ∈ 0 ˙ ↔ S = 0 ˙
15 14 anbi2i ⊢ F ∈ J ⁡ X ∧ S ∈ 0 ˙ ↔ F ∈ J ⁡ X ∧ S = 0 ˙
16 10 15 bitri ⊢ F S ∈ J ⁡ X × 0 ˙ ↔ F ∈ J ⁡ X ∧ S = 0 ˙
17 9 16 bitrdi ⊢ K ∈ V ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W → F S ∈ I ⁡ X ↔ F ∈ J ⁡ X ∧ S = 0 ˙