Metamath Proof Explorer

Theorem dibn0

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

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

Proof

Step Hyp Ref Expression
1 dibn0.b ⊢B=BaseK
2 dibn0.l ⊢≤˙=≤K
3 dibn0.h ⊢H=LHyp⁡K
4 dibn0.i ⊢I=DIsoB⁡K⁡W
5 eqid ⊢LTrn⁡K⁡W=LTrn⁡K⁡W
6 eqid ⊢f∈LTrn⁡K⁡W⟼I↾B=f∈LTrn⁡K⁡W⟼I↾B
7 eqid ⊢DIsoA⁡K⁡W=DIsoA⁡K⁡W
8 1 2 3 5 6 7 4 dibval2 ⊢K∈HL∧W∈H∧X∈B∧X≤˙W→I⁡X=DIsoA⁡K⁡W⁡X×f∈LTrn⁡K⁡W⟼I↾B
9 1 2 3 7 dian0 ⊢K∈HL∧W∈H∧X∈B∧X≤˙W→DIsoA⁡K⁡W⁡X≠∅
10 fvex ⊢LTrn⁡K⁡W∈V
11 10 mptex ⊢f∈LTrn⁡K⁡W⟼I↾B∈V
12 11 snnz ⊢f∈LTrn⁡K⁡W⟼I↾B≠∅
13 9 12 jctir ⊢K∈HL∧W∈H∧X∈B∧X≤˙W→DIsoA⁡K⁡W⁡X≠∅∧f∈LTrn⁡K⁡W⟼I↾B≠∅
14 xpnz ⊢DIsoA⁡K⁡W⁡X≠∅∧f∈LTrn⁡K⁡W⟼I↾B≠∅↔DIsoA⁡K⁡W⁡X×f∈LTrn⁡K⁡W⟼I↾B≠∅
15 13 14 sylib ⊢K∈HL∧W∈H∧X∈B∧X≤˙W→DIsoA⁡K⁡W⁡X×f∈LTrn⁡K⁡W⟼I↾B≠∅
16 8 15 eqnetrd ⊢K∈HL∧W∈H∧X∈B∧X≤˙W→I⁡X≠∅