Metamath Proof Explorer


Theorem dibglbN

Description: Partial isomorphism B of a lattice glb. (Contributed by NM, 9-Mar-2014) (New usage is discouraged.)

Ref Expression
Hypotheses dibglb.g G = glb K
dibglb.h H = LHyp K
dibglb.i I = DIsoB K W
Assertion dibglbN K HL W H S dom I S I G S = x S I x

Proof

Step Hyp Ref Expression
1 dibglb.g G = glb K
2 dibglb.h H = LHyp K
3 dibglb.i I = DIsoB K W
4 simpl K HL W H S dom I S K HL W H
5 simprl K HL W H S dom I S S dom I
6 eqid Base K = Base K
7 eqid K = K
8 6 7 2 3 dibdmN K HL W H dom I = y Base K | y K W
9 8 sseq2d K HL W H S dom I S y Base K | y K W
10 9 adantr K HL W H S dom I S S dom I S y Base K | y K W
11 5 10 mpbid K HL W H S dom I S S y Base K | y K W
12 simprr K HL W H S dom I S S
13 2 3 dibvalrel K HL W H Rel I G S
14 13 adantr K HL W H S y Base K | y K W S Rel I G S
15 n0 S x x S
16 15 biimpi S x x S
17 16 ad2antll K HL W H S y Base K | y K W S x x S
18 2 3 dibvalrel K HL W H Rel I x
19 18 adantr K HL W H S y Base K | y K W S Rel I x
20 19 a1d K HL W H S y Base K | y K W S x S Rel I x
21 20 ancld K HL W H S y Base K | y K W S x S x S Rel I x
22 21 eximdv K HL W H S y Base K | y K W S x x S x x S Rel I x
23 17 22 mpd K HL W H S y Base K | y K W S x x S Rel I x
24 df-rex x S Rel I x x x S Rel I x
25 23 24 sylibr K HL W H S y Base K | y K W S x S Rel I x
26 reliin x S Rel I x Rel x S I x
27 25 26 syl K HL W H S y Base K | y K W S Rel x S I x
28 id K HL W H S y Base K | y K W S K HL W H S y Base K | y K W S
29 simpl K HL W H S y Base K | y K W S K HL W H
30 simprl K HL W H S y Base K | y K W S S y Base K | y K W
31 eqid DIsoA K W = DIsoA K W
32 6 7 2 31 diadm K HL W H dom DIsoA K W = y Base K | y K W
33 32 adantr K HL W H S y Base K | y K W S dom DIsoA K W = y Base K | y K W
34 30 33 sseqtrrd K HL W H S y Base K | y K W S S dom DIsoA K W
35 simprr K HL W H S y Base K | y K W S S
36 1 2 31 diaglbN K HL W H S dom DIsoA K W S DIsoA K W G S = x S DIsoA K W x
37 29 34 35 36 syl12anc K HL W H S y Base K | y K W S DIsoA K W G S = x S DIsoA K W x
38 37 eleq2d K HL W H S y Base K | y K W S f DIsoA K W G S f x S DIsoA K W x
39 vex f V
40 eliin f V f x S DIsoA K W x x S f DIsoA K W x
41 39 40 ax-mp f x S DIsoA K W x x S f DIsoA K W x
42 38 41 bitrdi K HL W H S y Base K | y K W S f DIsoA K W G S x S f DIsoA K W x
43 42 anbi1d K HL W H S y Base K | y K W S f DIsoA K W G S s = h LTrn K W I Base K x S f DIsoA K W x s = h LTrn K W I Base K
44 r19.27zv S x S f DIsoA K W x s = h LTrn K W I Base K x S f DIsoA K W x s = h LTrn K W I Base K
45 44 ad2antll K HL W H S y Base K | y K W S x S f DIsoA K W x s = h LTrn K W I Base K x S f DIsoA K W x s = h LTrn K W I Base K
46 43 45 bitr4d K HL W H S y Base K | y K W S f DIsoA K W G S s = h LTrn K W I Base K x S f DIsoA K W x s = h LTrn K W I Base K
47 hlclat K HL K CLat
48 47 ad2antrr K HL W H S y Base K | y K W S K CLat
49 ssrab2 y Base K | y K W Base K
50 30 49 sstrdi K HL W H S y Base K | y K W S S Base K
51 6 1 clatglbcl K CLat S Base K G S Base K
52 48 50 51 syl2anc K HL W H S y Base K | y K W S G S Base K
53 hllat K HL K Lat
54 53 ad3antrrr K HL W H S y Base K | y K W S x S K Lat
55 47 ad3antrrr K HL W H S y Base K | y K W S x S K CLat
56 simplrl K HL W H S y Base K | y K W S x S S y Base K | y K W
57 56 49 sstrdi K HL W H S y Base K | y K W S x S S Base K
58 55 57 51 syl2anc K HL W H S y Base K | y K W S x S G S Base K
59 50 sselda K HL W H S y Base K | y K W S x S x Base K
60 6 2 lhpbase W H W Base K
61 60 ad3antlr K HL W H S y Base K | y K W S x S W Base K
62 simpr K HL W H S y Base K | y K W S x S x S
63 6 7 1 clatglble K CLat S Base K x S G S K x
64 55 57 62 63 syl3anc K HL W H S y Base K | y K W S x S G S K x
65 30 sselda K HL W H S y Base K | y K W S x S x y Base K | y K W
66 breq1 y = x y K W x K W
67 66 elrab x y Base K | y K W x Base K x K W
68 65 67 sylib K HL W H S y Base K | y K W S x S x Base K x K W
69 68 simprd K HL W H S y Base K | y K W S x S x K W
70 6 7 54 58 59 61 64 69 lattrd K HL W H S y Base K | y K W S x S G S K W
71 17 70 exlimddv K HL W H S y Base K | y K W S G S K W
72 eqid LTrn K W = LTrn K W
73 eqid h LTrn K W I Base K = h LTrn K W I Base K
74 6 7 2 72 73 31 3 dibopelval2 K HL W H G S Base K G S K W f s I G S f DIsoA K W G S s = h LTrn K W I Base K
75 29 52 71 74 syl12anc K HL W H S y Base K | y K W S f s I G S f DIsoA K W G S s = h LTrn K W I Base K
76 opex f s V
77 eliin f s V f s x S I x x S f s I x
78 76 77 ax-mp f s x S I x x S f s I x
79 simpll K HL W H S y Base K | y K W S x S K HL W H
80 6 7 2 72 73 31 3 dibopelval2 K HL W H x Base K x K W f s I x f DIsoA K W x s = h LTrn K W I Base K
81 79 68 80 syl2anc K HL W H S y Base K | y K W S x S f s I x f DIsoA K W x s = h LTrn K W I Base K
82 81 ralbidva K HL W H S y Base K | y K W S x S f s I x x S f DIsoA K W x s = h LTrn K W I Base K
83 78 82 syl5bb K HL W H S y Base K | y K W S f s x S I x x S f DIsoA K W x s = h LTrn K W I Base K
84 46 75 83 3bitr4d K HL W H S y Base K | y K W S f s I G S f s x S I x
85 84 eqrelrdv2 Rel I G S Rel x S I x K HL W H S y Base K | y K W S I G S = x S I x
86 14 27 28 85 syl21anc K HL W H S y Base K | y K W S I G S = x S I x
87 4 11 12 86 syl12anc K HL W H S dom I S I G S = x S I x