Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dicn0 Structured version   Unicode version

Theorem dicn0 31991
 Description: The value of the partial isomorphism C is not empty. (Contributed by NM, 15-Feb-2014.)
Hypotheses
Ref Expression
dicn0.l
dicn0.a
dicn0.h
dicn0.i
Assertion
Ref Expression
dicn0

Proof of Theorem dicn0
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpl 445 . . . . . 6
2 dicn0.l . . . . . . . 8
3 eqid 2437 . . . . . . . 8
4 dicn0.a . . . . . . . 8
5 dicn0.h . . . . . . . 8
62, 3, 4, 5lhpocnel 30816 . . . . . . 7
76adantr 453 . . . . . 6
8 simpr 449 . . . . . 6
9 eqid 2437 . . . . . . 7
10 eqid 2437 . . . . . . 7
112, 4, 5, 9, 10ltrniotacl 31377 . . . . . 6
121, 7, 8, 11syl3anc 1185 . . . . 5
13 eqid 2437 . . . . . 6
14 eqid 2437 . . . . . 6
1513, 14tendo02 31585 . . . . 5
1612, 15syl 16 . . . 4
1716eqcomd 2442 . . 3
18 eqid 2437 . . . . 5
1914, 5, 9, 18, 13tendo0cl 31588 . . . 4