Metamath Proof Explorer

Theorem dibopelvalN

Description: Member of the partial isomorphism B. (Contributed by NM, 18-Jan-2014) (Revised by Mario Carneiro, 6-May-2015) (New usage is discouraged.)

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

Proof

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