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 ˙