Metamath Proof Explorer

Theorem dian0

Description: The value of the partial isomorphism A is not empty. (Contributed by NM, 17-Jan-2014)

Ref Expression
Hypotheses dian0.b ⊢B=BaseK
dian0.l ⊢≤˙=≤K
dian0.h ⊢H=LHyp⁡K
dian0.i ⊢I=DIsoA⁡K⁡W
Assertion dian0 ⊢K∈HL∧W∈H∧X∈B∧X≤˙W→I⁡X≠∅

Proof

Step Hyp Ref Expression
1 dian0.b ⊢B=BaseK
2 dian0.l ⊢≤˙=≤K
3 dian0.h ⊢H=LHyp⁡K
4 dian0.i ⊢I=DIsoA⁡K⁡W
5 eqid ⊢LTrn⁡K⁡W=LTrn⁡K⁡W
6 1 3 5 idltrn ⊢K∈HL∧W∈H→I↾B∈LTrn⁡K⁡W
7 6 adantr ⊢K∈HL∧W∈H∧X∈B∧X≤˙W→I↾B∈LTrn⁡K⁡W
8 eqid ⊢0.⁡K=0.⁡K
9 eqid ⊢trL⁡K⁡W=trL⁡K⁡W
10 1 8 3 9 trlid0 ⊢K∈HL∧W∈H→trL⁡K⁡W⁡I↾B=0.⁡K
11 10 adantr ⊢K∈HL∧W∈H∧X∈B∧X≤˙W→trL⁡K⁡W⁡I↾B=0.⁡K
12 hlatl ⊢K∈HL→K∈AtLat
13 12 adantr ⊢K∈HL∧W∈H→K∈AtLat
14 simpl ⊢X∈B∧X≤˙W→X∈B
15 1 2 8 atl0le ⊢K∈AtLat∧X∈B→0.⁡K≤˙X
16 13 14 15 syl2an ⊢K∈HL∧W∈H∧X∈B∧X≤˙W→0.⁡K≤˙X
17 11 16 eqbrtrd ⊢K∈HL∧W∈H∧X∈B∧X≤˙W→trL⁡K⁡W⁡I↾B≤˙X
18 1 2 3 5 9 4 diaelval ⊢K∈HL∧W∈H∧X∈B∧X≤˙W→I↾B∈I⁡X↔I↾B∈LTrn⁡K⁡W∧trL⁡K⁡W⁡I↾B≤˙X
19 7 17 18 mpbir2and ⊢K∈HL∧W∈H∧X∈B∧X≤˙W→I↾B∈I⁡X
20 19 ne0d ⊢K∈HL∧W∈H∧X∈B∧X≤˙W→I⁡X≠∅